HolderGagliardoRangeGuard #

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

The `s < 1/2` range guard and the `(1-2s)^{-1/2}` constant #

The target #

The C^{0,1/2} ⊂ H^s embedding used by l.excess.decay.good.scales and by t.regularity Step 4 holds only for s < 1/2, with constant ~ (1-2s)^{-1/2}·3^{(1/2-s)n} — a factor absent from the printed excess-decay constant. This module makes that constant explicit and machine-checked in the development's own carrier:

  C_{S4.4}(d,s) := ( C_rad(d, d+2s-1) )^{1/2}
                 ≤ ( 2^{d+1} 3^{d} / (1-2s) )^{1/2}
                 = 2^{(d+1)/2} 3^{d/2} (1-2s)^{-1/2}          (0 < s < 1/2),

The s-free form at the §4.4/§4.5 gate s ≤ 1/4, where 1 - 2s ≥ 1/2 and the right-hand side collapses to ( 2^{d+2} 3^{d} )^{1/2}, is read off this bound downstream, in the §4.5 data embedding.

The only analytic content is the elementary lower bound 1 - 3^{-t} ≥ t/2 on t ∈ [0,1], which is Bernoulli's inequality for exponents in [0,1] (the chord bound for t ↦ 3^{-t}); t := 1 - 2s is exactly the gap to the endpoint.

References #

ABK26, (l.excess.decay.good.scales, the printed range s ∈ [8γ, 1/2]), (the s := 1/4 pin).

1. The Step-4 seminorm constant #

source

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepFourGagliardoConst (d : ℕ) (s : ℝ) :

ℝ

C_{S4.4}(d,s) = ( C_rad(d, d+2s-1) )^{1/2}, the constant of the C^{0,1/2} ↪ H^s atom once the scale weight R^{1/2-s} is factored out.

Equations

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

Instances For

source

theorem Algsuperdiff.Section4.Provider.Regularity.stepFourGagliardoConst_nonneg (d : ℕ) (s : ℝ) :

0 ≤ stepFourGagliardoConst d s

2. The elementary gap estimate `1 - 3^{-t} ≥ t/2` #

source

theorem Algsuperdiff.Section4.Provider.Regularity.half_le_one_sub_three_rpow_neg {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :

t / 2 ≤ 1 - 3 ^ (-t)

The gap estimate. For 0 ≤ t ≤ 1, 1 - 3^{-t} ≥ t/2.

This is the quantitative form of "the Gagliardo integral converges with room at s < 1/2": at t = 1 - 2s the left side is the denominator of radialKernelConst, so the constant blows up at most like 2/(1-2s). The proof is Bernoulli's inequality for exponents in [0,1] (the chord bound for the convex function t ↦ 3^{-t} on [0,1], whose endpoints are 1 and 1/3); it needs no numerical bound on log 3.