← Mathematical handbook

theorem Verification.empiricalCDFRadius_scaled_bound (n : ℕ) : (↑n + 2) ^ (1 / 3) * empiricalCDFRadius n ≤ √(16 * Real.log (↑n + 2) / (↑n + 2) ^ (1 / 3))

theorem Verification.empiricalCDFRadius_scaled_tendsto : Filter.Tendsto (fun (n : ℕ) => (↑n + 2) ^ (1 / 3) * empiricalCDFRadius n) Filter.atTop (nhds 0)

theorem Verification.empiricalMesh_scaled_tendsto : Filter.Tendsto (fun (n : ℕ) => (↑n + 2) ^ (1 / 3) / (↑n + 1)) Filter.atTop (nhds 0)

theorem Verification.empiricalRankRate_scaled_tendsto : Filter.Tendsto (fun (n : ℕ) => (↑n + 2) ^ (1 / 3) * (3 * empiricalCDFRadius n + 8 / (↑n + 1))) Filter.atTop (nhds 0)