Coarse-graining support: Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale

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

Variance bound at a good scale

This file exposes the LaTeX-facing Section 5.4 variance lemma. The proof assembles the refined finite-probe estimate, the deterministic budget summation, and the logarithmic scale-separation absorption.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceBoundGoodScaleConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : ℝ

Final constant used in the good-scale variance bound.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBetaCoreParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the Section 5.4 variance beta core.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBetaParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the Section 5.4 variance beta.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBetaParams params = HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBetaCoreParams params / 2

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceScaleSeparationConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the variance scale-separation constant.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.lpVarianceDecayParams (d : ℕ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the L^ξ geometric decay exponent.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.lpVarianceDecayParams d params = ↑d - ↑d / ↑params.xi

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairLinearBudgetConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the linear weighted pair-budget constant.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairPointwiseBudgetConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the pointwise pair-budget constant.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.weightedRefinedBudgetConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the weighted refined budget constant.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceBoundGoodScaleConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only final constant for the good-scale variance bound.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBetaCoreParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : section54VarianceBetaCoreParams hP4.params = section54VarianceBetaCore hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.section54VarianceBetaParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : section54VarianceBetaParams hP4.params = section54VarianceBeta hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceScaleSeparationConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : varianceScaleSeparationConstParams hP4.params = varianceScaleSeparationConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.lpVarianceDecayParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : lpVarianceDecayParams d hP4.params = lpVarianceDecay d hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairLinearBudgetConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : pairLinearBudgetConstParams hP4.params = pairLinearBudgetConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairPointwiseBudgetConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : pairPointwiseBudgetConstParams hP4.params = pairPointwiseBudgetConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.weightedRefinedBudgetConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : weightedRefinedBudgetConstParams hP4.params = weightedRefinedBudgetConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceBoundGoodScaleConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : varianceBoundGoodScaleConstParams hP4.params = varianceBoundGoodScaleConst hP4

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceBoundGoodScale_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {delta : ℝ}, 0 < delta → delta ≤ 1 / 2 → ∀ {m : ℕ}, C * ↑params.xi * Real.log (2 + delta⁻¹ * ↑params.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m → hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m → (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ → varianceGoodScaleFullBlockSumAtScale hP hStruct hP4 m ≤ C * √delta

Section 5.4, variance bound at a good scale.