Coarse-graining support: Support.Book.Ch05.Theorems.Section57.LocalizedUnitEllipticity #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Localized limiting-normalized unit ellipticity #
This file gives the stationarity transfer and finite-sup tail bound for the unit-cube ellipticity observable normalized by the limiting scalar matrix.
theorem
HCPolySupport.Book.Ch05.Section57.aemeasurable_limitWeightedUnitEllipticityObservableOnCube
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(Q : TriadicCube d)
{sUpper sLower : ℝ}
(hsUpper : 0 < sUpper)
(hsLower : 0 < sLower)
:
AEMeasurable (limitWeightedUnitEllipticityObservableOnCube hP hStruct Q sUpper sLower) P
theorem
HCPolySupport.Book.Ch05.Section57.map_limitWeightedUnitEllipticityObservableOnCube_eq_origin_of_scale_zero
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
{U : TriadicCube d}
(hUscale : U.scale = 0)
{sUpper sLower : ℝ}
(hsUpper : 0 < sUpper)
(hsLower : 0 < sLower)
:
MeasureTheory.Measure.map (limitWeightedUnitEllipticityObservableOnCube hP hStruct U sUpper sLower) P = MeasureTheory.Measure.map (limitWeightedUnitEllipticityObservable hP hStruct sUpper sLower) P
The localized limiting-normalized unit ellipticity observable has the same law as the origin observable on every scale-zero cube.
theorem
HCPolySupport.Book.Ch05.Section57.isBigO_limitWeightedUnitEllipticityObservableOnCube_of_scale_zero
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
{U : TriadicCube d}
(hUscale : U.scale = 0)
:
IndependentSums.IsBigO P (IndependentSums.gammaSigma hΓ.sigma)
(limitWeightedUnitEllipticityObservableOnCube hP hStruct U hΓ.params.sUpper hΓ.params.sLower)
(thetaAtScale hP hStruct 0 * hΓ.thetaHat)
The Γσ tail of the limiting-normalized unit ellipticity observable transfers to every scale-zero cube.
noncomputable def
HCPolySupport.Book.Ch05.Section57.localizedLimitWeightedUnitEllipticitySup
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(params : QuantitativeCoarseGrainedEllipticityParams d)
(m : ℕ)
:
RegCoeffField d → ℝ
Scale-zero descendant supremum of the limiting-normalized unit ellipticity
inside \cu_m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.Book.Ch05.Section57.scaleZero_ellipticity_sup_bounds_of_localizedLimitWeightedUnitEllipticitySup_le
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
{m : ℕ}
{t M : ℝ}
(hUpper_t : hΓ.params.sUpper < t)
(hLower_t : hΓ.params.sLower < t)
(hsup : localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m a ≤ M ^ 2)
:
let Q := originCube d ↑m;
let D := descendantsAtScale Q 0;
have hD := ⋯;
have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha;
((barSigmaLimit hP hStruct)⁻¹ * D.sup' hD fun (U : TriadicCube d) => Ch02.LambdaSq U t (Ch02.MultiscaleExponent.finite 1) F) ≤ M ^ 2 ∧ (barSigmaLimit hP hStruct * D.sup' hD fun (U : TriadicCube d) => (Ch02.lambdaSq U t (Ch02.MultiscaleExponent.finite 1) F)⁻¹) ≤ M ^ 2
A collapsed bound on the localized limiting-normalized unit ellipticity supremum controls the Ch2 upper and lower unit-ellipticity suprema at any larger exponent.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_localizedLimitWeightedUnitEllipticitySup_tail_le_card_mul_exp
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
(m : ℕ)
{lam : ℝ}
(hlam : 1 ≤ lam)
:
have Q := originCube d ↑m;
have D := descendantsAtScale Q 0;
MeasureTheory.Measure.real P
{a : RegCoeffField d | thetaAtScale hP hStruct 0 * hΓ.thetaHat * lam < localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m a} ≤ ↑D.card * Real.exp (-lam ^ hΓ.sigma)