Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.AdditivityDefects

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

Response-defect expectation conversion

This file contains the proof-internal expectation conversion for the response-defect baseline sums in the third Section 5.3 lemma.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integrable_sq_weighted_sqrt_responseDefectAverageAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (w : ℤ → ℝ) (p q : Vec d) (hw : ∀ n ∈ Finset.Icc (k + 1) m, 0 ≤ w n) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDesc : ∀ n ∈ Finset.Icc (k + 1) m, ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (∑ n ∈ Finset.Icc (k + 1) m, w n * √(WeakNormsMaximizer.responseDefectAverageAtScale m n p q a)) ^ 2) P

Integrability of the square of a finite weighted response-defect square-root sum. This is the integrability part of the Cauchy/tau estimate below, exposed proof-internally for the final paired-square assembly.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_sq_weighted_sqrt_responseDefectAverageAtScale_le_sum_weights_mul_tauAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (w : ℤ → ℝ) (p q : Vec d) (hw : ∀ n ∈ Finset.Icc (k + 1) m, 0 ≤ w n) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDesc : ∀ n ∈ Finset.Icc (k + 1) m, ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), (∑ n ∈ Finset.Icc (k + 1) m, w n * √(WeakNormsMaximizer.responseDefectAverageAtScale m n p q a)) ^ 2 ∂P ≤ (∑ n ∈ Finset.Icc (k + 1) m, w n) * ∑ n ∈ Finset.Icc (k + 1) m, w n * tauAtScale P m n p q

Finite weighted Cauchy plus stationarity converts the square of a weighted sum of response-defect square roots into the corresponding weighted tau sum.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_sq_beta_weighted_sqrt_responseDefectAverageAtScale_le_geometric_tauSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) {β : ℝ} (hβ : 0 < β) (p q : Vec d) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDesc : ∀ n ∈ Finset.Icc (k + 1) m, ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), (∑ n ∈ Finset.Icc (k + 1) m, Real.rpow 3 (-β * ↑(m - n).toNat) * √(WeakNormsMaximizer.responseDefectAverageAtScale m n p q a)) ^ 2 ∂P ≤ (1 - Real.rpow 3 (-β))⁻¹ * ∑ n ∈ Finset.Icc (k + 1) m, Real.rpow 3 (-β * ↑(m - n).toNat) * tauAtScale P m n p q

The beta-weighted response-defect baseline term is bounded by the geometric series factor times the beta-weighted tau sum.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_sq_beta_weighted_sqrt_responseDefectAverageAtScale_le_beta_inv_tauSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) {β : ℝ} (hβ : 0 < β) (hβ_le : β ≤ 1) (p q : Vec d) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDesc : ∀ n ∈ Finset.Icc (k + 1) m, ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), (∑ n ∈ Finset.Icc (k + 1) m, Real.rpow 3 (-β * ↑(m - n).toNat) * √(WeakNormsMaximizer.responseDefectAverageAtScale m n p q a)) ^ 2 ∂P ≤ 5 * β⁻¹ * ∑ n ∈ Finset.Icc (k + 1) m, Real.rpow 3 (-β * ↑(m - n).toNat) * tauAtScale P m n p q

The beta-weighted response-defect baseline term with the geometric factor absorbed into the standard 5 * beta^{-1} loss.