ComparisonErrorBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit rounding and normality errors fit inside the strict-slack saving.

lemma OAI.TotientAsymptotic.collisionMesh_eq_sqrt_ratio line 13
lemma OAI.TotientAsymptotic.sum_a_le_square line 19
lemma OAI.TotientAsymptotic.comparison_log_sum_bound line 27
lemma OAI.TotientAsymptotic.grid_error_polynomial_bound line 47

theorem OAI.TotientAsymptotic.comparison_grid_error_absorbed line 73

Source documentation

The exponent loss from the paired grid and normality consumes at most a quarter of the available h⁻⁴ strict slack.

theorem comparison_grid_error_absorbed {b h : ℕ} {δ : ℝ}
    (hbh : b ≤ h) (hh : 2 ≤ h) (hδ : 0 ≤ δ) (hδu : δ ≤ 2/(h : ℝ)^32) :
    ((2*(b : ℝ)+3)*δ)*(∑ j ∈ Finset.Icc 1 b, a j)+
      2*b*((2*(b : ℝ)+3)*δ)+δ*(∑ j ∈ Finset.Icc 2 b, ((j : ℝ)*Real.log j+j)) ≤
      1/(4*(h : ℝ)^4) := by
…

Mentions: OAI.TotientAsymptotic.a