SuperposedFluxLocalPayoffAE

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

Unconditional a.e. local lower payoff

The priced all-cutoff payoff has a target independent of its separation depth H and wave amplitude t. This file chooses the explicit sequence H_j = j + 1, t_j = sqrt (j + 1) and proves that both terms of the price vanish. It then bounds the outer measure of the target's failure set by every price in the sequence. This does not require the target itself to be measurable and never promotes an almost-everywhere assertion to a pointwise one.

The resulting one-cube payoff is intersected over the finite descendant grid, and the local random lane is replaced by its honest finite-grid maximum. A final producer pairs this a.e. payoff with the existing direct-gate Orlicz certificate. Its exponent upper gate remains explicit because the payoff hypotheses do not imply it.

def Algsuperdiff.Section3.Provider.CoarseEllipticity.allLPriceLimitDepth (j : ℕ) : ℕ

Separation depth in the explicit zero-price limiting sequence.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.allLPriceLimitDepth j = j + 1

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.allLPriceLimitAmplitude (j : ℕ) : ℝ

Wave amplitude in the explicit zero-price limiting sequence.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.allLPriceLimitAmplitude j = √(↑j + 1)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tendsto_randomHsepAllLWavePrice_limitSequence {sigma b : ℝ} (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) : Filter.Tendsto (fun (j : ℕ) => Multiscale.randomHsepAllLWavePrice sigma b (allLPriceLimitDepth j) (allLPriceLimitAmplitude j)) Filter.atTop (nhds 0)

Along H_j = j + 1 and t_j = sqrt (j + 1), the all-cutoff price tends to zero. The wave term is polynomial times exponential decay, while the separation term is double-exponential.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLocalConst_pos {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n i : ℤ) (eps beta : ℝ) (k₀ kp : ℕ) : 0 < superposedFluxLocalConst M n i eps beta k₀ kp

The finite pure-flux coordinate sum is strictly positive in positive dimension, so the shifted local payoff constant meets the strict scale premise of the bfa Orlicz A.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measureReal_not_randomHsepAllLWaveEnvelope_translate_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {n : ℤ} {E sigma b : ℝ} (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (n - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) (k₀ : ℕ) {L₀ : ℤ} (hnL₀ : n ≤ L₀) {H : ℕ} (hH : 1 ≤ H) {t : ℝ} (ht : 1 ≤ t) (z : HCPolySupport.Vec d) : (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | ¬Multiscale.randomHsepAllLWaveEnvelope M n E b k₀ L₀ t (Cutoff.translateCutoffSample z omega)} ≤ Multiscale.randomHsepAllLWavePrice sigma b H t

Stationarity transports the all-cutoff wave failure bound to an arbitrary real translation. Measurability is supplied by the literal wave event.