OAI/NumberTheory/JointDickman/Arithmetic/TotientLogBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.totient_eq_prime_product_real line 12
2. theorem OAI.JointDickman.totient_log_bound line 19

   Source documentation

   Only moduli up to the fixed B^15 major-arc cutoff are needed.

   theorem totient_log_bound (hMP : PublishedInputs.PrimeProductMertensInput) :
       ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ q : ℕ,
         0 < q → q ≤ B^15 → (q : ℝ) ≤ K*Real.log B*q.totient := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeProductMertensInput

3. theorem OAI.JointDickman.majorArc_totient_power line 59

   Source documentation

   The reciprocal totient has the required B^(-0.4+epsilon) saving.

   theorem majorArc_totient_power (hMP : PublishedInputs.PrimeProductMertensInput)
       {ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ B : ℕ in atTop, ∀ q : ℕ, 0 < q → q ≤ B^15 →
         (B : ℝ)^(2/5 : ℝ) ≤ q →
         1/(q.totient : ℝ) ≤ (B : ℝ)^(-2/5+ε) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeProductMertensInput