PPTNormalizedParameters.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The PPT construction has a first normalized cutoff approaching one. Its inverse-log-cube loss still implies the literal first-cutoff power bound in Ford's comparison lemma. No fixed bound such as ν₁ ≤ 4/5 is needed.

lemma OAI.TotientAsymptotic.ppt_log_loss_of_contracted_coordinate line 19

Source documentation

A contracting adjacent row leaves enough room for the grid and normality errors before checking the published first-cutoff bound.

lemma ppt_log_loss_of_contracted_coordinate {t ω e ν : ℝ}
    (ht : 0 < t) (hω : 0 < ω) (hω1 : ω ≤ 1)
    (hν : ν ≤ 1/(1+ω)+e) (herr : 4*e ≤ ω)
    (hbudget : 4*Real.log (10*t) ≤ t*ω) :
    Real.log (10*t) ≤ t*(1-ν) := by
…

lemma OAI.TotientAsymptotic.ppt_comparison_cutoff_power_of_log_loss line 32
lemma OAI.TotientAsymptotic.ppt_inverse_log_cube_cutoff_loss line 47
theorem OAI.TotientAsymptotic.ppt_comparison_cutoff_power_of_inverse_log_cube line 68

theorem OAI.TotientAsymptotic.ppt_ford_parameters_of_normalized_grid line 86

Source documentation

The first normalized cutoff is controlled by its actual logarithmic loss. All other assumptions are the literal Ford parameter restrictions expressed through normalized coordinates.

theorem ppt_ford_parameters_of_normalized_grid {z : ℝ} (hz : 1 < z)
    (hB : 0 < B z) (b D r : ℕ) (S : ℝ) (ν μ : ℕ → ℝ)
    (hb : 1 ≤ b) (hν : ν 0=1) (hS : Real.exp (Real.exp 1) ≤ S)
    (hSb : S ≤ comparisonCutoffs z ν b)
    (horder : ∀ j ∈ Finset.range b, ν (j+1) < μ j ∧ μ j < ν j)
    (hfirst : Real.log (10*B z) ≤ B z*(1-ν 1))
    (hgap : ∀ j ∈ Finset.Icc 2 b,
      2*Real.sqrt (B S/B z) < ν (j-1)-ν j)
    (hD : 1 ≤ D) (hDz : (D : ℝ) ≤ z^(1/100 : ℝ))
    (hDs : (largestPrimeFactor D : ℝ) ≤ comparisonCutoffs z ν b)
    (hr : 1 ≤ r) (hrz : (r : ℝ) ≤ z^(1/10 : ℝ)) :
    FordComparisonParameters b z S D r
…

Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.comparisonCutoffs, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.FordComparisonParameters