Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.Basic

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

Basic definitions for the one-step contraction

This file contains only the scalar abbreviations used by the Section 5.4 one-step contraction proof. The theorem-facing statement remains in the final assembly file.

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContractionEpsilon (delta : ℝ) : ℝ

The internal manuscript choice epsilon = delta^(1/4).

Equations

• HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepContractionEpsilon delta = delta.rpow (1 / 4)

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScalarWeightAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℕ) : ℝ

The scalar coefficient combination multiplying the additivity-defect sum in the Section 5.3 coarse-fluctuation estimate.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScalarWeightAtScale_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℕ) : oneStepScalarWeightAtScale hP hStruct m = sigmaHatAtScale hP hStruct ↑m * (hP.barSigmaStarAtScale hStruct 0)⁻¹ + (sigmaHatAtScale hP hStruct ↑m)⁻¹ * hP.barSigmaAtScale hStruct 0

The one-step scalar weight is the sum of the two good-scale scalar comparisons used in the manuscript proof.