Coarse-graining support: Support.Besov.Localization

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

Localization lemmas for the finite-depth cube Besov package.

This first checkpoint records that the local positive-order quantities attached to a parent cube Q only depend on the function on cubeSet Q. These congruence lemmas are the clean API needed before later descendant-localized and cutoff-localized estimates are added.

theorem HCPolySupport.cubeAverage_congr_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → ℝ} (h : ∀ x ∈ cubeSet Q, u x = v x) : cubeAverage Q u = cubeAverage Q v

theorem HCPolySupport.cubeLpNorm_congr_on_cubeSet {d : ℕ} (Q : TriadicCube d) (p : ENNReal) {u v : Vec d → ℝ} (h : ∀ x ∈ cubeSet Q, u x = v x) : cubeLpNorm Q p u = cubeLpNorm Q p v

theorem HCPolySupport.cubeProjection_congr_on_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) {u v : Vec d → ℝ} (h : ∀ x ∈ cubeSet Q, u x = v x) : cubeProjection Q j u = cubeProjection Q j v

theorem HCPolySupport.cubeProjection_ae_eq_cubeProjection_depth_zero_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (f : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeProjection Q j f =ᵐ[normalizedCubeMeasure R] cubeProjection R 0 f

theorem HCPolySupport.cubeProjection_memLp_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (f : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : MeasureTheory.MemLp (cubeProjection Q j f) p (normalizedCubeMeasure R)

theorem HCPolySupport.cubeProjectionResidual_ae_eq_childDepthZero {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeProjectionResidual Q j u =ᵐ[normalizedCubeMeasure R] cubeProjectionResidual R 0 u

theorem HCPolySupport.cubeLpNorm_cubeProjectionResidual_eq_cubeProjectionResidual_depth_zero_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeLpNorm R p (cubeProjectionResidual Q j u) = cubeLpNorm R p (cubeProjectionResidual R 0 u)

theorem HCPolySupport.cubeProjectionResidual_memLp_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) (hu : MeasureTheory.MemLp (cubeFluctuation R u) p (normalizedCubeMeasure R)) : MeasureTheory.MemLp (cubeProjectionResidual Q j u) p (normalizedCubeMeasure R)

theorem HCPolySupport.abs_cubeAverage_mul_cubeProjectionResidual_le_cubeLpNormBesovOscillation {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (f u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure R)) (hu : MeasureTheory.MemLp (cubeFluctuation R u) p.conjExponent (normalizedCubeMeasure R)) (hp : 1 ≤ p) : |cubeAverage R fun (x : Vec d) => f x * cubeProjectionResidual Q j u x| ≤ cubeLpNorm R p f * cubeBesovOscillation R p.conjExponent u

theorem HCPolySupport.abs_cubeAverage_mul_cubeProjectionResidual_le_cubeBesovOscillation {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (f u : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) (hu : MeasureTheory.MemLp (cubeFluctuation R u) p.conjExponent (normalizedCubeMeasure R)) (hp0 : p ≠ 0) (hp : 1 ≤ p) : |cubeAverage R fun (x : Vec d) => cubeProjection Q j f x * cubeProjectionResidual Q j u x| ≤ ‖cubeAverage R f‖ * cubeBesovOscillation R p.conjExponent u

theorem HCPolySupport.cubeVolume_eq_of_mem_descendantsAtDepth {d : ℕ} {Q R S : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (hS : S ∈ descendantsAtDepth Q j) : cubeVolume R = cubeVolume S

theorem HCPolySupport.cubeVolume_eq_card_mul_cubeVolume_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : cubeVolume Q = ↑(descendantsAtDepth Q j).card * cubeVolume R

theorem HCPolySupport.cubeAverage_eq_descendantsAverage_cubeAverage_of_integrableOn {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) : cubeAverage Q f = descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R f

theorem HCPolySupport.cubeBesovPartialSeminorm_congr_on_cubeSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) {u v : Vec d → ℝ} (h : ∀ x ∈ cubeSet Q, u x = v x) : cubeBesovPartialSeminorm Q s p q N u = cubeBesovPartialSeminorm Q s p q N v

theorem HCPolySupport.cubeBesovPartialNorm_congr_on_cubeSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) {u v : Vec d → ℝ} (h : ∀ x ∈ cubeSet Q, u x = v x) : cubeBesovPartialNorm Q s p q N u = cubeBesovPartialNorm Q s p q N v