PPTGridError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The PPT grid uses a mesh of order (log t)^5 / sqrt t, where t is the double logarithm of the comparison scale. With logarithmically many coordinates its rounding and normality errors fit inside the constructed inverse-cube row margin.

lemma OAI.TotientAsymptotic.ppt_grid_error_polynomial_bound line 21

Source documentation

A direct bound for the three terms charged to the comparison exponent. The two grid widths may differ, as in Ford's PPT construction.

lemma ppt_grid_error_polynomial_bound {b H : ℕ} {e w η δ : ℝ}
    (hH : 1 ≤ H) (hbH : b ≤ H) (hδ : 0 ≤ δ)
    (he : e ≤ (2*(b : ℝ)+4)*δ) (hw : w ≤ (4*(b : ℝ)+3)*δ)
    (hη : η ≤ δ) :
    e*(∑ j ∈ Finset.Icc 1 (b-1), a j)+2*(b-1 : ℕ)*w+
      η*(∑ i ∈ Finset.Icc 2 b, ((i : ℝ)*Real.log i+i)) ≤
        32*(H : ℝ)^3*δ := by
…

Mentions: OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.a

theorem OAI.TotientAsymptotic.ppt_log_dimension_mesh_budget line 74

Source documentation

The logarithmic dimension range is uniform in the integer dimension. Its sixth power is absorbed by the square-root denominator of the mesh.

theorem ppt_log_dimension_mesh_budget {C : ℝ} (_hC : 0 < C) :
    ∀ᶠ t : ℝ in atTop, ∀ H : ℕ,
      1 ≤ H → (H : ℝ) ≤ C*Real.log t →
      32*(H : ℝ)^3*((Real.log t)^5/Real.sqrt t) ≤
        1/(80*(H : ℝ)^3) := by
…

theorem OAI.TotientAsymptotic.ppt_grid_error_absorbed line 108

Source documentation

All error terms fit below the exact row margin for every row index whose remaining dimension is bounded by H.

theorem ppt_grid_error_absorbed {C : ℝ} (hC : 0 < C) :
    ∀ᶠ t : ℝ in atTop, ∀ (b H r : ℕ) (e w η δ : ℝ),
      1 ≤ H → b ≤ H → r+1 ≤ H → (H : ℝ) ≤ C*Real.log t →
      0 ≤ δ → δ ≤ (Real.log t)^5/Real.sqrt t →
      e ≤ (2*(b : ℝ)+4)*δ → w ≤ (4*(b : ℝ)+3)*δ → η ≤ δ →
      e*(∑ j ∈ Finset.Icc 1 (b-1), a j)+2*(b-1 : ℕ)*w+
        η*(∑ i ∈ Finset.Icc 2 b, ((i : ℝ)*Real.log i+i)) ≤
          rowContractionError r/16 := by
…

Mentions: OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.rowContractionError