UpperLeg

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

Upper coarse-ellipticity leg

This module provides the direct upper leg consumed by coarse_ellipticity_bounds_of_legs. Its public result superposedFlux_coarse_ellipticity_upper_leg chooses one dimension-only constant before the model, scale, exponent, and window data and returns the literal upper Orlicz carrier of the frozen theorem.

The proof has two branches. For m ≤ mStarStar M, coarse_ellipticity_upper_of_le_mStarStar uses the base-case cutoff-mass estimate. For mStarStar M < m, the twelve analytic lanes are constructed per descendant and then aggregated separately for finite exponents below two and for finite exponents at least two together with infinity. The deep-band mean enters the deterministic shift; it is not hidden in the ordinary Orlicz lane.

No caller supplies an upper estimate, summability assertion, measurability assertion, or packaged fraction of the conclusion to the final theorem.

References

• ABK26, p.cg.ellipticity.bounds, statement and proof.
• ABK26, e.basecase.homogenization.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseEllipticityRareBudgetConst (d : ℕ) : ℝ

The dimension-dependent budget for the rare coarse-ellipticity contribution.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseEllipticityUpperMergeConst (d : ℕ) : ℝ

A common constant joining the upper coarse-ellipticity estimates.

Equations

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

1. The model-free split constructor

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isDeterministicShiftTwoTermOneSidedOrlicz_of_split {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {sigma1 sigma2 : ℝ} {X Udet U1 Uexp : Ω → ℝ} {b A1 A2 : ℝ} (hsigma1 : 0 < sigma1) (hsigma2 : 0 < sigma2) (hA1 : 0 < A1) (hA2 : 0 < A2) (hXmeas : Measurable X) (h1m : Measurable U1) (hexpm : Measurable Uexp) (hdom : ∀ (omega : Ω), X omega ≤ Udet omega + U1 omega + Uexp omega) (hdet : ∀ (omega : Ω), Udet omega ≤ b) (h1 : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma sigma1) U1 A1) (hexp : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma sigma2) Uexp A2) : Probability.IsDeterministicShiftTwoTermOneSidedOrlicz μ (HCPolySupport.IndependentSums.gammaSigma sigma1) (HCPolySupport.IndependentSums.gammaSigma sigma2) X b A1 A2

A pointwise three-term split with a deterministic first summand is the source's X ≤ b + O_{Gamma_{sigma1}}(A1) + O_{Gamma_{sigma2}}(A2).

This is the only probabilistic step of the leg's reduction: the mean-split route produces its output as Udet + U1 + Uexp with Udet deterministic, and this lemma is what turns that into the frozen carrier.

2. Direct small-scale branch

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.directSmallUpperMassConst (d : ℕ) : ℝ

The dimension-dependent mass constant in the direct small-scale upper estimate.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.directSmallUpperMassConst d = 320 * Algsuperdiff.Section3.Provider.Base.cutoffMassSqrtConst d ^ 2 * (1 + 12 * ↑d * Real.log 3)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.directSmallUpper_mass_scale_le {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStarStar M) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hhalf : M.gamma / 2 < s) : 4 * (HCPolySupport.Book.Ch02.geometricDiscount (s / 2) 2)⁻¹ * (HCPolySupport.IndependentSums.gammaTriangleConst 1 * Base.cutoffMassLinearWeightedScale M m ⟨s / 2, ⋯⟩) ≤ directSmallUpperMassConst d * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffUpperEllipticity_le_four_mul_infinity_half {d : ℕ} (M : ABKModel d) (m L : ℤ) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : Observable.cutoffUpperEllipticity M m L s hs q omega ≤ 4 * Observable.cutoffUpperEllipticity M m L (s / 2) ⋯ CoarseEllipticityExponent.infinity omega

Every admissible cutoff upper coefficient at s is bounded by four times the true infinity endpoint at s / 2, uniformly in the exponent.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffUpperEllipticity_mul_sigmaBarInv_le_four_add_mass {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStarStar M) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : Observable.cutoffUpperEllipticity M m m s hs q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹ ≤ 4 + 4 * (HCPolySupport.Book.Ch02.geometricDiscount (s / 2) 2)⁻¹ * Base.cutoffMassLinearWeightedSum M (HCPolySupport.originCube d m) m ⟨s / 2, ⋯⟩ omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_upper_of_le_mStarStar {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStarStar M) {Cup : ℝ} (hfour : 4 ≤ Cup) (hmassConst : directSmallUpperMassConst d ≤ Cup) (E : { E : ℝ // 1 ≤ E }) (sigma : ℝ) (hsigma : sigma ∈ Set.Ioc 0 (1 / 2)) (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1) : Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Cup (Cup * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The upper-family carrier in the direct branch m ≤ mStarStar M. The branch uses no induction-state or large-scale gate premise.

3. The complete upper leg

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFlux_coarse_ellipticity_upper_leg (d : ℕ) : ∃ (Cup : ℝ), 0 < Cup ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Cup (Cup * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The direct upper half of the exact coarse-ellipticity theorem. One dimension-only constant is selected before the model and every scale; the small-scale branch is handled above, while the large-scale branch constructs the twelve-lane per-descendant split and aggregates all finite and infinite exponents.