OAI/NumberTheory/TotientAsymptotic/UntruncatedCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.untruncated_totient_lower line 12
2. theorem OAI.TotientAsymptotic.untruncated_witness_count line 36

   Source documentation

   Count any finite family before truncating its smooth cofactor. The largest-prime count is uniform in both the cofactor and the prime vector.

   theorem untruncated_witness_count : ∀ᶠ x : ℝ in atTop, ∀ H : ℕ,
       ∀ S : Finset (RemainderDatum (L x H) × ℕ),
       (∀ q ∈ S, IsUntruncatedRemainder x H q.1 ∧ q.2.Prime ∧
         x^(9/10 : ℝ) ≤ q.2 ∧ ((wholePreimage q.2 q.1).totient : ℝ) ≤ x) →
       (S.card : ℝ) ≤ (10*x/Real.log x)*
         ∑ η ∈ S.image Prod.fst, (η.cofactor.totient : ℝ)⁻¹*reciprocalShiftWeight η.primes := by
   …

   Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsUntruncatedRemainder, OAI.TotientAsymptotic.wholePreimage, OAI.TotientAsymptotic.reciprocalShiftWeight