Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformEllipticityEndpoint

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

The uniform ellipticity endpoint in Section 5.7

This file records the σ = ∞ endpoint of the quenched coarse-grained ellipticity assumption. The endpoint is deliberately kept as a separate API: it gives an a.s. unit-scale bound, and from that bound we may recover every finite Γσ input needed by the existing concentration arguments.

structure HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : Type

The σ = ∞ endpoint of the quenched coarse-grained ellipticity assumption.

The field bound is the Lean version of the uniform estimate Γ_∞: the unit-cube ellipticity observable is bounded by thetaHat almost surely.

• params : QuantitativeCoarseGrainedEllipticityParams d

  Parameters specifying the coarse-grained upper and lower ellipticity observables.

• thetaHat : ℝ

  Uniform almost-sure bound for the unit-cube coarse-grained ellipticity observable.

• thetaHat_pos : 0 < self.thetaHat
• bound : gammaSigmaUnitEllipticityObservable hP hStruct self.params.sUpper self.params.sLower ≤ᵐ[P] fun (x : RegCoeffField d) => self.thetaHat

structure HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticityNoXi {d : ℕ} [NeZero d] (P : Ch04.RestrictionCoeffLaw d) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : Type

Manuscript-facing σ = ∞ endpoint of (P5), with no exposed moment exponent xi.

• params : GammaCoarseGrainedEllipticityParams d

  Parameters specifying the coarse-grained upper and lower ellipticity observables.

• thetaHat : ℝ

  Uniform almost-sure bound for the unit-cube coarse-grained ellipticity observable.

• thetaHat_pos : 0 < self.thetaHat
• bound : gammaSigmaUnitEllipticityObservable hP hStruct self.params.sUpper self.params.sLower ≤ᵐ[P] fun (x : RegCoeffField d) => self.thetaHat

noncomputable def HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticityNoXi.withInternalXi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticityNoXi P hP hStruct) : GammaInfinityCoarseGrainedEllipticity P hP hStruct

Add the internal finite moment exponent used by the existing endpoint proof infrastructure.

Equations

• hInf.withInternalXi = { params := hInf.params.toQuantitativeParams, thetaHat := hInf.thetaHat, thetaHat_pos := ⋯, bound := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticityNoXi.withInternalXi_thetaHat {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticityNoXi P hP hStruct) : hInf.withInternalXi.thetaHat = hInf.thetaHat

theorem HCPolySupport.Book.Ch05.Section57.ae_le_of_map_eq_map_aemeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {A : ℝ} (hYm : AEMeasurable Y μ) (hXm : AEMeasurable X μ) (hmap : MeasureTheory.Measure.map Y μ = MeasureTheory.Measure.map X μ) (hX : X ≤ᵐ[μ] fun (x : Ω) => A) : Y ≤ᵐ[μ] fun (x : Ω) => A

Transfer an a.s. upper bound across equality in law.

theorem HCPolySupport.Book.Ch05.Section57.blockJObservableCubeSetBlockVec_originCube_le_of_scaleZero_ae {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {θ : ℝ} (Pvec Qvec : BlockVec d) (h0 : Ch04.blockJObservableCubeSetBlockVec (originCube d 0) Pvec Qvec ≤ᵐ[Pμ] fun (x : RegCoeffField d) => θ) {n : ℤ} (hn : 0 ≤ n) : Ch04.blockJObservableCubeSetBlockVec (originCube d n) Pvec Qvec ≤ᵐ[Pμ] fun (x : RegCoeffField d) => θ

A deterministic counterpart of the finite-Γσ scale-zero propagation: an a.s. bound at the unit origin cube propagates to every larger origin cube.

theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_of_mem_descendantsAtScale_le_ae {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {θ : ℝ} {m n : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) (e : FullBlockVec d) (hOrigin : limitNormalizedBlockJObservable hPμ hStruct (originCube d n) e ≤ᵐ[Pμ] fun (x : RegCoeffField d) => θ) : limitNormalizedBlockJObservable hPμ hStruct R e ≤ᵐ[Pμ] fun (x : RegCoeffField d) => θ

Transfer an a.s. bound from the origin cube at scale n to a descendant cube at the same scale, using stationarity.

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_le_of_originCube_ae {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {θ : ℝ} {m n : ℕ} (hnm : n ≤ m) (e : FullBlockVec d) (hOrigin : limitNormalizedBlockJObservable hPμ hStruct (originCube d ↑n) e ≤ᵐ[Pμ] fun (x : RegCoeffField d) => θ) : localizedLimitNormalizedJMax hPμ hStruct m n e ≤ᵐ[Pμ] fun (x : RegCoeffField d) => θ

An a.s. origin-cube bound controls the localized maximum over descendants.

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.sUpper_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) : 0 < hInf.params.sUpper

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.sLower_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) : 0 < hInf.params.sLower

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.unitEllipticityObservable_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) (a : RegCoeffField d) : 0 ≤ gammaSigmaUnitEllipticityObservable hP hStruct hInf.params.sUpper hInf.params.sLower a

The guarded unit-cube observable is nonnegative even before proving that the normalizing scalar barσ_0 is positive.

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.abs_unitEllipticityObservable_le_thetaHat_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) : (fun (a : RegCoeffField d) => |gammaSigmaUnitEllipticityObservable hP hStruct hInf.params.sUpper hInf.params.sLower a|) ≤ᵐ[P] fun (x : RegCoeffField d) => hInf.thetaHat

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.unitEllipticityObservable_isBigO {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) {σ : ℝ} (_hσ : 0 < σ) : IndependentSums.IsBigO P (IndependentSums.gammaSigma σ) (gammaSigmaUnitEllipticityObservable hP hStruct hInf.params.sUpper hInf.params.sLower) hInf.thetaHat

