Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.BetaBridge #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Beta bridge between Sections 5.3 and 5.4 #
The current Section 5.3 coarse-fluctuation proof uses half of the Section 5.4 variance exponent. This file keeps that comparison local to the one-step-contraction implementation slice.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.section53CoarseFluctuationBetaCore_eq_section54VarianceBetaCore
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP4 : QuantitativeCoarseGrainedEllipticity P)
:
The Section 5.3 and Section 5.4 beta cores are definitionally the same minimum of manuscript exponent gaps.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.section53CoarseFluctuationBeta_eq_quarter_section54VarianceBeta
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP4 : QuantitativeCoarseGrainedEllipticity P)
:
The current Section 5.3 beta is a fixed fraction of the Section 5.4 variance beta.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.section53CoarseFluctuationBeta_pos
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP4 : QuantitativeCoarseGrainedEllipticity P)
:
The Section 5.3 beta is positive.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.section53CoarseFluctuationBeta_le_section54VarianceBeta
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP4 : QuantitativeCoarseGrainedEllipticity P)
:
The Section 5.3 beta is no larger than the Section 5.4 variance beta.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.varianceWeight_section54VarianceBeta_le_section53CoarseFluctuationBeta
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m j : ℕ)
:
Section 5.4 variance weights are bounded by the slower Section 5.3 coarse-fluctuation weights.