OAI/NumberTheory/TotientAsymptotic/PrefixWeight.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.prefixQ line 11
2. lemma OAI.TotientAsymptotic.prefixQ_bounds line 13
3. lemma OAI.TotientAsymptotic.prefix_candidate_ratio line 29
4. theorem OAI.TotientAsymptotic.prefix_weight_error line 52

   Source documentation

   The true interval weight is uniformly close to the arithmetic tail weight.

   theorem prefix_weight_error : ∀ᶠ H : ℕ in atTop,
       ∀ x : ℝ, 0 ≤ theta x → H ≤ m x → ∀ k : ℕ,
       ∀ ζ : PrefixDatum (R x H), IsPrefixDatum x H ζ →
         |fk k ((prefixCandidateFactor ζ : ℝ)/prefixDenominator ζ)-fk k ((ell ζ.d : ℝ)/ζ.d)| ≤
           (2*(k : ℝ)+1)*prefixReciprocalError H := by
   …

   Mentions: OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.PrefixDatum, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsPrefixDatum, OAI.TotientAsymptotic.fk, OAI.TotientAsymptotic.prefixCandidateFactor, OAI.TotientAsymptotic.prefixDenominator, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.prefixReciprocalError

5. lemma OAI.TotientAsymptotic.prefix_ell_bound line 69
6. lemma OAI.TotientAsymptotic.prefix_candidate_ratio_bounds line 79