ShellBounds

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

The single-shell stream bounds of ABK26

This module proves the first two displays in the proof of ABK26's stream increment lemma: the value bound e.jk.O and the derivative bound e.nabla.jk.O. Both are obtained from the frozen assumption (J2) transported through the frozen marginal scaling law e.diff.law.shift, exactly as in the source.

The two source displays are, for every k ∈ ℤ,

• ‖j_k‖_{L∞(cu_k)} = O_{Γ₂}(3^{γk}) (ABK26), and
• ‖∇j_k‖_{L∞(cu_k)} + 3^k ‖∇²j_k‖_{L∞(cu_k)} = O_{Γ₂}(^{(γ-1)k}) (ABK26).

Here ‖j_k‖_{L∞(cu_k)} is Algsuperdiff.Section3.Cutoff.localCubeControl k applied to the shell at index k, and the two derivative suprema are localCubeDerivNorm k and localCubeSecondDerivNorm k. The amplitudes below are the literal source amplitudes with constant 1: the J2 normalization e.kn.reg.ass.with.gamma (ABK26) weights the derivative terms by √d ≥ 1 and d ≥ 1, so no dimensional constant is needed. In particular the conclusions are at least as strong as the source's C(d) form.

Main results

• isBigOWith_gammaSigma_localCubeControl_shell: e.jk.O.
• isBigOWith_gammaSigma_shellDerivGauge: e.nabla.jk.O.
• isBigOWith_gammaSigma_shellDerivGauge_cube: the same estimate measured on any smaller origin cube cu_ell with ell ≤ k, which is the form consumed by the increment estimate.

References

• ABK26.
• ABK26, e.kn.reg.ass.with.gamma.

The J2 tail under the zero-shell marginal law

theorem Algsuperdiff.Section3.Provider.Stream.zeroShell_j2Observable_gaussian_tail {d : ℕ} (M : ABKModel d) (t : ℝ) (ht : 1 ≤ t) : ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) {j : Frozen.Assumptions.ShellField d | t < Frozen.Assumptions.ShellField.j2Observable d j} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))

The frozen (J2) Gaussian tail, read under the exact zero-shell marginal law.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_zeroShell_j2Observable {d : ℕ} (M : ABKModel d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)) (HCPolySupport.IndependentSums.gammaSigma 2) (Frozen.Assumptions.ShellField.j2Observable d) 1

The J2 observable has a unit-scale Γ₂ tail under the zero-shell law.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_zeroShell_unitCubeValueNorm {d : ℕ} (M : ABKModel d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)) (HCPolySupport.IndependentSums.gammaSigma 2) Frozen.Assumptions.ShellField.unitCubeValueNorm 1

The unit-cube value norm has a unit-scale Γ₂ tail under the zero-shell law.

theorem Algsuperdiff.Section3.Provider.Stream.unitCubeDerivNorm_add_unitCubeSecondDerivNorm_le_j2Observable {d : ℕ} (hd : 1 ≤ d) (j : Frozen.Assumptions.ShellField d) : j.unitCubeDerivNorm + j.unitCubeSecondDerivNorm ≤ Frozen.Assumptions.ShellField.j2Observable d j

In dimension d ≥ 1 the unweighted sum of the two J2 derivative norms is dominated by the J2 observable itself, because the source weights √d and d are at least one. This is why the derivative display below carries no dimensional constant.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_zeroShell_unitCubeDerivSum {d : ℕ} (M : ABKModel d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (j : Frozen.Assumptions.ShellField d) => j.unitCubeDerivNorm + j.unitCubeSecondDerivNorm) 1

The unweighted sum of the two J2 derivative norms has a unit-scale Γ₂ tail under the zero-shell law.

e.jk.O: the value display

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_localCubeControl_shell {d : ℕ} (M : ABKModel d) (k : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => Cutoff.localCubeControl k (omega k)) (Real.rpow 3 (M.gamma * ↑k))

ABK26's e.jk.O: under the canonical shell-sequence law, ‖j_k‖_{L∞(cu_k)} ≤ O_{Γ₂}(3^{γk}). The amplitude is the source amplitude with constant 1.

e.nabla.jk.O: the derivative display

theorem Algsuperdiff.Section3.Provider.Stream.shellDerivGauge_nonneg {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) : 0 ≤ localCubeDerivNorm ell j + 3 ^ ell * localCubeSecondDerivNorm ell j

The shell derivative gauge is nonnegative.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_shellDerivGauge {d : ℕ} (ell : ℤ) : Measurable fun (j : Frozen.Assumptions.ShellField d) => localCubeDerivNorm ell j + 3 ^ ell * localCubeSecondDerivNorm ell j

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivGauge {d : ℕ} (M : ABKModel d) (k : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => localCubeDerivNorm k (omega k) + 3 ^ k * localCubeSecondDerivNorm k (omega k)) (Real.rpow 3 ((M.gamma - 1) * ↑k))

ABK26's e.nabla.jk.O: under the canonical shell-sequence law, ‖∇j_k‖_{L∞(cu_k)} + 3^k ‖∇²j_k‖_{L∞(cu_k)} ≤ O_{Γ₂}(3^{(γ-1)k}). The source states the amplitude with a dimensional constant C(d); the exact J2 normalization gives it with constant 1.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivGauge_cube {d : ℕ} (M : ABKModel d) {ell k : ℤ} (h : ell ≤ k) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => localCubeDerivNorm ell (omega k) + 3 ^ ell * localCubeSecondDerivNorm ell (omega k)) (Real.rpow 3 ((M.gamma - 1) * ↑k))

The derivative display measured on a smaller origin cube. For ell ≤ k the cube cu_ell is contained in cu_k, so the shell at index k obeys the same Γ₂ bound there; this is the form summed in ABK26's e.nabla.km.kn.infty.