Exponent

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Section 3 coarse-ellipticity exponents

This file fixes the admissible finite-or-infinite exponent carrier and the source window used by the Section 3 coarse-ellipticity statements, together with the source-corrected deterministic lower-pole amplitude.

Main definitions

• CoarseEllipticityExponent: the admissible subtype of CoarseGraining's multiscale exponent carrier.
• lowerEllipticityProfile: the source-corrected total deterministic lower profile on raw parameters.

References

• ABK26, Proposition p.cg.ellipticity.bounds.

def Algsuperdiff.Section3.CoarseEllipticityExponent : Type

The exact admissible carrier for the source range q ∈ [1, infinity]: finite CoarseGraining multiscale exponents at least one, together with the infinity endpoint.

Equations

• Algsuperdiff.Section3.CoarseEllipticityExponent = { q : HCPolySupport.Book.Ch02.MultiscaleExponent // q.IsAdmissible }

def Algsuperdiff.Section3.CoarseEllipticityExponent.finite (q : { q : ℝ // 1 ≤ q }) : CoarseEllipticityExponent

An admissible finite coarse-ellipticity exponent.

Equations

• Algsuperdiff.Section3.CoarseEllipticityExponent.finite q = ⟨HCPolySupport.Book.Ch02.MultiscaleExponent.finite ↑q, ⋯⟩

def Algsuperdiff.Section3.CoarseEllipticityExponent.infinity : CoarseEllipticityExponent

The admissible infinity endpoint.

Equations

• Algsuperdiff.Section3.CoarseEllipticityExponent.infinity = ⟨HCPolySupport.Book.Ch02.MultiscaleExponent.infinity, trivial⟩

noncomputable def Algsuperdiff.Section3.lowerEllipticityProfile (C gamma s : ℝ) (q : CoarseEllipticityExponent) : ℝ

The total deterministic lower-ellipticity profile in the supersession-resolved Section 3.3 source. At finite exponents below 2, the pole has order 2 / q; at finite exponents at least 2, it has order one; the infinity endpoint is the direct constant bound.

Positivity of 2 * s - gamma is a theorem-side consequence of the source window. It is deliberately not stored in this definition's arguments, so a frozen source statement can quantify the manuscript's raw s : ℝ without a proof-valued carrier or an equality premise.

Equations

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