Coarse-graining support: Support.Book.Ch04.Theorems.WidetildeTheta

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

Moment roots and widetildeTheta

Clean Ch4 definitions of the scalar moment roots used to compare the primitive contrast Theta_n to the moment-enhanced quantity widetildeTheta_n.

noncomputable def HCPolySupport.Book.Ch04.annealedMomentRoot {d : ℕ} (P : RestrictionCoeffLaw d) (ξ : ℕ) (X : RegCoeffField d → ℝ) : ℝ

The annealed L^ξ moment root of a nonnegative scalar observable.

Equations

• HCPolySupport.Book.Ch04.annealedMomentRoot P ξ X = (∫ (a : HCPolySupport.RegCoeffField d), X a ^ ξ ∂P) ^ (1 / ↑ξ)

noncomputable def HCPolySupport.Book.Ch04.LambdaSqCoeffField {d : ℕ} (Q : TriadicCube d) (s : ℝ) (q : Ch02.MultiscaleExponent) (a : RegCoeffField d) : ℝ

The upper multiscale ellipticity observable on ambient coefficient fields. On the a.e.-elliptic support it uses the canonical dependent Ch2 coefficient family; off support it is totalized by 0.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.lambdaSqCoeffField {d : ℕ} (Q : TriadicCube d) (s : ℝ) (q : Ch02.MultiscaleExponent) (a : RegCoeffField d) : ℝ

The lower multiscale ellipticity observable on ambient coefficient fields. On the a.e.-elliptic support it uses the canonical dependent Ch2 coefficient family; off support it is totalized by 0.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch04.LambdaSqCoeffField_originCube_zero_translateByInt_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (z : Fin d → ℤ) (s : ℝ) (q : Ch02.MultiscaleExponent) : (fun (a : RegCoeffField d) => LambdaSqCoeffField (translateCube z (originCube d 0)) s q a) =ᵐ[P] fun (a : RegCoeffField d) => LambdaSqCoeffField (originCube d 0) s q (translateReg (intVecToRealVec z) a)

Upper multiscale ellipticity on the scale-zero origin cube is covariant under integer translations, almost surely under a stationary law carrier.

theorem HCPolySupport.Book.Ch04.lambdaSqCoeffField_originCube_zero_translateByInt_ae {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (hstat : RestrictionStationaryLaw P) (z : Fin d → ℤ) (s : ℝ) (q : Ch02.MultiscaleExponent) : (fun (a : RegCoeffField d) => lambdaSqCoeffField (translateCube z (originCube d 0)) s q a) =ᵐ[P] fun (a : RegCoeffField d) => lambdaSqCoeffField (originCube d 0) s q (translateReg (intVecToRealVec z) a)

Lower multiscale ellipticity on the scale-zero origin cube is covariant under integer translations, almost surely under a stationary law carrier.

theorem HCPolySupport.Book.Ch04.LambdaSqCoeffField_finite_nonneg {d : ℕ} (Q : TriadicCube d) {s q : ℝ} (a : RegCoeffField d) (hs : 0 < s) (hq : 1 ≤ q) : 0 ≤ LambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite q) a

theorem HCPolySupport.Book.Ch04.lambdaSqCoeffField_finite_nonneg {d : ℕ} (Q : TriadicCube d) {s q : ℝ} (a : RegCoeffField d) (hs : 0 < s) (hq : 1 ≤ q) : 0 ≤ lambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite q) a

noncomputable def HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : RegCoeffField d) : ℝ

Ambient coefficient-field lift of the Ch2 descendant upper-left operator norm maximum. It uses the canonical dependent Ch2 coefficient family on the a.e.-locally elliptic support and is zero off that support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : RegCoeffField d) : ℝ

Ambient coefficient-field lift of the Ch2 descendant lower-right inverse operator-norm maximum.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.finsetSupReal_eq_sup' {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (f : α → ℝ) : Ch02.finsetSupReal s f = s.sup' hs f

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_finset_sup' {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s : Finset ι} (hs : s.Nonempty) {f : ι → Ω → ℝ} (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (s.sup' hs f) μ

