Coarse-graining support: Support.Book.Ch05.Theorems.Section57.QuenchedGammaEllipticity #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Quenched Γσ coarse-grained ellipticity #
This file formalizes the strengthened unit-cube ellipticity assumption from
Section 5.7. The assumption is intentionally kept separate from (P4): the
manuscript says this Γσ condition implies the moment hypothesis, so later files
must prove that implication rather than assume it.
The parameter-only part of the strengthened Section 5.7 (P5) input.
Unlike the Chapter 5 (P4) parameter bundle, this record carries no moment
exponent xi: a finite xi can be chosen internally from the positivity of
sUpper and sLower whenever the older moment-based API is needed.
- sUpper : ℝ
The upper-ellipticity exponent, required to lie strictly between zero and one.
- sLower : ℝ
The lower-ellipticity exponent, required to lie strictly between zero and one.
Instances For
Choose an internal finite moment exponent compatible with the older (P4)
parameter API.
Convert the Section 5.7 (P5) parameters to the older (P4) parameter
bundle by choosing an internal finite moment exponent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit-cube Γσ ellipticity observable from
(a.cg.ellipticity.Gamma.sigma).
In the manuscript notation this is
barσ_0^{-1} Λ_{s_1,1}(□_0) + barσ_0 λ_{s_2,1}^{-1}(□_0).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The strengthened quenched ellipticity assumption (P5) in Section 5.7.
The constant thetaHat is the manuscript's \hat Θ_0. No probability law
appears in the choice of the exponents or constants beyond the tail statement
itself; later estimates should quantify their constants before the law.
- sigma : ℝ
The positive parameter of the
gammaSigmatail bound. - params : QuantitativeCoarseGrainedEllipticityParams d
The coarse-grained ellipticity exponents and their finite moment parameter.
- thetaHat : ℝ
The positive size parameter in the tail bound for the unit-cube ellipticity observable.
- tail : IndependentSums.IsBigO P (IndependentSums.gammaSigma self.sigma) (gammaSigmaUnitEllipticityObservable hP hStruct self.params.sUpper self.params.sLower) self.thetaHat
Instances For
The manuscript-facing finite-σ Section 5.7 (P5) input, with no exposed
moment exponent xi.
- sigma : ℝ
The positive parameter of the
gammaSigmatail bound. - params : GammaCoarseGrainedEllipticityParams d
The coarse-grained ellipticity exponents, without an exposed moment parameter.
- thetaHat : ℝ
The positive size parameter in the tail bound for the unit-cube ellipticity observable.
- tail : IndependentSums.IsBigO P (IndependentSums.gammaSigma self.sigma) (gammaSigmaUnitEllipticityObservable hP hStruct self.params.sUpper self.params.sLower) self.thetaHat
Instances For
Add the internal finite moment exponent used by the existing Section 5.7 proof infrastructure.
Equations
- hΓ.withInternalXi = { sigma := hΓ.sigma, sigma_pos := ⋯, params := hΓ.params.toQuantitativeParams, thetaHat := hΓ.thetaHat, thetaHat_pos := ⋯, tail := ⋯ }
Instances For
The Γσ tail assumption gives finite moments of the normalized unit-cube
ellipticity observable itself. Splitting this into separate Λ and
λ^{-1} moments is the next deterministic normalization step.
The Γσ tail makes the unit-scale normalization well-formed: the scalar
\bar σ_0 is strictly positive.
The guarded definition of gammaSigmaUnitEllipticityObservable agrees with the
manuscript expression when this theorem is used. In the contradictory branch
\bar σ_0 ≤ 0, the guard asks for Γσ control of the unnormalized factor sum;
that gives the unit-scale factor integrability needed to recover
\bar σ_0 > 0 from the Chapter 4 positivity theorem.
Conditional bridge from the Γσ unit-cube assumption to the old (P4)
moment hypothesis.
The extra input is exactly the positivity of the normalizing scalar
\bar σ_0. Mathematically this is implicit in the displayed Γσ assumption;
Lean's inverse is total, so the positivity must be supplied or proved before
the two normalized summands can be split.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Γσ unit-cube assumption implies the old (P4) moment hypothesis.
Instances For
The L^ξ root of the normalized unit-cube Γσ ellipticity observable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit-scale annealed scalar contrast is controlled linearly by the Γσ moment root.
The unit-scale annealed scalar contrast is controlled by the deterministic Γσ moment scale.
Quantitative ordering of the old unit-scale moment contrast by the Γσ
scale. This is the Lean form of the \widetilde Θ_0 consequence; with the
current definitions the direct bound is quadratic in the Γσ scale.