OscillationProbability

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

The scale-resolved oscillation probability bound

This module proves the oscillation branch of ABK26's Lemma l.bad.event.probabilities (statement, proof Step 2): for every integer scale j, every centre z in 3^j Z^d and every L >= j,

P[ B_{osc,L}(z + square_j) ] <= exp( - c E^{-2} gamma^{-1} 3^{(3/2)(L-j)} ) .

The proof, and what each step uses

Step 2 of the manuscript's proof reads: by e.nabla.jk.O and e.maxy.bound, 3^{2j} ||grad j_L||_{W^{1,infinity}(z+square_j)} <= O_{Gamma_2}(^{gamma L - (L-j)}); comparing with the e.BoscL.def threshold gives exp(-c c_star gamma^{-1} 3^{2(4/5 - gamma)(L-j)}), and then gamma <= 1/20 converts the exponent 2(4/5 - gamma) into 3/2.

Here the first display is shellOscGauge_le_shellDerivGauge together with the proved translated single-shell gauge Provider.Stream.isBigOWith_gammaSigma_shellDerivGauge_cube_translate (e.nabla.jk.O at the base point z) transported to the cutoff sample law by Provider.Stream.isBigOWith_cutoffSampleLaw_comp_val. No maximum over centres is taken, so e.maxy.bound (l.maximums.Gamma.s) is not needed at this point: the translated law of a single shell already carries the amplitude of the centered one. The constant C of the manuscript's display is 1 here.

Admissibility

The tail hypothesis of a weak-Orlicz bound is only available above the amplitude, so the threshold-to-amplitude ratio must be at least one. That is exactly the content of unitGate, and unitGate_of_admissible derives it from the manuscript's own admissibility e.bad.event.admissibility.prelim with the dimension-only choice C(d) := 25 / delta_osc(d)^2, so nothing is added to the source hypotheses.

The conversion of 2(4/5 - gamma) into 3/2 needs gamma <= 1/20, which the manuscript's proof uses ("where we used gamma <= 1/20 in the last step").

Main results

• measureReal_badOscAt_le: the sharp bound, exponent 2(4/5 - gamma)(L-j).
• measureReal_badOscAt_le_printed: the manuscript's display e.BoscL.prob.

References

• ABK26, l.bad.event.probabilities.
• ABK26, e.nabla.jk.O.

The admissibility gate

def Algsuperdiff.Section3.Provider.BadEvents.unitGate {d : ℕ} (M : ABKModel d) : Prop

The threshold-to-amplitude gate of the weak-Orlicz tail: the e.BoscL.def threshold at L = j is at least the amplitude of e.nabla.jk.O.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.unitGate M = (1 ≤ 1 / 5 * Algsuperdiff.Section3.Provider.BadEvents.deltaOsc d * √(Algsuperdiff.Section3.Disorder.cstar M) * (√M.gamma)⁻¹)

The tail of the single-shell oscillation gauge

theorem Algsuperdiff.Section3.Provider.BadEvents.isBigOWith_gammaSigma_shellOscGauge {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {L : ℤ} (hL : Q.scale ≤ L) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (shellOscGauge Q L) (3 ^ ↑Q.scale * 3 ^ ((M.gamma - 1) * ↑L))

e.nabla.jk.O at the base point of Q, transported to the cutoff sample law and rescaled into the e.BoscL.def gauge: the manuscript's display 3^{2j} ||grad j_L||_{W^{1,infinity}(z+square_j)} <= O_{Gamma_2}(3^{gamma L - (L-j)}), with constant one.

The probability bound

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_badOscAt_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {L : ℤ} (hL : Q.scale ≤ L) (hgate : unitGate M) : (↑(Cutoff.cutoffSampleLaw M)).real (badOscAt M Q L) ≤ Real.exp (-(1 / 25 * deltaOsc d ^ 2 * Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * (4 / 5 - M.gamma) * (↑L - ↑Q.scale))))

The sharp form of ABK26 e.BoscL.prob: the exponent carries the honest rate 2(4/5 - gamma)(L-j) and the explicit constant delta_osc(d)^2 / 25.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_badOscAt_le_printed {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {L : ℤ} (hL : Q.scale ≤ L) (hgate : unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) {E : ℝ} (hEc : E⁻¹ ^ 2 ≤ Disorder.cstar M) : (↑(Cutoff.cutoffSampleLaw M)).real (badOscAt M Q L) ≤ Real.exp (-(1 / 25 * deltaOsc d ^ 2 * E⁻¹ ^ 2 * M.gamma⁻¹ * 3 ^ (3 / 2 * (↑L - ↑Q.scale))))

ABK26's displayed oscillation bound e.BoscL.prob:

P[ B_{osc,L}(z + square_j) ] <= exp( - c E^{-2} gamma^{-1} 3^{(3/2)(L-j)} ) ,

with c = delta_osc(d)^2 / 25.

hgamma20 is the manuscript's own proof-side gate gamma <= 1/20; hEc is the consequence E^{-2} <= c_star of the printed admissibility E >= C c_star^{-1} for any C >= 1 and E >= 1.