OscillationBranchLow

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

The oscillation branch of l.bad.event.lemma at n < m

BadEventLemmaOscillation.lean supplies a local result associated with ABK26's e.oscillation.bound on the branch m <= n, where the increment base sits at or above the cube scale. This module supplies a local result for the other branch, n < m, on which

• the increment k_L - k_n contains shells k in (n, m) strictly below the cube scale, and
• the displayed exponent carries the factor 3^{-5 (m-n)_+}.

The conclusion is the manuscript's own display at (n-m)_+ = 0,

P[ sensitivity clause of Q(m,n,z) fails ]  <=  exp( - c c_star gamma^{-1} 3^{-5(m-n)} ) .

The two corrections this branch runs under

• The printed wave/shell inclusion is invalid on this branch: for L in [n, m) the partial increment k_L - k_n is dominated neither by k_m - k_n nor by any shell above m. The correction recorded there is to price the shell sum sum_{k = n+1}^{m} ||grad j_k|| instead, which is what e.W.1.inf.bound bounds.
• On this branch the printed bound is not derivable from the cited inputs at the printed admissibility for unrestricted m; the correction is the self-consistent restriction

  3^{5 (m-n)_+}  <=  c c_star gamma^{-1} ,
  

  i.e. the display's own exponent is at least one. It is carried here by the binder hrestrict : 1 <= badEventOscFullRate M Ccg Q n, which is literally that inequality, and it is the only hypothesis of this module beyond the manuscript's own data. Every manuscript use satisfies it.

The two ingredients

1. The weight conversion shellOscGauge_le_translatedLargeCubeDerivGauge: for k <= m,

   3^{2m} ||grad j_k||_{W^{1,infinity}(z+square_m)}
     <=  3^{2(m-k)} ( 3^k ||grad j_k||_{L^infinity(z+square_m)}
                      + 3^{2k} ||grad^2 j_k||_{L^infinity(z+square_m)} ) ,
   

   the intrinsic factor between the e.BoscL.def gauge at cube scale m and the e.W.1.inf.bound summand of a shell at scale k < m.
2. The translated e.W1inf.jL.bound.smaller Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_lt_translate.

Above the cube scale the proved per-shell tail isBigOWith_gammaSigma_shellOscGauge (e.nabla.jk.O at the base point of Q) is used, exactly as on the branch m <= n.

The constant

c of the display is chosen as badEventOscLowConst d Ccg, the constant of the branch m <= n further divided by (1 or C_{(e.W1inf.jL.bound.smaller)})^2, where the latter is the dimension-only covering constant Provider.Stream.shellW1InfSmallerConst d. Both factors are dimension-only, so the manuscript's requirement that c depends only on d is respected.

Main definitions

• badEventOscLowConst: the constant of e.oscillation.bound on this branch.
• badEventOscFullRate: the exponent of e.oscillation.bound over the whole range, c c_star gamma^{-1} 3^{-5(m-n)_+} 3^{(n-m)_+}.

Main results

• shellOscGauge_le_translatedLargeCubeDerivGauge (the weight conversion).
• measureReal_shellSensitivityFailure_le_low (one shell, either regime).
• measureReal_goodLocalSensitivityFailure_le_low (the branch n < m).

References

• ABK26, l.bad.event.lemma; e.oscillation.bound; the wave decomposition.
• ABK26, e.W.1.inf.bound; e.nabla.jk.O.

Elementary numerics

theorem Algsuperdiff.Section3.Provider.BadEvents.shellOscGauge_le_translatedLargeCubeDerivGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (omega : Cutoff.CutoffSample d) : shellOscGauge Q k omega ≤ 3 ^ (2 * (Q.scale - k)) * Stream.largeCubeDerivGauge Q.scale k (Frozen.Assumptions.ShellField.translate (cubeBasePoint Q) (↑omega k))

The constant and the exponent

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.badEventOscLowConst (d : ℕ) (Ccg : ℝ) : ℝ

