OAI/NumberTheory/TotientAsymptotic/LargeNonNormalValues.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Distinct exceptional totient values, grouped by the residual value.

  1. def OAI.TotientAsymptotic.abnormalExtensionPrimes line 12
  2. def OAI.TotientAsymptotic.abnormalExtensionValues line 15
  3. lemma OAI.TotientAsymptotic.abnormal_extension_values_card line 18
  4. lemma OAI.TotientAsymptotic.totient_mem_abnormalExtensionValues line 26
  5. theorem OAI.TotientAsymptotic.large_non_normal_value_count line 44

    Source documentation

    Large non-normal prime divisors cost only the reciprocal mass of the residual totient values, even when a value has many preimages.

    theorem large_non_normal_value_count : ∃ C : ℝ,0 < C ∧
    ∀ S x : ℝ,2 < S → 4 ≤ x → ∀ R Q : Finset ℕ,(∀ d ∈ R,0 < d) →
    (∀ v ∈ Q,∃ n p : ℕ,0 < n ∧ n.totient=v ∧ p.Prime ∧ p ∣ n ∧ 4 ≤ p ∧
      x^(1/4:ℝ) ≤ p ∧ (v:ℝ) ≤ x ∧ ¬IsNormalPrime S p ∧ (n/p).totient ∈ R) →
    (Q.card:ℝ) ≤ (C*x/Real.log x*(B (2*x))^5*(Real.log S)^(-1/6:ℝ))*
      ∑ d ∈ R,(d:ℝ)⁻¹ := by
…

    Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B