Coarse-graining support: Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.Averages

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

Averages

Cube-average algebra used by the first Section 5.3 lemma.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integrable_normalizedCubeMeasure_of_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) : MeasureTheory.Integrable f (normalizedCubeMeasure Q)

Integrability on a cube gives integrability with respect to the normalized cube measure.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_add_of_integrableOn {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume) : (cubeAverage Q fun (x : Vec d) => f x + g x) = cubeAverage Q f + cubeAverage Q g

Linearity of cube averages under cube-set integrability hypotheses.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.ch02_average_cubeDomain_eq_cubeAverage {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : Ch02.average (Ch02.cubeDomain Q) f = cubeAverage Q f

The public Ch2 average on an open cube agrees with cubeAverage.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_sub_const_eq_integral_cutoff_centered_add_integral_one_sub_cutoff_mul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {φ F : α → ℝ} {c : ℝ} (hF_int : MeasureTheory.Integrable F μ) (hφ_int : MeasureTheory.Integrable φ μ) (hCut_int : MeasureTheory.Integrable (fun (x : α) => φ x * (F x - c)) μ) (hRem_int : MeasureTheory.Integrable (fun (x : α) => (1 - φ x) * F x) μ) (hMean : ∫ (x : α), φ x ∂μ = 1) : ∫ (x : α), F x ∂μ - c = ∫ (x : α), φ x * (F x - c) ∂μ + ∫ (x : α), (1 - φ x) * F x ∂μ

Scalar cutoff insertion behind the centered energy splitting.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_sub_const_eq_cubeAverage_cutoff_centered_add_cubeAverage_one_sub_cutoff_mul {d : ℕ} (Q : TriadicCube d) {φ F : Vec d → ℝ} {c : ℝ} (hF_int : MeasureTheory.Integrable F (normalizedCubeMeasure Q)) (hφ_int : MeasureTheory.Integrable φ (normalizedCubeMeasure Q)) (hCut_int : MeasureTheory.Integrable (fun (x : Vec d) => φ x * (F x - c)) (normalizedCubeMeasure Q)) (hRem_int : MeasureTheory.Integrable (fun (x : Vec d) => (1 - φ x) * F x) (normalizedCubeMeasure Q)) (hMean : cubeAverage Q φ = 1) : cubeAverage Q F - c = (cubeAverage Q fun (x : Vec d) => φ x * (F x - c)) + cubeAverage Q fun (x : Vec d) => (1 - φ x) * F x

Cube-average form of mean-one cutoff insertion.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_one_sub_cutoff_mul_eq_cutoff_oscillation_add_mean_defect {d : ℕ} (R : TriadicCube d) (φ F : Vec d → ℝ) (hOsc : MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * F x) (cubeSet R) MeasureTheory.volume) (hF : MeasureTheory.IntegrableOn F (cubeSet R) MeasureTheory.volume) : (cubeAverage R fun (x : Vec d) => (1 - φ x) * F x) = (cubeAverage R fun (x : Vec d) => (cubeAverage R φ - φ x) * F x) + (1 - cubeAverage R φ) * cubeAverage R F

On a child cube, the leftover cutoff factor decomposes as 1 - φ = ((φ)_R - φ) + (1 - (φ)_R).

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_one_sub_cutoff_mul_eq_descendantsAverage_cutoff_oscillation_add_mean_defect {d : ℕ} (Q : TriadicCube d) (j : ℕ) (φ F : Vec d → ℝ) (hRem : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * F x) (cubeSet Q) MeasureTheory.volume) (hOsc : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * F x) (cubeSet R) MeasureTheory.volume) (hF : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn F (cubeSet R) MeasureTheory.volume) : (cubeAverage Q fun (x : Vec d) => (1 - φ x) * F x) = descendantsAverage Q j fun (R : TriadicCube d) => (cubeAverage R fun (x : Vec d) => (cubeAverage R φ - φ x) * F x) + (1 - cubeAverage R φ) * cubeAverage R F

Descendant partition of the leftover cutoff energy term.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.descendantsAverage_congr_of_eq_on_descendants {d : ℕ} (Q : TriadicCube d) (j : ℕ) {F G : TriadicCube d → ℝ} (h : ∀ R ∈ descendantsAtDepth Q j, F R = G R) : descendantsAverage Q j F = descendantsAverage Q j G

Congruence for descendant averages at a fixed depth.