The local choice of the manuscript's c in e.oscillation.bound valid on both branches: the constant badEventOscConst of the branch m <= n, divided by the square of the dimension-only covering constant (1 or C_{(e.W1inf.jL.bound.smaller)}) that the shells below the cube scale cost.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.badEventOscLowConst_pos {Ccg : ℝ} (hCcg : 0 < Ccg) (d : ℕ) : 0 < badEventOscLowConst d Ccg

theorem Algsuperdiff.Section3.Provider.BadEvents.badEventOscLowConst_le_badEventOscConst {Ccg : ℝ} (hCcg : 0 < Ccg) (d : ℕ) : badEventOscLowConst d Ccg ≤ badEventOscConst d Ccg

The branch constant is below the constant of the branch m <= n, so the proved bound on that branch implies the same bound at this constant.

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.badEventOscFullRate {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : ℝ

The exponent of e.oscillation.bound over the whole range of m, n (ABK26): c c_star gamma^{-1} 3^{-5 (m-n)_+} 3^{(n-m)_+}.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.badEventOscFullRate_of_lt {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) {n : ℤ} (h : n < Q.scale) : badEventOscFullRate M Ccg Q n = badEventOscLowConst d Ccg * Disorder.cstar M * M.gamma⁻¹ * 3 ^ (-5 * (↑Q.scale - ↑n))

On the branch n < m the full exponent is the printed c c_star gamma^{-1} 3^{-5(m-n)}.

theorem Algsuperdiff.Section3.Provider.BadEvents.badEventOscFullRate_le_badEventOscRate {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n : ℤ} (h : Q.scale ≤ n) : badEventOscFullRate M Ccg Q n ≤ badEventOscRate M Ccg Q n

On the branch m <= n the full exponent is below the proved rate badEventOscRate.

The two abstract threshold comparisons

The per-shell probability bound on the branch n < m

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_shellSensitivityFailure_le_low {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n k m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m0 - 1) E) (hn : n ≤ m0 - 1) (hmn : n < Q.scale) (hnk : n < k) (hrestrict : 1 ≤ badEventOscFullRate M Ccg Q n) : (↑(Cutoff.cutoffSampleLaw M)).real (shellSensitivityFailure M Ccg Q n k) ≤ Real.exp (-(badEventOscFullRate M Ccg Q n * 3 ^ (↑k - ↑n)))

One shell of the oscillation branch at n < m. For every shell k > n the probability that j_k exceeds its share of the e.good.local.events threshold is at most exp(- rate 3^{k-n}), where rate is the exponent badEventOscFullRate of e.oscillation.bound.

Shells at or above the cube scale are priced by the proved translated e.nabla.jk.O tail isBigOWith_gammaSigma_shellOscGauge; shells strictly below it are priced by the translated e.W1inf.jL.bound.smaller (Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_lt_translate) after the weight conversion shellOscGauge_le_translatedLargeCubeDerivGauge — this is the shell-sum pricing.

hrestrict is the restriction.

The oscillation branch at n < m

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_goodLocalSensitivityFailure_le_low {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m0 - 1) E) (hn : n ≤ m0 - 1) (hmn : n < Q.scale) (hrestrict : 1 ≤ badEventOscFullRate M Ccg Q n) : (↑(Cutoff.cutoffSampleLaw M)).real (goodLocalSensitivityFailure M Ccg Q n) ≤ Real.exp (-badEventOscFullRate M Ccg Q n)

The oscillation branch of l.bad.event.lemma at n < m (ABK26, e.oscillation.bound), where (n-m)_+ = 0:

P[ sensitivity clause of Q(m,n,z) fails ]
  <= exp( - c c_star gamma^{-1} 3^{-5(m-n)} ) ,

with c = badEventOscLowConst d Ccg, dimension-only.

It is the only hypothesis beyond the manuscript's own data, and it is also exactly the gate that the weak-Orlicz tail and the geometric summation need.