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

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

Section 5.2 internals: ScalarAlgebra

Scalar identities, positive-excess algebra, and product estimates.

theorem HCPolySupport.Book.Ch05.Section52.one_le_thetaAtScale_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n : ℤ) (hBlock : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) : 1 ≤ thetaAtScale hP hStruct n

The 1 <= Theta_n part of the scalar preliminary lemma, with the inverse-star positivity proved in Chapter 4.

theorem HCPolySupport.Book.Ch05.Section52.thetaAtScale_le_widetildeThetaAtScale_of_integrable_factor_observables {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) (n : ℕ) : thetaAtScale hP hStruct ↑n ≤ widetildeThetaAtScale P (↑n) hP4

The Theta_n <= widetildeTheta_n part of the scalar preliminary lemma, using the direct Chapter 4 moment-factor endpoint.

theorem HCPolySupport.Book.Ch05.Section52.LambdaPositiveExcessMomentAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (s : ℝ) (ξ : ℕ) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) : 0 ≤ LambdaPositiveExcessMomentAtScale P m s ξ hP hStruct

The upper positive-excess moment is nonnegative.

theorem HCPolySupport.Book.Ch05.Section52.lambdaInvPositiveExcessMomentAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (s : ℝ) (ξ : ℕ) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) : 0 ≤ lambdaInvPositiveExcessMomentAtScale P m s ξ hP hStruct

The lower inverse positive-excess moment is nonnegative.

theorem HCPolySupport.Book.Ch05.Section52.real_le_base_add_max_sub_base_zero (x base : ℝ) : x ≤ base + max (x - base) 0

theorem HCPolySupport.Book.Ch05.Section52.max_sub_base_zero_le_of_le_base_add_nonneg {x base y : ℝ} (hy : 0 ≤ y) (hxy : x ≤ base + y) : max (x - base) 0 ≤ y

theorem HCPolySupport.Book.Ch05.Section52.weighted_sum_le_base_add_weighted_positiveExcess {ι : Type u_1} {s : Finset ι} {w f : ι → ℝ} {base : ℝ} (hbase : 0 ≤ base) (hw_nonneg : ∀ i ∈ s, 0 ≤ w i) (hw_sum : ∑ i ∈ s, w i ≤ 1) : ∑ i ∈ s, w i * f i ≤ base + ∑ i ∈ s, w i * max (f i - base) 0

