Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UnitEllipticityMinimalExpLogSq #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Compressed unit-ellipticity minimal scale #
This file gives the localized unit-ellipticity stopping scale the same
manuscript-scale stochastic envelope as the quenched J stopping scale:
exp(C log^2(2 + thetaHat)).
theorem
HCPolySupport.Book.Ch05.Section57.exists_unitEllipticityMinimalScale_interpolated_expLogSq
{d : ℕ}
[NeZero d]
{σ : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
{t α : ℝ}
:
have η := finiteQuenchedTailExponent d σ t;
0 < t →
0 ≤ α →
α < t →
∃ (Cscale : ℝ),
0 < Cscale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = σ →
hΓ.params = params →
∃ (X : RegCoeffField d → ℝ),
IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X
(Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m : ℕ},
X aω ≤ 3 ^ m →
localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m aω ≤ (Real.rpow 3 (t * ↑m) * √((3 ^ m / X aω) ^ (-α))) ^ 2
The localized unit-ellipticity minimal scale with the note-facing
exp(C log^2(2 + thetaHat)) stochastic size.