Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.WeightedChildren

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

WeightedChildren

Weighted child response observables and stationarity cancellations.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_weightedChildResponseJ_eq_zero_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) (weight : TriadicCube d → ℝ) (p q : Vec d) (hweight : descendantsAverage (originCube d m) (m - k).toNat weight = 0) (hJ : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), descendantsAverage (originCube d m) (m - k).toNat fun (R : TriadicCube d) => weight R * Ch04.restrictionResponseJObservableCubeSet R p q a ∂P = 0

Private Section 5.3 stationarity cancellation for weighted child responses.

The manuscript later supplies weight R = 1 - (phi)_R; the only stochastic input here is the Ch4 source theorem for weighted descendant response expectations.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffChildWeight {d : ℕ} (φ : Vec d → ℝ) (R : TriadicCube d) : ℝ

Manuscript cutoff child weight 1 - (phi)_R. This is deterministic; measurability and stationarity enter only through the response observable that it weights.

Equations

• HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffChildWeight φ R = 1 - HCPolySupport.cubeAverage R φ

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.descendantsAverage_cutoffChildWeight_eq_zero_of_cubeAverage_eq_one {d : ℕ} (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) : (descendantsAverage Q j fun (R : TriadicCube d) => cutoffChildWeight φ R) = 0

If the cutoff has parent average one, then the finite average of the child weights 1 - (phi)_R is zero.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffWeightedChildResponseJAtScale {d : ℕ} (m k : ℤ) (φ : Vec d → ℝ) (p q : Vec d) : RegCoeffField d → ℝ

Cutoff-weighted child response average from the manuscript splitting.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integrable_cutoffWeightedChildResponseJAtScale {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {k m : ℤ} (hkm : k ≤ m) (φ : Vec d → ℝ) (p q : Vec d) (hJ : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : MeasureTheory.Integrable (cutoffWeightedChildResponseJAtScale m k φ p q) P

Childwise response integrability makes the cutoff-weighted child average integrable. The cutoff weights are deterministic scalars.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_cutoffWeightedChildResponseJAtScale_eq_zero_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) (φ : Vec d → ℝ) (p q : Vec d) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet (originCube d m)) MeasureTheory.volume) (hMean : cubeAverage (originCube d m) φ = 1) (hJ : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), cutoffWeightedChildResponseJAtScale m k φ p q a ∂P = 0

The manuscript cutoff-weighted child response has zero expectation under stationarity once the cutoff is normalized to have parent average one.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredResponseJAtScale {d : ℕ} (m : ℤ) (p q p0 q0 : Vec d) : RegCoeffField d → ℝ

Parent centered response in the Section 5.3 notation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredJMinusCutoffWeightedChildAtScale {d : ℕ} (m k : ℤ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) : RegCoeffField d → ℝ

The centered parent response minus the cutoff-weighted child response average. This is the stochastic side of the manuscript's centered splitting.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_centeredJMinusCutoffWeightedChildAtScale_eq_expectedResponseJCubeSet_sub_half_dot {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet (originCube d m)) MeasureTheory.volume) (hMean : cubeAverage (originCube d m) φ = 1) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hJ : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), centeredJMinusCutoffWeightedChildAtScale m k φ p q p0 q0 a ∂P = Ch04.expectedResponseJCubeSet P (originCube d m) p q - 1 / 2 * vecDot p0 q0

The expectation of the centered splitting term is just the centered parent expectation: the cutoff-weighted child contribution cancels by stationarity and normalization.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJAdditivityDefectAtScale {d : ℕ} (m k : ℤ) (p q : Vec d) : RegCoeffField d → ℝ

Private additivity-defect observable from the manuscript proof: child-scale average of J minus parent-scale J.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_responseJAdditivityDefectAtScale_eq_tauAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) (p q : Vec d) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDesc : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), responseJAdditivityDefectAtScale m k p q a ∂P = tauAtScale P m k p q

The additivity-defect observable has expectation tau_{m,k} under stationarity. This is the stochastic identity used in the square-root Cauchy step of Lemma l.J.upper.bound.weak.norms.homogenization.scale.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_le_integral_of_ae_abs_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {X Y : α → ℝ} (hX : MeasureTheory.Integrable X μ) (hY : MeasureTheory.Integrable Y μ) (hXY : ∀ᵐ (a : α) ∂μ, |X a| ≤ Y a) : ∫ (a : α), X a ∂μ ≤ ∫ (a : α), Y a ∂μ

If a scalar observable is a.e. bounded in absolute value by an integrable right-hand side, then its expectation is bounded by the expectation of that right-hand side.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_centeredJMinusCutoffWeightedChildAtScale_le_integral_of_ae_abs_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (RHS : RegCoeffField d → ℝ) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet (originCube d m)) MeasureTheory.volume) (hMean : cubeAverage (originCube d m) φ = 1) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hJ : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) (hRHS : MeasureTheory.Integrable RHS P) (hBound : ∀ᵐ (a : RegCoeffField d) ∂P, |centeredJMinusCutoffWeightedChildAtScale m k φ p q p0 q0 a| ≤ RHS a) : Ch04.expectedResponseJCubeSet P (originCube d m) p q - 1 / 2 * vecDot p0 q0 ≤ ∫ (a : RegCoeffField d), RHS a ∂P

Expectation assembly for the centered-minus-child split: stationarity turns the left side into the centered parent expectation, and an a.e. deterministic absolute-value bound controls it by the expectation of any integrable RHS.