Local-Gap Fixed-n Layer

This file contains the fixed-n fallback argument used by cor_uniform.

The public theorem a reader should inspect first is:

• fixed_n_count_asymptotic

The staged bridge lemmas and the primary-box telescope are implementation detail for that endpoint.

def fixedCountDelta (t : ℕ) : ℝ

Equations

• fixedCountDelta t = ↑(max t 1) ^ (-(2 / 5))

theorem const_mul_nat_rpow_mul_exp_neg_mul_nat_rpow_eventually_le (K s a p ε : ℝ) (hK : 0 ≤ K) (ha : 0 < a) (hp : 0 < p) (hε : 0 < ε) : ∀ᶠ (t : ℕ) in Filter.atTop, K * ↑t ^ s * Real.exp (-a * ↑t ^ p) ≤ ε

theorem fixed_n_normalizedCount_asymptotic (n : ℕ) (hn : 2 ≤ n) : Filter.Tendsto (fun (t : ℕ) => normalizedCount n (4 * t) / gaussianScale n ↑t) Filter.atTop (nhds 1)

Fixed-n normalized-count asymptotic, replacing the external DL10 patch on the normalized-count side.

theorem fixed_n_count_asymptotic (n : ℕ) (hn : 2 ≤ n) : Filter.Tendsto (fun (t : ℕ) => ↑(hadamardCount n (4 * t)) / countScale n t) Filter.atTop (nhds 1)

Fixed-n count asymptotic for the small-dimension branch of cor_uniform.