ComparisonExponentSaving.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The complete gridding error still leaves half of the strict exponent saving.

lemma OAI.TotientAsymptotic.collisionMesh_le_quarter_slack line 12

theorem OAI.TotientAsymptotic.comparison_exponent_saving line 28

Source documentation

The extra endpoint normalization costs at most one mesh unit. Together with every grid-width and normality term, it leaves exponent -1-1/(2h^4).

theorem comparison_exponent_saving {b h : ℕ} {y S δ : ℝ} {Y U : ℕ → ℝ}
    (hbh : b≤h) (hh : 2≤h) (hδ : 0≤δ) (hδu : δ≤2/(h : ℝ)^32)
    (hmesh : Real.sqrt (B S/B y)=δ)
    (hweighted : (∑ j ∈ Finset.Icc 1 (b-1), a j*(B (Y j)/B y)) ≤
      1-1/(h : ℝ)^4+δ+((2*(b : ℝ)+3)*δ)*(∑ j ∈ Finset.Icc 1 b, a j))
    (hwidth : ∀ j ∈ Finset.Icc 1 (b-1), B (Y j)/B y-B (U j)/B y≤(2*(b : ℝ)+3)*δ) :
    -2+(∑ j ∈ Finset.Icc 1 (b-1), a j*(B (Y j)/B y))+comparisonError b y S Y U ≤
      -1-1/(2*(h : ℝ)^4) := by
…

Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.comparisonError