OAI/NumberTheory/JointDickman/Arithmetic/PrimeAgreementZeroDistance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.zeta_prime_distance_zero line 12
2. theorem OAI.JointDickman.prime_agreement_zero_distance_bounded line 22

   Source documentation

   A function equal to one at all small primes has bounded distance to one, even after arbitrary fixed finite-prime changes.

   theorem prime_agreement_zero_distance_bounded {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1)
       (P : Finset ℕ) : ∃ C : ℝ, 0 ≤ C ∧
       ∀ᶠ X : ℝ in atTop, ∀ f : ArithmeticFunction ℂ,
         (∀ n, ‖f n‖ ≤ 1) →
         (∀ p : ℕ, p.Prime → p ∉ P → (p:ℝ) ≤ X^c → f p = 1) →
         primeDistanceSquared f X 0 ≤ C := by
   …