Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.GlobalLocalization

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Localization for the global good-λ extension

The global good-λ argument extends the reflected parent-cube gradient and datum by zero. This file records exactly the identities which let that global extension be used on a ball lying in the original parent cube. In particular, no assertion identifies the extension with the original function away from its support.

theorem HCPolySupport.CubeCalderonZygmund.indicator_aeEq_of_subset {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [Zero E] {μ : MeasureTheory.Measure α} {U B : Set α} {f : α → E} (hB : MeasurableSet B) (hBU : B ⊆ U) : U.indicator f =ᵐ[μ.restrict B] f

On every set contained in U, the zero extension U.indicator f agrees pointwise (and hence almost everywhere) with f.

theorem HCPolySupport.CubeCalderonZygmund.aestronglyMeasurable_indicator_iff_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [TopologicalSpace E] [Zero E] {μ : MeasureTheory.Measure α} {U : Set α} {f : α → E} (hU : MeasurableSet U) : MeasureTheory.AEStronglyMeasurable (U.indicator f) μ ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict U)

Measurability of a zero extension is precisely measurability of the underlying function on its support.

theorem HCPolySupport.CubeCalderonZygmund.memLp_indicator_iff_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {U : Set α} {f : α → E} {p : ENNReal} (hU : MeasurableSet U) : MeasureTheory.MemLp (U.indicator f) p μ ↔ MeasureTheory.MemLp f p (μ.restrict U)

The global Lᵖ membership of a zero extension is exactly its local membership on the support.

theorem HCPolySupport.CubeCalderonZygmund.integral_indicator_eq_integral_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {U : Set α} {f : α → E} (hU : MeasurableSet U) : ∫ (x : α), U.indicator f x ∂μ = ∫ (x : α) in U, f x ∂μ

Integrating a zero extension over the ambient space is integration of the original function over its measurable support.

theorem HCPolySupport.CubeCalderonZygmund.lintegral_indicator_eq_lintegral_restrict {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {U : Set α} {f : α → ENNReal} (hU : MeasurableSet U) : ∫⁻ (x : α), U.indicator f x ∂μ = ∫⁻ (x : α) in U, f x ∂μ

The analogous identity for nonnegative extended-valued integrands.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_indicator_eq_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {U : Set α} {f : α → E} (hU : MeasurableSet U) : sqWeightedMeasure (U.indicator f) μ = sqWeightedMeasure f (μ.restrict U)

Squared weighted measure commutes exactly with extension by zero: its base measure is simply restricted to the support.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_indicator_restrict_eq_of_subset {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {U B : Set α} {f : α → E} (hU : MeasurableSet U) (hB : MeasurableSet B) (hBU : B ⊆ U) : (sqWeightedMeasure (U.indicator f) μ).restrict B = (sqWeightedMeasure f μ).restrict B

On a measurable set inside U, squared weighted mass is unchanged by extension by zero. The test set need not itself be measurable.

theorem HCPolySupport.CubeCalderonZygmund.indicator_tail_set_eq_inter {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {U : Set α} {f : α → E} {a : ℝ} (ha : 0 < a) : {x : α | a < ‖U.indicator f x‖} = U ∩ {x : α | a < ‖f x‖}

A positive-level tail of a zero extension is the corresponding tail inside its support.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_indicator_tail_inter_eq_of_subset {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {U B : Set α} {f : α → E} {a : ℝ} (hU : MeasurableSet U) (hB : MeasurableSet B) (hBU : B ⊆ U) : (sqWeightedMeasure (U.indicator f) μ) ({x : α | a < ‖U.indicator f x‖} ∩ B) = (sqWeightedMeasure f μ) ({x : α | a < ‖f x‖} ∩ B)

Inside a set contained in U, level tails and their squared weighted mass are exactly those of the unextended function.