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

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

Section 5.2 internals: MomentBounds

Final positive-excess and multiscale ellipticity moment bounds.

theorem HCPolySupport.Book.Ch05.Section52.section52_annealedMomentRoot_positiveExcess_le_finset_sum {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ι : Type u_1} {ξ : ℕ} {s : Finset ι} {X : RegCoeffField d → ℝ} {base : ℝ} {G : ι → RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hG_nonneg : ∀ i ∈ s, ∀ (a : RegCoeffField d), 0 ≤ G i a) (hG_aemeas : ∀ i ∈ s, AEMeasurable (G i) P) (hG_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G i a| ^ ξ) P) (hExcess_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |max (X a - base) 0| ^ ξ) P) (hPoint : ∀ᵐ (a : RegCoeffField d) ∂P, max (X a - base) 0 ≤ ∑ i ∈ s, G i a) : (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => max (X a - base) 0) ≤ ∑ i ∈ s, Ch04.annealedMomentRoot P ξ (G i)

theorem HCPolySupport.Book.Ch05.Section52.section52_annealedMomentRoot_positiveExcess_le_scaled_initial {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ι : Type u_1} {ξ : ℕ} {s : Finset ι} {X : RegCoeffField d → ℝ} {base initial finalCoeff : ℝ} {G : ι → RegCoeffField d → ℝ} {coeff : ι → ℝ} (hξ : 1 ≤ ξ) (hInitial_nonneg : 0 ≤ initial) (hG_nonneg : ∀ i ∈ s, ∀ (a : RegCoeffField d), 0 ≤ G i a) (hG_aemeas : ∀ i ∈ s, AEMeasurable (G i) P) (hG_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G i a| ^ ξ) P) (hExcess_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |max (X a - base) 0| ^ ξ) P) (hPoint : ∀ᵐ (a : RegCoeffField d) ∂P, max (X a - base) 0 ≤ ∑ i ∈ s, G i a) (hRoot : ∀ i ∈ s, Ch04.annealedMomentRoot P ξ (G i) ≤ coeff i * initial) (hCoeffSum : ∑ i ∈ s, coeff i ≤ finalCoeff) : (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => max (X a - base) 0) ≤ finalCoeff * initial

theorem HCPolySupport.Book.Ch05.Section52.section52_integrable_positiveExcess_pow_of_one_add_finset_bound {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ι : Type u_1} {ξ : ℕ} {s : Finset ι} {X : RegCoeffField d → ℝ} {base : ℝ} {G0 : RegCoeffField d → ℝ} {G : ι → RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hG0_nonneg : ∀ (a : RegCoeffField d), 0 ≤ G0 a) (hG_nonneg : ∀ i ∈ s, ∀ (a : RegCoeffField d), 0 ≤ G i a) (hG0_aemeas : AEMeasurable G0 P) (hG_aemeas : ∀ i ∈ s, AEMeasurable (G i) P) (hG0_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G0 a| ^ ξ) P) (hG_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G i a| ^ ξ) P) (hX_aemeas : AEMeasurable X P) (hPoint : ∀ᵐ (a : RegCoeffField d) ∂P, max (X a - base) 0 ≤ G0 a + ∑ i ∈ s, G i a) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (X a - base) 0 ^ ξ) P

theorem HCPolySupport.Book.Ch05.Section52.section52_annealedMomentRoot_positiveExcess_le_one_add_finset_scaled {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {ι : Type u_1} {ξ : ℕ} {s : Finset ι} {X : RegCoeffField d → ℝ} {base initial finalCoeff coeff0 : ℝ} {G0 : RegCoeffField d → ℝ} {G : ι → RegCoeffField d → ℝ} {coeff : ι → ℝ} (hξ : 1 ≤ ξ) (hInitial_nonneg : 0 ≤ initial) (hG0_nonneg : ∀ (a : RegCoeffField d), 0 ≤ G0 a) (hG_nonneg : ∀ i ∈ s, ∀ (a : RegCoeffField d), 0 ≤ G i a) (hG0_aemeas : AEMeasurable G0 P) (hG_aemeas : ∀ i ∈ s, AEMeasurable (G i) P) (hG0_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G0 a| ^ ξ) P) (hG_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G i a| ^ ξ) P) (hX_aemeas : AEMeasurable X P) (hPoint : ∀ᵐ (a : RegCoeffField d) ∂P, max (X a - base) 0 ≤ G0 a + ∑ i ∈ s, G i a) (hRoot0 : Ch04.annealedMomentRoot P ξ G0 ≤ coeff0 * initial) (hRoot : ∀ i ∈ s, Ch04.annealedMomentRoot P ξ (G i) ≤ coeff i * initial) (hCoeffSum : coeff0 + ∑ i ∈ s, coeff i ≤ finalCoeff) : (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => max (X a - base) 0) ≤ finalCoeff * initial

theorem HCPolySupport.Book.Ch05.Section52.upperPositiveExcessMomentAtScale_integrable_and_le_raw_twoExponentCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s r : ℝ} {ξ m : ℕ} (hs : 0 < s) (hsr : s < r) (hr_lt_one : r < 1) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hBlock0 : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d 0)) P) (hUpperSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) : have D := descendantsAtScale (originCube d ↑m) 0; MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d ↑m) r (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 ^ ξ) P ∧ LambdaPositiveExcessMomentAtScale P (↑m) r ξ hP hStruct ≤ ((25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m)) ^ 2 / section52SmallTailWeight r m * ↑D.card ^ (1 / ↑ξ) + ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleRootCoeff d ξ r m n) * Ch04.LambdaMomentAtScale P 0 s ξ

