Compactly Supported Cutoff Preserves Global $L^2$ Integrability

This statement shows that a compactly supported cutoff converts local $L^2$ control into global $L^2$ control.

Let $n\in\mathbb{N}$ and let $f,\chi:\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)\to\mathbb{R}$. Assume that $\chi$ is continuous and compactly supported. Assume also that, for every compact set $S$, the restriction of $f$ to $S$ belongs to $L^2$ with respect to restricted Lebesgue measure:

Then

The exponent is the Lean MemLp exponent $2$, and the conclusion uses the full volume measure. This is a reusable localization lemma.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem memLp_mul_of_hasCompactSupport {n : ℕ}
    {f χ : EuclideanSpace ℝ (Fin n) → ℝ}
    (hχ : Continuous χ) (hχc : HasCompactSupport χ)
    (hf : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp f 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) :
    MemLp (fun x => χ x * f x) 2
      (volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Previous: HasWeakDerivAlong.mul_of_memLp_two · Next: HasWeakDerivAlong.mul_of_locally_memLp_two.

Source excerpt, lines 186–192 · Frozen source 408915f.