SuperposedFluxLowerInfinity

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

The sharp lower endpoint branch

This file sums the sharp pointwise remainder against the exact endpoint weight and supplies the conditional infinity-exponent payload. Its scalar output-constant inequalities remain caller-supplied obligations; these Provider helpers assert no source-node status.

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

Fixed prefactor in the infinity-exponent final Orlicz budget.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxInfinityBudgetConst_pos {d : ℕ} (hd : 2 ≤ d) : 0 < superposedFluxInfinityBudgetConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFlux_lower_branchPayload_infinity {d : ℕ} [NeZero d] (hd : 2 ≤ d) {Clow : ℝ} (hClow : 0 < Clow) (haux : profileAuxiliaryConst d ≤ Clow) (hdet : 2 * superposedFluxSharpDetConst d ≤ Clow) (hbudgetChoice : superposedFluxInfinityBudgetConst d + 6 ≤ superposedFluxBfaRate d * Clow) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) : Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), ∃ (Ydet : Cutoff.CutoffSample d → ℝ) (Y : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → Observable.cutoffLowerEllipticityInv M m L s ⋯ CoarseEllipticityExponent.infinity omega * ↑(Annealed.sigmaBar M (m - 1)) ≤ Ydet omega + Y omega) ∧ (∀ (omega : Cutoff.CutoffSample d), Ydet omega ≤ Clow) ∧ Measurable Y ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) Y (Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

A payload-valued helper for the conditional infinity-exponent A.