PPTComparisonDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed-seed comparison budget in the proof of Ford (5.23). The positive error has size at most a constant times t^(2/3) (log t)^2, where t = log log z; the negative simplex gap has size t/(log t)^3. The latter absorbs every fixed inverse power of t.

theorem OAI.TotientAsymptotic.ppt_comparison_exp_decay line 18
theorem OAI.TotientAsymptotic.ppt_comparison_exp_decay_at_scale line 65
Source documentation
Direct substitution of the totient scale, with the conventional (log log z)^(-K) remainder in the exceptional-candidate count.
```
theorem ppt_comparison_exp_decay_at_scale (A K : ℝ) {δ : ℝ} (hδ : 0 < δ) :
    ∀ᶠ z : ℝ in atTop,
      Real.exp (A*(B z)^(2/3 : ℝ)*(Real.log (B z))^2 -
        δ*B z/(Real.log (B z))^3) ≤ (B z)^(-K) := by
…
```
Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.B