Uniform estimates on all finite boundary arcs #

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.arc_width_bound {n v s : ℝ} (hn : 1 ≤ n) (_hv : 0 ≤ v) (hs : 0 ≤ s) (hnv : n * (n + 1) * v ≤ 1 / 2) (hns : 1 ≤ (n + 1) * s) :

v ≤ s ^ 2

The spline width is quadratically small, uniformly in its integer index.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.source_moment_estimates {k ell delta s : ℝ} (hk : 0 ≤ k) (hs : 0 ≤ s) (hs1 : s ≤ 1) (he : s = 2 * ell + delta) (hv : |delta| ≤ s ^ 2) (hkv : k * |delta| ≤ 1 / 2) :

have m := ell + k * delta * |delta|; have q := ell * (2 * m - ell) + 2 / 3 * k * |delta| ^ 3; 0 ≤ m ∧ m ≤ s ∧ |m - s / 2| ≤ s ^ 2 / 2 ∧ |q - s ^ 2 / 4| ≤ 2 * s ^ 3

First and second distance moments have uniform quadratic/cubic errors.

Documentation