Support Restrict #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Foundation.Measure.aestronglyMeasurable_of_restrict_of_support
{h : Parabolic.Vec3 → ℝ}
{s : Set Parabolic.Vec3}
(hs : MeasurableSet s)
(hmeas : MeasureTheory.AEStronglyMeasurable h (MeasureTheory.volume.restrict s))
(hsupp : Function.support h ⊆ s)
:
If a function is almost everywhere strongly measurable with respect to the
restricted measure volume.restrict s and its support is contained in the
measurable set s, then it is almost everywhere strongly measurable with
respect to the ambient volume.
theorem
CKN.Foundation.Measure.memLp_volume_of_memLp_restrict_of_support
{h : Parabolic.Vec3 → ℝ}
{s : Set Parabolic.Vec3}
{p : ENNReal}
(hmeas : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume)
(hsupp : Function.support h ⊆ s)
(hh : MeasureTheory.MemLp h p (MeasureTheory.volume.restrict s))
:
If a function is MemLp on the restricted measure volume.restrict s and its
support is contained in the measurable set s, then it is MemLp on the
ambient volume.
theorem
CKN.Foundation.Measure.integrable_mul_of_tsupport_subset
{α : Type u_1}
[TopologicalSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f g : α → ℝ}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : Continuous g)
(hgc : HasCompactSupport g)
(hsupport : tsupport g ⊆ s)
:
MeasureTheory.Integrable (fun (x : α) => f x * g x) μ
A continuous compactly supported multiplier localizes an integrable function.