OAI/NumberTheory/TotientAsymptotic/PrimeExtensionCoverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact coverage of large-prime totients by their residual totient values.

  1. lemma OAI.TotientAsymptotic.totient_prime_extension_cases line 11
  2. lemma OAI.TotientAsymptotic.totient_mem_primeExtensionValues line 22
  3. theorem OAI.TotientAsymptotic.large_prime_totient_count line 38

    Source documentation

    The residual set consists of values, so repeated preimages incur no extra factor.

    theorem large_prime_totient_count : ∀ᶠ x : ℝ in atTop,
    ∀ R Q : Finset ℕ,(∀ d ∈ R,0 < d) →
    (∀ v ∈ Q,∃ n p : ℕ,0 < n ∧ n.totient=v ∧ p.Prime ∧ p ∣ n ∧
      x^(1/4:ℝ) ≤ p ∧ (v:ℝ) ≤ x ∧ (n/p).totient ∈ R) →
    (Q.card:ℝ) ≤ (64*x/Real.log x)*(∑ d ∈ R,(d:ℝ)⁻¹) := by
…

    Mentions: OAI.TotientAsymptotic.R