CstarUpperBound

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

An absolute upper bound on the shell constant cstar

ABK26 states, immediately after assumption (J4), that the normalized Gaussian tail e.kn.reg.ass of (J2) and the non-degeneracy identity e.nondeg of (J4) "together imply c_star <= 1". This module proves the corresponding Lean bound from the two frozen assumptions alone.

The argument

e.nondeg says that c_star (log 3) is the second moment of the potential part of the origin forcing j_0 e. Orthogonal projections are norm contractions, so

c_star (log 3) <= E[ |j_0(0) e|^2 ] <= E[ ||j_0(0)||_op^2 ] <= E[ X^2 ] ,

where X is the exact J2 observable ||j_0||_{L^inf(cu_0)} + sqrt d ||grad j_0||_{L^inf(cu_0)} + d ||grad^2 j_0||_{L^inf(cu_0)}. The J2 tail P[X > t] <= exp(-t^2) for t >= 1 gives, by the layer-cake formula,

E[X^2] = int_0^inf P[X^2 > t] dt <= 1 + int_1^inf exp(-t) dt = 1 + e^{-1} ,

whence c_star <= (1 + e^{-1}) / log 3 = 1.2451..., in particular the clean absolute bound c_star <= 3/2.

The constant obtained here is absolute: it depends on neither the dimension nor any model parameter. It is slightly weaker than the manuscript's own c_star <= 1; sharpening it to 1 would need more than the frozen tail (the tail is only assumed above level one, and E[X^2] <= 1 + e^{-1} is sharp for that information).

Main results

• integral_sq_le_of_gaussian_tail: the second-moment bound E[X^2] <= 1 + e^{-1} for any nonnegative observable with the normalized J2 tail.
• cstar_mul_log_three_le: c_star (log 3) <= 1 + e^{-1}, the sharp form.
• cstar_le_three_halves: the absolute bound c_star <= 3/2.

References

• ABK26, e.kn.reg.ass, e.nondeg and the remark.

The second moment of a normalized Gaussian tail

theorem Algsuperdiff.Section3.Provider.Disorder.integral_sq_le_of_gaussian_tail {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℝ} (hXmeas : Measurable X) (hXnonneg : ∀ (omega : Omega), 0 ≤ X omega) (htail : ∀ (t : ℝ), 1 ≤ t → mu {omega : Omega | t < X omega} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))) : ∫ (omega : Omega), X omega ^ 2 ∂mu ≤ 1 + Real.exp (-1)

The second-moment bound behind c_star <= 1. A nonnegative measurable observable on a probability space whose upper tail obeys the normalized Gaussian bound P[X > t] <= exp(-t^2) for t >= 1 has second moment at most 1 + e^{-1}.

The two contributions are the trivial one below level one and the layer-cake integral int_1^inf exp(-t) dt = e^{-1} above it.

The origin forcing energy

The bound

theorem Algsuperdiff.Section3.Provider.Disorder.cstar_mul_log_three_le {d : ℕ} (M : ABKModel d) : Disorder.cstar M * Real.log 3 ≤ 1 + Real.exp (-1)

The sharp form of the manuscript's remark. The J4 normalization c_star (log 3) of e.nondeg is at most the second moment 1 + e^{-1} allowed by the J2 tail e.kn.reg.ass.

theorem Algsuperdiff.Section3.Provider.Disorder.cstar_le_three_halves {d : ℕ} (M : ABKModel d) : Disorder.cstar M ≤ 3 / 2

The dimension-free gate constant. The shell constant of any standing ABK model is at most 3/2; the manuscript's own remark asserts the sharper c_star <= 1, which the frozen tail alone does not deliver.