IncrementOscillation

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

The literal increment oscillation gauge

ABK26's oscillation event e.Bosc.def is stated with the literal stream increment k_L - k_j: sup_{L >= j} 3^{2j} ||grad (k_L - k_j)||_{W^{1,infinity}(z + square_j)}.

That local measurability input is now proved. Algsuperdiff.Section3.Provider.Stream.shellIncrement is the increment as a genuine shell field (values literally k_L - k_j, by shellIncrement_apply_eq_cutoff_sub), and this module measures it in exactly the norm of e.Bosc.def:

incrementOscGauge Q L = 3^{2j} ||grad (k_L - k_j)||_{W^{1,infinity}(z+square_j)} = max { 3^{2j} ||grad² (k_L - k_j)||_{L∞}, 3^{j} ||grad (k_L - k_j)||_{L∞} },

the same shape as shellOscGauge (ABK26, the volume-normalized Sobolev norm; the factor |U|^{-1/d} of a cube of side 3^j is 3^{-j}).

Main definitions

• incrementOscGauge: the literal e.Bosc.def gauge at the cube Q and scale L.

Main results

• incrementOscGauge_le_sum_shellOscGauge: the W^{1,infinity} triangle inequality along the shell decomposition of the increment.
• incrementOscGauge_le_oscThreshold: the complement control of e.Bosc.def. On the complement of badOsc M Q, for every L >= Q.scale, 3^{2j} ||grad (k_L - k_j)||_{W^{1,infinity}(z+square_j)} <= delta_osc c_star^{1/2} gamma^{-1/2} 3^{gamma j}.
• sqrt_cstar_mul_inv_sqrt_gamma_mul_rpow_le_two_mul_sigmaBar: the constant chain of ABK26, consuming the induction-state clause e.shom.h.bounds: c_star^{1/2} gamma^{-1/2} 3^{gamma m} <= 2 sigmabar_m.

References

• ABK26, e.Bosc.def, e.BoscL.def, e.Bosc.decomp.
• ABK26, p.bfA.multiscalebound, e.we.can.apply.cg.
• ABK26 (the volume-normalized Sobolev norms).

The literal increment gauge

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.incrementOscGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (L : ℤ) : Cutoff.CutoffSample d → ℝ

The literal left-hand side of e.Bosc.def: 3^{2j} ||grad (k_L - k_j)||_{W^{1,infinity}(z + square_j)} at the cube Q with j = Q.scale, measured on the honest shell-field realization of the increment k_L - k_j.

Equations

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

The W^{1,infinity} triangle inequality along shells

theorem Algsuperdiff.Section3.Provider.BadEvents.incrementOscGauge_le_sum_shellOscGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (L : ℤ) (omega : Cutoff.CutoffSample d) : incrementOscGauge Q L omega ≤ ∑ k ∈ Finset.Ioc Q.scale L, shellOscGauge Q k omega

The literal increment gauge is bounded by the sum of the single-shell gauges of e.BoscL.def over the shells that make up the increment.

The complement control of e.Bosc.def

theorem Algsuperdiff.Section3.Provider.BadEvents.incrementOscGauge_le_oscThreshold {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {omega : Cutoff.CutoffSample d} (homega : omega ∉ badOsc M Q) {L : ℤ} (hL : Q.scale ≤ L) : incrementOscGauge Q L omega ≤ oscThreshold M Q.scale

The manuscript's e.Bosc.def complement control, now for the literal increment: on the complement of badOsc M Q, for every scale L >= Q.scale,

3^{2j} ||grad (k_L - k_j)||_{W^{1,infinity}(z + square_j)} <= delta_osc c_star^{1/2} gamma^{-1/2} 3^{gamma j}.

The constant chain of ABK26

theorem Algsuperdiff.Section3.Provider.BadEvents.sqrt_cstar_mul_inv_sqrt_gamma_mul_rpow_le_two_mul_sigmaBar {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {m : ℤ} (hm : m ≤ m0) : √(Disorder.cstar M) * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑m) ≤ 2 * ↑(Annealed.sigmaBar M m)

The induction-state clause e.shom.h.bounds gives c_star^{1/2} gamma^{-1/2} 3^{gamma m} <= 2 sigmabar_m.