Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.ScaleCompression

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

Scalar compression at a good scale

This file records the scale-zero scalar comparisons used to compress the unit-cube moment factors in the variance-bound proof. These are internal Section 5.4 bridges: they are derived from (P4) and the displayed good-scale hypotheses, rather than being added to the public theorem statement.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.barSigmaStarAtScale_le_barSigmaAtScale_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : hP.barSigmaStarAtScale hStruct ↑m ≤ hP.barSigmaAtScale hStruct ↑m

Under (P4), the starred scalar is bounded by the upper scalar at every nonnegative scale.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.barSigmaAtScale_inv_le_one_add_delta_mul_lambdaInvMomentAtScale_zero_of_good {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (m : ℕ) (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) : (hP.barSigmaAtScale hStruct ↑m)⁻¹ ≤ (1 + delta) * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi

Good-scale comparison: the inverse upper normalization at scale m is controlled by the scale-zero lower moment factor.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.barSigmaStarAtScale_le_one_add_delta_mul_LambdaMomentAtScale_zero_of_good {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (m : ℕ) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) : hP.barSigmaStarAtScale hStruct ↑m ≤ (1 + delta) * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi

Good-scale comparison: the starred normalization at scale m is controlled by the scale-zero upper moment factor.