Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.ScalarLoss

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

Uniform scalar losses for the third Section 5.3 lemma

This file isolates the purely scalar estimates that keep the Section 5.3 coarse-fluctuation constant independent of the scale parameters. In particular, it bounds the corrected Section 5.2 two-exponent loss at the β-shifted exponents by the manuscript ξ β^{-3} factor.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_inv_le_xi_of_sUpper {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : hP4.sUpper⁻¹ ≤ ↑hP4.xi

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta_inv_le_xi_of_sLower {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : hP4.sLower⁻¹ ≤ ↑hP4.xi

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section52MomentLossCoeff_upper_beta_shift_le_xi_beta_cubed {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : have β := section53CoarseFluctuationBeta hP4; section52MomentLossCoeff d hP4.xi hP4.sUpper (hP4.sUpper + β) ≤ 2 * ↑hP4.xi * (β ^ 3)⁻¹

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section52MomentLossCoeff_lower_beta_shift_le_xi_beta_cubed {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : have β := section53CoarseFluctuationBeta hP4; section52MomentLossCoeff d hP4.xi hP4.sLower (hP4.sLower + β) ≤ 2 * ↑hP4.xi * (β ^ 3)⁻¹

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section52MomentLossCoeff_upper_two_beta_shift_le_xi_beta_cubed {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : have β := section53CoarseFluctuationBeta hP4; section52MomentLossCoeff d hP4.xi (hP4.sUpper + β) (hP4.sUpper + 2 * β) ≤ 2 * ↑hP4.xi * (β ^ 3)⁻¹

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.section52MomentLossCoeff_lower_two_beta_shift_le_xi_beta_cubed {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : have β := section53CoarseFluctuationBeta hP4; section52MomentLossCoeff d hP4.xi (hP4.sLower + β) (hP4.sLower + 2 * β) ≤ 2 * ↑hP4.xi * (β ^ 3)⁻¹