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

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

FiveTermSplit

Deterministic five-term splitting of the centered response.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredResponseJOnCube_eq_cutoffProduct_add_cutoffOscillation_add_meanDefect_add_linearPair {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (j : ℕ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (hTop_int : MeasureTheory.IntegrableOn (topHalfEnergyDensityOnCube Q a p q) (cubeSet Q) MeasureTheory.volume) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q a p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q a p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q a p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q a p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hOsc_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q a p q x) (cubeSet R) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) : centeredResponseJOnCube Q a p q p0 q0 = cutoffProductTermOnCube Q a φ p q p0 q0 + cutoffOscillationTermOnCubeAtDepth Q a j φ p q + meanDefectTopEnergyTermOnCubeAtDepth Q a j φ p q + cutoffLinearPairTermOnCube Q a φ p q p0 q0

Cutoff insertion and descendant partition for the parent centered response, before the mean-defect term is rewritten using child energies.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.meanDefectTopEnergyTermOnCubeAtDepth_eq_additivityCross_add_cutoffWeightedChildResponseJ {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q : Vec d) (cross : TriadicCube d → ℝ) (hChildEnergy : ∀ R ∈ descendantsAtDepth Q j, cubeAverage R (topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q) = cross R + Ch02.responseJ (Ch02.cubeDomain R) (a.coeffOn R) p q) : meanDefectTopEnergyTermOnCubeAtDepth Q (a.coeffOn Q) j φ p q = additivityCrossTermOnCubeAtDepth Q j φ cross + cutoffWeightedChildResponseJOnFamilyAtDepth a Q j φ p q