theorem HCPolySupport.Book.Ch05.Section52.max_sup'_sub_base_le_sup'_max_sub_base {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) (f : ι → ℝ) (base : ℝ) : max (s.sup' hs f - base) 0 ≤ s.sup' hs fun (i : ι) => max (f i - base) 0

theorem HCPolySupport.Book.Ch05.Section52.section52_sq_finset_sum_weighted_rpow_half_le_finset_sum_weighted {ι : Type u_1} (s : Finset ι) {w H : ι → ℝ} (hw_nonneg : ∀ (i : ι), 0 ≤ w i) (hH_nonneg : ∀ (i : ι), 0 ≤ H i) (hw_sum : ∑ i ∈ s, w i ≤ 1) : (∑ i ∈ s, w i * (H i).rpow (1 / 2)) ^ 2 ≤ ∑ i ∈ s, w i * H i

theorem HCPolySupport.Book.Ch05.Section52.section52_sq_finset_sum_weighted_rpow_half_le_weight_sum_mul_finset_sum_weighted {ι : Type u_1} (s : Finset ι) {w H : ι → ℝ} (hw_nonneg : ∀ (i : ι), 0 ≤ w i) (hH_nonneg : ∀ (i : ι), 0 ≤ H i) : (∑ i ∈ s, w i * (H i).rpow (1 / 2)) ^ 2 ≤ (∑ i ∈ s, w i) * ∑ i ∈ s, w i * H i

theorem HCPolySupport.Book.Ch05.Section52.LambdaMomentAtScale_le_barSigma_zero_add_positiveExcessMomentAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {m : ℤ} {s : ℝ} {ξ : ℕ} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hξ : 1 ≤ ξ) (hs : 0 < s) (hBarSigma0_nonneg : 0 ≤ hP.barSigmaAtScale hStruct 0) (hUpperMeas : AEMeasurable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d m) s (Ch02.MultiscaleExponent.finite 1) a) P) (hUpperPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d m) s (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) (hUpperExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max (Ch04.LambdaSqCoeffField (originCube d m) s (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0 ^ ξ) P) : Ch04.LambdaMomentAtScale P m s ξ ≤ hP.barSigmaAtScale hStruct 0 + LambdaPositiveExcessMomentAtScale P m s ξ hP hStruct

Root decomposition for the upper ellipticity factor: ||Λ_m||_ξ <= \barσ_0 + ||(Λ_m-\barσ_0)_+||_ξ.

theorem HCPolySupport.Book.Ch05.Section52.lambdaInvMomentAtScale_le_barSigmaStar_zero_inv_add_positiveExcessMomentAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {m : ℤ} {s : ℝ} {ξ : ℕ} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hξ : 1 ≤ ξ) (hs : 0 < s) (hBarSigmaStar0_inv_nonneg : 0 ≤ (hP.barSigmaStarAtScale hStruct 0)⁻¹) (hLowerMeas : AEMeasurable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d m) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹) P) (hLowerPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d m) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) (hLowerExcessPowInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => max ((Ch04.lambdaSqCoeffField (originCube d m) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0 ^ ξ) P) : Ch04.lambdaInvMomentAtScale P m s ξ ≤ (hP.barSigmaStarAtScale hStruct 0)⁻¹ + lambdaInvPositiveExcessMomentAtScale P m s ξ hP hStruct

Root decomposition for the lower inverse ellipticity factor: ||λ_m^{-1}||_ξ <= \barσ_{*,0}^{-1} + ||(λ_m^{-1}-\barσ_{*,0}^{-1})_+||_ξ.

theorem HCPolySupport.Book.Ch05.Section52.widetildeThetaAtScale_le_thetaAtScale_zero_add_positiveExcess_products {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℤ) (hUpper : Ch04.LambdaMomentAtScale P m hP4.sUpper hP4.xi ≤ hP.barSigmaAtScale hStruct 0 + LambdaPositiveExcessMomentAtScale P m hP4.sUpper hP4.xi hP hStruct) (hLower : Ch04.lambdaInvMomentAtScale P m hP4.sLower hP4.xi ≤ (hP.barSigmaStarAtScale hStruct 0)⁻¹ + lambdaInvPositiveExcessMomentAtScale P m hP4.sLower hP4.xi hP hStruct) (hUpper0 : hP.barSigmaAtScale hStruct 0 ≤ Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi) (hLower0 : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi) (hBarSigma0_nonneg : 0 ≤ hP.barSigmaAtScale hStruct 0) : 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 "in particular" estimate in the multiscale ellipticity moment lemma.

Once the two component positive-excess estimates are known, this theorem is the Ch5 algebra turning them into a bound for widetildeTheta_m.

theorem HCPolySupport.Book.Ch05.Section52.widetildeThetaAtScale_le_thetaAtScale_zero_add_error_of_positiveExcess_bounds {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℤ) {coeffUpper coeffLower finalCoeff : ℝ} (hUpper : Ch04.LambdaMomentAtScale P m hP4.sUpper hP4.xi ≤ hP.barSigmaAtScale hStruct 0 + LambdaPositiveExcessMomentAtScale P m hP4.sUpper hP4.xi hP hStruct) (hLower : Ch04.lambdaInvMomentAtScale P m hP4.sLower hP4.xi ≤ (hP.barSigmaStarAtScale hStruct 0)⁻¹ + lambdaInvPositiveExcessMomentAtScale P m hP4.sLower hP4.xi hP hStruct) (hUpper0 : hP.barSigmaAtScale hStruct 0 ≤ Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi) (hLower0 : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi) (hBarSigma0_nonneg : 0 ≤ hP.barSigmaAtScale hStruct 0) (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

Product assembly with the two positive-excess roots already bounded by unit-scale moment roots. This is the final algebraic step in the Section 5.2 moment lemma.

theorem HCPolySupport.Book.Ch05.Section52.widetildeThetaAtScale_le_thetaAtScale_zero_add_error_of_positiveExcess_product_bound {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℤ) {coeffUpper coeffLower finalCoeff : ℝ} (hProduct : 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) (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

Final product algebra from an already assembled positive-excess product bound. This is useful when the scalar root decomposition has already been proved upstream.