Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.FinalAbsorption

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

Final scalar absorption for the good-scale variance bound

This file finishes the purely deterministic part of the Section 5.4 variance lemma. The analytic work has already reduced the fluctuation estimate to the refined scalar budgets in BudgetAbsorption; here we sum those budgets and absorb the remaining \widetilde\Theta_0 terms with the manuscript scale-separation hypothesis.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_rpow_decay_le {β γ : ℝ} (hgap : 0 < γ - β) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, varianceWeight β m j * Real.rpow 3 (-γ * ↑j) ≤ Real.rpow 3 (-β * ↑m) * (geometricDiscount (γ - β) 1)⁻¹

A beta-weighted finite sum with an additional scale decay gains the top-scale factor 3^{-βm}.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairProbeRefinedDescendantAverageK_eq_geometric {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (delta : ℝ) (j : ℕ) : pairProbeRefinedDescendantAverageK hP4 delta j = 8 * ((1 + delta) * Ch04.widetildeThetaAtScale P 0 hP4.sUpper hP4.sLower hP4.xi) * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * Real.rpow 3 ((↑d / ↑hP4.xi - ↑d) * ↑j) + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * Real.rpow 3 (-(↑d / 2 * ↑j)))

The pair-probe descendant-average budget has the expected two geometric decay components.

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

The L^ξ geometric decay exponent in the refined pair budget.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.lpVarianceDecay d hP4 = ↑d - ↑d / ↑hP4.xi

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sqrtVarianceDecay (d : ℕ) : ℝ

The square-root geometric decay exponent in the refined pair budget.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sqrtVarianceDecay d = ↑d / 2

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

Linear constant for the weighted refined pair budgets.

Equations

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

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

Pointwise constant for the refined pair budget before the extra top-scale decay is summed.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairProbeRefinedDescendantAverageK_le_geometric {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_le_half : delta ≤ 1 / 2) (j : ℕ) : pairProbeRefinedDescendantAverageK hP4 delta j ≤ 16 * widetildeThetaAtScale P 0 hP4 * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * Real.rpow 3 (-lpVarianceDecay d hP4 * ↑j) + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * Real.rpow 3 (-sqrtVarianceDecay d * ↑j))

Pointwise refined pair budgets are controlled by the two geometric decays with the scale-zero moment factor.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairProbeRefinedDescendantAverageK_le_pointwiseConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_le_half : delta ≤ 1 / 2) (j : ℕ) : pairProbeRefinedDescendantAverageK hP4 delta j ≤ pairPointwiseBudgetConst hP4 * widetildeThetaAtScale P 0 hP4

A scale-uniform pointwise bound for refined pair budgets.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.refinedVarianceBasicBudget_le_pairBudget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (j : ℕ) : refinedVarianceBasicBudget hP4 delta j ≤ delta + 2 * pairProbeRefinedDescendantAverageK hP4 delta j + 2 * pairProbeRefinedDescendantAverageK hP4 delta j ^ 2

The compressed scalar budget is controlled by the pair budget.

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

Constant controlling the beta-weighted refined scalar budget before the scale-separation absorption.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.weightedRefinedBudgetConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ weightedRefinedBudgetConst hP4

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_pairProbeRefinedK_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_le_half : delta ≤ 1 / 2) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, varianceWeight (section54VarianceBeta hP4) m j * pairProbeRefinedDescendantAverageK hP4 delta j ≤ pairLinearBudgetConst hP4 * widetildeThetaAtScale P 0 hP4 * Real.rpow 3 (-section54VarianceBeta hP4 * ↑m)

Weighted sum of the refined pair budgets.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_pairProbeRefinedK_sq_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le_half : delta ≤ 1 / 2) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, varianceWeight (section54VarianceBeta hP4) m j * pairProbeRefinedDescendantAverageK hP4 delta j ^ 2 ≤ pairPointwiseBudgetConst hP4 * pairLinearBudgetConst hP4 * widetildeThetaAtScale P 0 hP4 ^ 2 * Real.rpow 3 (-section54VarianceBeta hP4 * ↑m)

Weighted sum of the squares of the refined pair budgets.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.sum_Icc_varianceWeight_mul_refinedVarianceBasicBudget_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, varianceWeight (section54VarianceBeta hP4) m j * refinedVarianceBasicBudget hP4 delta j ≤ weightedRefinedBudgetConst hP4 * (delta + Real.rpow 3 (-section54VarianceBeta hP4 * ↑m) * (widetildeThetaAtScale P 0 hP4 + widetildeThetaAtScale P 0 hP4 ^ 2))

The full weighted refined scalar budget has only the manuscript-size terms δ and 3^{-βm}(\widetilde\Theta_0+\widetilde\Theta_0^2).