A uniform unit-scale bound is, in particular, a finite Γσ tail for every positive finite exponent σ.

def HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.toGammaSigma {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) (σ : ℝ) (hσ : 0 < σ) : GammaSigmaCoarseGrainedEllipticity P hP hStruct

Forget the endpoint input to any finite positive Γσ input.

Equations

• hInf.toGammaSigma σ hσ = { sigma := σ, sigma_pos := hσ, params := hInf.params, thetaHat := hInf.thetaHat, thetaHat_pos := ⋯, tail := ⋯ }

noncomputable def HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.toQuantitativeCoarseGrainedEllipticity {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) : QuantitativeCoarseGrainedEllipticity P

The endpoint implies the Chapter 5 quantitative coarse-grained ellipticity package, via any finite exponent.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.barSigmaAtScale_zero_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) : 0 < hP.barSigmaAtScale hStruct 0

noncomputable def HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.unitJConst (d : ℕ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

The deterministic unit-scale constant for the endpoint normalized J bound.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.unitJConst_pos {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < unitJConst d params

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.limitNormalizedBlockJObservable_unit_le_thetaHat_sq_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) (e : FullBlockVec d) (he : ∀ (α : BlockCoord d), |e α| ≤ 1) : limitNormalizedBlockJObservable hP hStruct (originCube d 0) e ≤ᵐ[P] fun (x : RegCoeffField d) => unitJConst d hInf.params * hInf.thetaHat ^ 2

Under the endpoint assumption, the limiting-normalized unit-cube J observable is almost surely bounded by a deterministic multiple of thetaHat^2.

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.limitNormalizedBlockJObservable_originCube_le_thetaHat_sq_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) (e : FullBlockVec d) (he : ∀ (α : BlockCoord d), |e α| ≤ 1) {n : ℕ} : limitNormalizedBlockJObservable hP hStruct (originCube d ↑n) e ≤ᵐ[P] fun (x : RegCoeffField d) => unitJConst d hInf.params * hInf.thetaHat ^ 2

The endpoint unit J bound propagates to every origin scale.

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.localizedNormalizedProbeJMax_le_thetaHat_sq_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) {m n : ℕ} (hnm : n ≤ m) : localizedNormalizedProbeJMax hP hStruct m n ≤ᵐ[P] fun (x : RegCoeffField d) => unitJConst d hInf.params * hInf.thetaHat ^ 2

The endpoint controls every localized normalized finite-probe maximum by a deterministic multiple of thetaHat^2.

theorem HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticity.localizedLimitWeightedUnitEllipticitySup_le_thetaHat_sq_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticity P hP hStruct) {m : ℕ} : localizedLimitWeightedUnitEllipticitySup hP hStruct hInf.params m ≤ᵐ[P] fun (x : RegCoeffField d) => Ch04.gammaMomentConst 1 * ↑hInf.params.xi * hInf.thetaHat ^ 2

The endpoint controls the localized scale-zero unit-ellipticity supremum by a deterministic multiple of thetaHat^2.

noncomputable def HCPolySupport.Book.Ch05.Section57.GammaInfinityCoarseGrainedEllipticityNoXi.toGammaSigmaNoXi {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hInf : GammaInfinityCoarseGrainedEllipticityNoXi P hP hStruct) (σ : ℝ) (hσ : 0 < σ) : GammaSigmaCoarseGrainedEllipticityNoXi P hP hStruct

Forget the endpoint input to any finite positive Γσ input, in the manuscript-facing parameter package with no exposed moment exponent.

Equations

• hInf.toGammaSigmaNoXi σ hσ = { sigma := σ, sigma_pos := hσ, params := hInf.params, thetaHat := hInf.thetaHat, thetaHat_pos := ⋯, tail := ⋯ }

theorem HCPolySupport.Book.Ch05.Section57.firstQuenchedEstimate_limitNormalized_uniformAnnealedExponent_noXi_infinity {d : ℕ} [NeZero d] (params : GammaCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∃ (Cfluct : ℝ), 0 < Cfluct ∧ ∀ {Pμ : Ch04.RestrictionCoeffLaw d} (hPμ : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hInf : GammaInfinityCoarseGrainedEllipticityNoXi Pμ hPμ hStruct), hInf.params = params → ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ {n m : ℕ}, n < m → have hΓ2 := hInf.toGammaSigmaNoXi 2 firstQuenchedEstimate_limitNormalized_uniformAnnealedExponent_noXi_infinity._proof_1; have N0 := annealedAlgebraicEntryScale Pμ hΓ2.withInternalXi.toQuantitativeCoarseGrainedEllipticity Centry; IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma 2) (fun (aω : RegCoeffField d) => limitNormalizedBlockJObservable hPμ hStruct (originCube d ↑(N0 + m)) e aω - Real.rpow 3 (-a * ↑n)) (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + m) - ↑(N0 + n)).toNat) * hInf.thetaHat ^ 2)

Endpoint (σ = ∞) version of Corollary c.first.quenched.estimate.

In Lean the endpoint assumption is a separate structure. The conclusion is obtained by applying the finite-σ corollary at σ = 2, which is exactly the Γ_{σ ∧ 2} exponent when σ = ∞.