Finite nonempty suprema of almost-everywhere measurable real observables remain almost-everywhere measurable.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.maxDescendantBMatrixNormCoeffFieldAtScale_eq_finsetSupReal_ae {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (k : ℤ) : maxDescendantBMatrixNormCoeffFieldAtScale Q k a = Ch02.finsetSupReal (descendantsAtScale Q k) fun (R : TriadicCube d) => Ch02.matrixNorm (coarseBlockMatrix (cubeSet R) a.toFun).upperLeft

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale_eq_finsetSupReal_ae {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (k : ℤ) : maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q k a = Ch02.finsetSupReal (descendantsAtScale Q k) fun (R : TriadicCube d) => Ch02.matrixNorm (coarseBlockMatrix (cubeSet R) a.toFun).lowerRight

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.summable_weighted_maxDescendantBMatrixNormCoeffFieldAtScale {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : RegCoeffField d) {s : ℝ} (hs : 0 < s) : Summable fun (n : ℕ) => Ch02.geometricWeight s 1 n * (maxDescendantBMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.summable_weightedMaxDescendantSigmaStarInverseMatrixNorm {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : RegCoeffField d) {s : ℝ} (hs : 0 < s) : Summable fun (n : ℕ) => Ch02.geometricWeight s 1 n * (maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.LambdaSqCoeffField_finite_one_eq_tsum_sq {d : ℕ} (Q : TriadicCube d) (a : RegCoeffField d) (s : ℝ) : LambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a = (∑' (n : ℕ), Ch02.geometricWeight s 1 n * (maxDescendantBMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) ^ 2

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.lambdaSqCoeffField_finite_one_eq_tsum_sq_inv {d : ℕ} (Q : TriadicCube d) (a : RegCoeffField d) {s : ℝ} (hs : 0 < s) : lambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a = ((∑' (n : ℕ), Ch02.geometricWeight s 1 n * (maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) ^ 2)⁻¹

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_LambdaSqCoeffField_finite_one {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) : AEMeasurable (fun (a : RegCoeffField d) => LambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a) P

The upper all-scale coefficient observable at a deterministic triadic cube is a.e.-measurable under a Chapter 4 law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_lambdaSqCoeffField_finite_one {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) : AEMeasurable (fun (a : RegCoeffField d) => lambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a) P

The lower all-scale coefficient observable at a deterministic triadic cube is a.e.-measurable under a Chapter 4 law carrier.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_lambdaSqCoeffField_finite_one_inv {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) : AEMeasurable (fun (a : RegCoeffField d) => (lambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a)⁻¹) P

The inverse lower all-scale coefficient observable at a deterministic triadic cube is a.e.-measurable under a Chapter 4 law carrier.

theorem HCPolySupport.Book.Ch04.LambdaSqCoeffField_finite_one_le_tsum_weighted_maxDescendantBMatrixNormAtScale {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : RegCoeffField d) {s : ℝ} (hs : 0 < s) : LambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a ≤ ∑' (n : ℕ), Ch02.geometricWeight s 1 n * maxDescendantBMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a

The q=1 deterministic Jensen split for the ambient upper multiscale ellipticity observable. This is the Ch4-facing form of the Ch2 theorem, with no probability or measurability assumptions.

theorem HCPolySupport.Book.Ch04.lambdaSqCoeffField_finite_one_inv_le_tsum_weighted_maxDescendantSigmaStarInvMatrixNormAtScale {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : RegCoeffField d) {s : ℝ} (hs : 0 < s) : (lambdaSqCoeffField Q s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ≤ ∑' (n : ℕ), Ch02.geometricWeight s 1 n * maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a

The q=1 deterministic Jensen split for the ambient lower inverse multiscale ellipticity observable.

noncomputable def HCPolySupport.Book.Ch04.LambdaMomentAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (s : ℝ) (ξ : ℕ) : ℝ

Upper multiscale ellipticity moment at scale n.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.lambdaInvMomentAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (s : ℝ) (ξ : ℕ) : ℝ

Lower inverse multiscale ellipticity moment at scale n.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch04.widetildeThetaAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (sUpper sLower : ℝ) (ξ : ℕ) : ℝ

The moment-enhanced contrast \widetilde\Theta_n.

Equations

• HCPolySupport.Book.Ch04.widetildeThetaAtScale P n sUpper sLower ξ = HCPolySupport.Book.Ch04.LambdaMomentAtScale P n sUpper ξ * HCPolySupport.Book.Ch04.lambdaInvMomentAtScale P n sLower ξ

theorem HCPolySupport.Book.Ch04.annealedMomentRoot_nonneg_of_nonneg {d : ℕ} (P : RestrictionCoeffLaw d) (ξ : ℕ) {X : RegCoeffField d → ℝ} (hX : ∀ (a : RegCoeffField d), 0 ≤ X a) : 0 ≤ annealedMomentRoot P ξ X

theorem HCPolySupport.Book.Ch04.annealedMomentRoot_le_of_ae_nonneg_le {d : ℕ} {P : RestrictionCoeffLaw d} {ξ : ℕ} {X Y : RegCoeffField d → ℝ} (hξ : 1 ≤ ξ) (hX_nonneg : ∀ (a : RegCoeffField d), 0 ≤ X a) (hX_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => X a ^ ξ) P) (hY_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Y a ^ ξ) P) (hXY : X ≤ᵐ[P] Y) : annealedMomentRoot P ξ X ≤ annealedMomentRoot P ξ Y

Monotonicity of the annealed moment root under a.e. domination of nonnegative observables.

theorem HCPolySupport.Book.Ch04.LambdaMomentAtScale_nonneg {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) {s : ℝ} (ξ : ℕ) (hs : 0 < s) : 0 ≤ LambdaMomentAtScale P n s ξ

theorem HCPolySupport.Book.Ch04.lambdaInvMomentAtScale_nonneg {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) {s : ℝ} (ξ : ℕ) (hs : 0 < s) : 0 ≤ lambdaInvMomentAtScale P n s ξ

theorem HCPolySupport.Book.Ch04.annealedMomentRoot_le_const_add_of_nonneg_le {d : ℕ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {ξ : ℕ} {X E : RegCoeffField d → ℝ} {A : ℝ} (hξ : 1 ≤ ξ) (hA_nonneg : 0 ≤ A) (hX_nonneg : ∀ (a : RegCoeffField d), 0 ≤ X a) (hE_nonneg : ∀ (a : RegCoeffField d), 0 ≤ E a) (hX_le : ∀ (a : RegCoeffField d), X a ≤ A + E a) (hX_meas : AEMeasurable X P) (hE_meas : AEMeasurable E P) (hX_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a| ^ ξ) P) (hE_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |E a| ^ ξ) P) : annealedMomentRoot P ξ X ≤ A + annealedMomentRoot P ξ E

Root decomposition for a nonnegative observable controlled by a deterministic base plus a nonnegative error: ||X||_ξ <= A + ||E||_ξ when X <= A + E.

This is the Ch4-owned scalar Minkowski step used in the Section 5.2 moment lemma.

theorem HCPolySupport.Book.Ch04.Internal.annealedThetaAtScaleOfPrimitive_le_widetildeThetaAtScale_of_factor_bounds {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} {sUpper sLower : ℝ} {ξ : ℕ} (primitive : AnnealedPrimitiveScalarizationData P n) (hsUpper : 0 < sUpper) (hUpper : barBAtScaleOfPrimitive primitive ≤ LambdaMomentAtScale P n sUpper ξ) (hStarInv_nonneg : 0 ≤ barSigmaStarInvAtScaleOfPrimitive primitive) (hLower : barSigmaStarInvAtScaleOfPrimitive primitive ≤ lambdaInvMomentAtScale P n sLower ξ) : annealedThetaAtScaleOfPrimitive primitive ≤ widetildeThetaAtScale P n sUpper sLower ξ

Internal primitive factor bounds imply Theta_n <= widetildeTheta_n.