The parent-energy mean-defect term becomes additivity-cross plus the cutoff-weighted child response once child energy has been identified.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJDifference_eq_additivityCross_cutoffOscillation_linearPair_product {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (cross : TriadicCube d → ℝ) (hTop_int : MeasureTheory.IntegrableOn (topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q) (cubeSet Q) MeasureTheory.volume) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q (a.coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q (a.coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q (a.coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hOsc_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q x) (cubeSet R) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) (hChildEnergy : ∀ R ∈ descendantsAtDepth Q j, cubeAverage R (topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q) = cross R + Ch02.responseJ (Ch02.cubeDomain R) (a.coeffOn R) p q) : centeredResponseJOnCube Q (a.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth a Q j φ p q = additivityCrossTermOnCubeAtDepth Q j φ cross + cutoffOscillationTermOnCubeAtDepth Q (a.coeffOn Q) j φ p q + cutoffLinearPairTermOnCube Q (a.coeffOn Q) φ p q p0 q0 + cutoffProductTermOnCube Q (a.coeffOn Q) φ p q p0 q0

Deterministic analytic core of the first Section 5.3 lemma: the centered parent response minus the cutoff-weighted child response splits into the additivity cross term, cutoff oscillation, linear terms, and product term.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJDifference_eq_concreteCross_cutoffOscillation_linearPair_product {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (hTop_int : MeasureTheory.IntegrableOn (topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q) (cubeSet Q) MeasureTheory.volume) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q (a.coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q (a.coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q (a.coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hOsc_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q x) (cubeSet R) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) (hCoeff : ∀ R ∈ descendantsAtDepth Q j, (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) : centeredResponseJOnCube Q (a.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth a Q j φ p q = concreteAdditivityCrossTermOnFamilyAtDepth a Q j φ p q + cutoffOscillationTermOnCubeAtDepth Q (a.coeffOn Q) j φ p q + cutoffLinearPairTermOnCube Q (a.coeffOn Q) φ p q p0 q0 + cutoffProductTermOnCube Q (a.coeffOn Q) φ p q p0 q0

Concrete deterministic analytic core, with the child-energy equality discharged by the explicit additivity-cross density.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJDifference_eq_concreteCross_cutoffOscillation_linearPair_of_linearPair {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hOsc_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet R) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; centeredResponseJOnCube Q (F.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth F Q j φ p q = concreteAdditivityCrossTermOnFamilyAtDepth F Q j φ p q + cutoffOscillationTermOnCubeAtDepth Q (F.coeffOn Q) j φ p q + cutoffLinearPairTermOnCube Q (F.coeffOn Q) φ p q p0 q0 + cutoffProductTermOnCube Q (F.coeffOn Q) φ p q p0 q0

Concrete deterministic analytic core for the Chapter 4 dependent coefficient family. Here the parent and child representatives are definitionally the sampled coefficient field, so no representative-equality hypothesis remains.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_responseJDifference_le_additivityError_cutoffOscillation_pair_product {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) {C : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hOsc_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet R) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; |centeredResponseJOnCube Q (F.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth F Q j φ p q| ≤ 2 * C * (√(responseJPartitionDefectOnFamilyAtDepth F Q j p q) * √(childResponseJAverageOnFamilyAtDepth F Q j p q)) + |cutoffOscillationTermOnCubeAtDepth Q (F.coeffOn Q) j φ p q| + |cutoffLinearPairTermOnCube Q (F.coeffOn Q) φ p q p0 q0| + |cutoffProductTermOnCube Q (F.coeffOn Q) φ p q p0 q0|

Deterministic assembled Section 5.3 estimate after the five-term split: the additivity-cross term is in the manuscript response-partition-defect form, while the cutoff oscillation, linear pair, and product terms remain as the separate deterministic terms estimated elsewhere.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJOnDependentFamily_eq_restrictionResponseJObservableCubeSet {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (p q : Vec d) : Ch02.responseJ (Ch02.cubeDomain Q) ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q = Ch04.restrictionResponseJObservableCubeSet Q p q a

Raw Ch2 response for the Chapter 4 dependent coefficient family is the Ch4 cube-set response observable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnDependentFamilyAtScale_eq_responseJAdditivityDefectAtScale {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m k : ℤ) (p q : Vec d) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; responseJPartitionDefectOnFamilyAtDepth F (originCube d m) (m - k).toNat p q = responseJAdditivityDefectAtScale m k p q a

At origin scales, the deterministic response partition defect for the Ch4 dependent family is the Ch4 additivity-defect observable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredResponseJOnDependentFamily_eq_restrictionCenteredResponseJObservableCubeSet {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (p q p0 q0 : Vec d) : centeredResponseJOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 = Ch04.restrictionCenteredResponseJObservableCubeSet Q p q p0 q0 a

Centered raw Ch2 response for the Chapter 4 dependent family is the Ch4 centered response observable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffWeightedChildResponseJOnDependentFamilyAtDepth_eq_ch04 {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q : Vec d) : cutoffWeightedChildResponseJOnFamilyAtDepth (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) Q j φ p q = descendantsAverage Q j fun (R : TriadicCube d) => cutoffChildWeight φ R * Ch04.restrictionResponseJObservableCubeSet R p q a

The deterministic child-weighted raw Ch2 response average agrees with the Ch4 response-observable average.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredResponseJOnDependentFamily_sub_cutoffWeightedChildResponseJ_eq_ch04 {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) : centeredResponseJOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) Q j φ p q = Ch04.restrictionCenteredResponseJObservableCubeSet Q p q p0 q0 a - descendantsAverage Q j fun (R : TriadicCube d) => cutoffChildWeight φ R * Ch04.restrictionResponseJObservableCubeSet R p q a

Pointwise bridge from the deterministic raw split left side to the Ch4 centered-minus-child expression used before taking expectations.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredJMinusCutoffWeightedChildAtScale_eq_dependentFamily_left {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m k : ℤ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) : centeredJMinusCutoffWeightedChildAtScale m k φ p q p0 q0 a = centeredResponseJOnCube (originCube d m) ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn (originCube d m)) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (originCube d m) (m - k).toNat φ p q

Origin-scale version of the raw/Ch4 left-side bridge, matching the private stochastic expression used above.