Coarse-graining support: Support.Book.Ch05.Theorems.Section52.WidetildeTheta

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

Section 5.2 internals: WidetildeTheta

Widetilde-theta product consequences.

theorem HCPolySupport.Book.Ch05.Section52.widetildeThetaAtScale_le_thetaAtScale_zero_add_positiveExcess_products_of_integrable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hBlock : ∀ (l : ℕ), MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d ↑l)) P) (hUpperPowInt : ∀ (l : ℕ), MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d ↑l) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a ^ hP4.xi) P) (hLowerPowInt : ∀ (l : ℕ), MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d ↑l) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ hP4.xi) P) (m : ℕ) (hUpperExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d ↑m) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 ^ hP4.xi) P) (hLowerExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d ↑m) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 ^ hP4.xi) P) : widetildeThetaAtScale P (↑m) hP4 ≤ thetaAtScale hP hStruct 0 + LambdaPositiveExcessMomentAtScale P (↑m) hP4.sUpper hP4.xi hP hStruct * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi + lambdaInvPositiveExcessMomentAtScale P (↑m) hP4.sLower hP4.xi hP hStruct * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + LambdaPositiveExcessMomentAtScale P (↑m) hP4.sUpper hP4.xi hP hStruct * lambdaInvPositiveExcessMomentAtScale P (↑m) hP4.sLower hP4.xi hP hStruct

Product assembly for the Section 5.2 moment lemma, with the scalar Minkowski decomposition and the unit-scale base comparisons proved from the Chapter 4 law-facing surfaces.

The remaining analytic inputs are exactly the two positive-excess power integrability facts; the quantitative bounds on those positive-excess roots are the genuine partition-average fluctuation step.

theorem HCPolySupport.Book.Ch05.Section52.widetildeThetaAtScale_le_thetaAtScale_zero_add_error_of_integrable_positiveExcess_bounds {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hBlock : ∀ (l : ℕ), MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d ↑l)) P) (hUpperPowInt : ∀ (l : ℕ), MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d ↑l) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a ^ hP4.xi) P) (hLowerPowInt : ∀ (l : ℕ), MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d ↑l) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ hP4.xi) P) (m : ℕ) (hUpperExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d ↑m) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 ^ hP4.xi) P) (hLowerExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d ↑m) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 ^ hP4.xi) P) {coeffUpper coeffLower finalCoeff : ℝ} (hCoeffUpper_nonneg : 0 ≤ coeffUpper) (hCoeffLower_nonneg : 0 ≤ coeffLower) (hUpperExcess : LambdaPositiveExcessMomentAtScale P (↑m) hP4.sUpper hP4.xi hP hStruct ≤ coeffUpper * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi) (hLowerExcess : lambdaInvPositiveExcessMomentAtScale P (↑m) hP4.sLower hP4.xi hP hStruct ≤ coeffLower * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi) (hCoeff : coeffUpper + coeffLower + coeffUpper * coeffLower ≤ finalCoeff) : widetildeThetaAtScale P (↑m) hP4 ≤ thetaAtScale hP hStruct 0 + finalCoeff * widetildeThetaAtScale P 0 hP4

The widetildeTheta consequence of the Section 5.2 moment lemma from quantitative positive-excess estimates, with all scalar root decomposition and unit-scale factor comparisons discharged from the Chapter 4 surfaces.

theorem HCPolySupport.Book.Ch05.Section52.widetildeThetaAtScale_le_thetaAtScale_zero_add_section52_error_of_integrable_positiveExcess_bounds {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hBlock : ∀ (l : ℕ), MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d ↑l)) P) (hUpperPowInt : ∀ (l : ℕ), MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d ↑l) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a ^ hP4.xi) P) (hLowerPowInt : ∀ (l : ℕ), MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d ↑l) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ hP4.xi) P) (m : ℕ) (hUpperExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d ↑m) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 ^ hP4.xi) P) (hLowerExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d ↑m) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 ^ hP4.xi) P) {CUpper CLower CTheta : ℝ} (hCUpper_nonneg : 0 ≤ CUpper) (hCLower_nonneg : 0 ≤ CLower) (hUpperExcess : LambdaPositiveExcessMomentAtScale P (↑m) hP4.sUpper hP4.xi hP hStruct ≤ section52MomentBoundCoeff d hP4.xi CUpper hP4.sUpper m * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi) (hLowerExcess : lambdaInvPositiveExcessMomentAtScale P (↑m) hP4.sLower hP4.xi hP hStruct ≤ section52MomentBoundCoeff d hP4.xi CLower hP4.sLower m * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi) (hCTheta : CUpper / (↑d / 2 + ↑d / ↑hP4.xi - hP4.sUpper) + CLower / (↑d / 2 + ↑d / ↑hP4.xi - hP4.sLower) + CUpper / (↑d / 2 + ↑d / ↑hP4.xi - hP4.sUpper) * (CLower / (↑d / 2 + ↑d / ↑hP4.xi - hP4.sLower)) ≤ CTheta) : widetildeThetaAtScale P (↑m) hP4 ≤ thetaAtScale hP hStruct 0 + section52WidetildeThetaErrorCoeff d hP4.xi CTheta (min hP4.sUpper hP4.sLower) m * widetildeThetaAtScale P 0 hP4

The displayed Section 5.2 widetildeTheta estimate from the two positive-excess estimates with their manuscript coefficients. The probabilistic content is exactly the two positive-excess bounds supplied as hypotheses.