theorem HCPolySupport.Book.Ch05.Section52.upperPositiveExcessMomentAtScale_le_raw_twoExponentCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s r : ℝ} {ξ m : ℕ} (hs : 0 < s) (hsr : s < r) (hr_lt_one : r < 1) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hBlock0 : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d 0)) P) (hUpperSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) : have D := descendantsAtScale (originCube d ↑m) 0; LambdaPositiveExcessMomentAtScale P (↑m) r ξ hP hStruct ≤ ((25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m)) ^ 2 / section52SmallTailWeight r m * ↑D.card ^ (1 / ↑ξ) + ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleRootCoeff d ξ r m n) * Ch04.LambdaMomentAtScale P 0 s ξ

theorem HCPolySupport.Book.Ch05.Section52.lowerPositiveExcessMomentAtScale_integrable_and_le_raw_twoExponentCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s r : ℝ} {ξ m : ℕ} (hs : 0 < s) (hsr : s < r) (hr_lt_one : r < 1) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hBlock0 : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d 0)) P) (hLowerSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) : have D := descendantsAtScale (originCube d ↑m) 0; MeasureTheory.Integrable (fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d ↑m) r (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 ^ ξ) P ∧ lambdaInvPositiveExcessMomentAtScale P (↑m) r ξ hP hStruct ≤ ((25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m)) ^ 2 / section52SmallTailWeight r m * ↑D.card ^ (1 / ↑ξ) + ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleRootCoeff d ξ r m n) * Ch04.lambdaInvMomentAtScale P 0 s ξ

theorem HCPolySupport.Book.Ch05.Section52.lowerPositiveExcessMomentAtScale_le_raw_twoExponentCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s r : ℝ} {ξ m : ℕ} (hs : 0 < s) (hsr : s < r) (hr_lt_one : r < 1) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hBlock0 : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d 0)) P) (hLowerSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) : have D := descendantsAtScale (originCube d ↑m) 0; lambdaInvPositiveExcessMomentAtScale P (↑m) r ξ hP hStruct ≤ ((25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m)) ^ 2 / section52SmallTailWeight r m * ↑D.card ^ (1 / ↑ξ) + ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleRootCoeff d ξ r m n) * Ch04.lambdaInvMomentAtScale P 0 s ξ

theorem HCPolySupport.Book.Ch05.Section52.LambdaPositiveExcessMomentAtScale_le_twoExponentMomentBoundCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s r : ℝ} {ξ m : ℕ} (hs : 0 < s) (hsr : s < r) (hr_lt_one : r < 1) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hlargeGap : 0 < ↑d / 2 + ↑d / ↑ξ - r) (hBlock0 : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d 0)) P) (hUpperSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) : LambdaPositiveExcessMomentAtScale P (↑m) r ξ hP hStruct ≤ section52TwoExponentMomentBoundCoeff d ξ (625 + section52LargeScalarAbsorptionConst d) s r m * Ch04.LambdaMomentAtScale P 0 s ξ

Upper positive-excess estimate in the corrected two-exponent Section 5.2 moment lemma. The source exponent is s; the scale-m target exponent is r.

theorem HCPolySupport.Book.Ch05.Section52.lambdaInvPositiveExcessMomentAtScale_le_twoExponentMomentBoundCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s r : ℝ} {ξ m : ℕ} (hs : 0 < s) (hsr : s < r) (hr_lt_one : r < 1) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hlargeGap : 0 < ↑d / 2 + ↑d / ↑ξ - r) (hBlock0 : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d 0)) P) (hLowerSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) : lambdaInvPositiveExcessMomentAtScale P (↑m) r ξ hP hStruct ≤ section52TwoExponentMomentBoundCoeff d ξ (625 + section52LargeScalarAbsorptionConst d) s r m * Ch04.lambdaInvMomentAtScale P 0 s ξ

Lower inverse positive-excess estimate in the corrected two-exponent Section 5.2 moment lemma.

theorem HCPolySupport.Book.Ch05.Section52.upperPositiveExcessPowIntegrableAtScale_from_P4_twoExponent {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {rUpper : ℝ} (hrUpper_gt : hP4.sUpper < rUpper) (hrUpper_lt_one : rUpper < 1) (m : ℕ) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d ↑m) rUpper (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 ^ hP4.xi) P

The shifted upper positive excess appearing in Section 5.3 is integrable under (P4). This extracts the integrability already used inside the Section 5.2 two-exponent moment estimate.

theorem HCPolySupport.Book.Ch05.Section52.lowerPositiveExcessPowIntegrableAtScale_from_P4_twoExponent {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {rLower : ℝ} (hrLower_gt : hP4.sLower < rLower) (hrLower_lt_one : rLower < 1) (m : ℕ) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d ↑m) rLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 ^ hP4.xi) P

The shifted lower inverse positive excess appearing in Section 5.3 is integrable under (P4).

theorem HCPolySupport.Book.Ch05.Section52.multiscaleEllipticityMomentBounds_homogenizationScale {d : ℕ} [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (rUpper rLower : ℝ) (m : ℕ), hP4.sUpper < rUpper → rUpper < 1 → hP4.sLower < rLower → rLower < 1 → LambdaPositiveExcessMomentAtScale P (↑m) rUpper hP4.xi hP hStruct ≤ section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sUpper rUpper m * Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi ∧ lambdaInvPositiveExcessMomentAtScale P (↑m) rLower hP4.xi hP hStruct ≤ section52TwoExponentMomentBoundCoeff d hP4.xi C hP4.sLower rLower m * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi

Manuscript Lemma l.multiscale.ellipticity.moments.homogenization.scale, in its corrected two-exponent form.

The single constant is explicit in Lean and depends only on d; the public statement exposes it existentially, matching the manuscript's C(d).