OAI/NumberTheory/JointDickman/Arithmetic/CandidateExceptionalPrimes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.candidateRootNumerator line 11
2. def OAI.JointDickman.candidateSiteValue line 14
3. def OAI.JointDickman.candidateRootDifference line 17
4. theorem OAI.JointDickman.candidate_quotient_exp_bounds line 20
5. theorem OAI.JointDickman.affine_candidate_size line 32

   Source documentation

   An affine coefficient of a candidate has logarithmic size O(B), with an explicit exponent sufficient for every exceptional-prime estimate.

   theorem affine_candidate_size {B T M b c : ℕ} {t : ℤ}
       (hB : 2 ≤ B) (hT : (T : ℝ) ≤ Real.exp B) (hM : (M : ℝ) ≤ Real.exp B)
       (hc : (c : ℝ) ≤ Real.exp (2*B)) (hb : b ≤ 2*T*c) (ht : t.natAbs ≤ M) :
       (((b : ℤ)+t*c).natAbs : ℝ) ≤ Real.exp (5*B) := by
   …

6. theorem OAI.JointDickman.candidateRootNumerator_size line 53
7. theorem OAI.JointDickman.candidateSiteValue_size line 66
8. theorem OAI.JointDickman.candidateSiteValue_ne_zero line 81
9. theorem OAI.JointDickman.candidateSiteValue_prime_mass line 94

   Source documentation

   Forced hits at another endpoint involve only primes dividing this nonzero affine coefficient.

   theorem candidateSiteValue_prime_mass {B L T H M : ℕ} {τ C : ℝ}
       (hB : 2 ≤ B) (hT : (T : ℝ) ≤ Real.exp B) (hM : (M : ℝ) ≤ Real.exp B)
       {e : BlockCandidateIndex M} (he : BlockCandidateAdmissible B L T H τ C e) (s : Fin M)
       (P : ℝ) (hP : 0 < P) (Q : Finset ℕ)
       (hQ : Q ⊆ (candidateSiteValue e s).natAbs.primeFactors)
       (hcut : ∀ p ∈ Q, P ≤ (p : ℝ)) :
       (∑ p ∈ Q, 1/(p : ℝ)) ≤ (5*(B : ℝ))/(Real.log 2*P) :=
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.candidateSiteValue

10. theorem OAI.JointDickman.candidateRoot_fraction line 105
11. theorem OAI.JointDickman.candidateRootDifference_ne_zero line 110
12. theorem OAI.JointDickman.candidateRootDifference_size line 126
13. theorem OAI.JointDickman.candidateRootDifference_prime_mass line 163

    Source documentation

    Distinct rational roots can collide modulo primes only at a set whose reciprocal mass has this uniform bound.

    theorem candidateRootDifference_prime_mass {B L T H M : ℕ} {τ C : ℝ}
        (hB : 2 ≤ B) (hT : (T : ℝ) ≤ Real.exp B) (hM : (M : ℝ) ≤ Real.exp B)
        {e f : BlockCandidateIndex M}
        (he : BlockCandidateAdmissible B L T H τ C e)
        (hf : BlockCandidateAdmissible B L T H τ C f)
        (hroots : blockCandidateRoot e ≠ blockCandidateRoot f)
        (P : ℝ) (hP : 0 < P) (Q : Finset ℕ)
        (hQ : Q ⊆ (candidateRootDifference e f).natAbs.primeFactors)
        (hcut : ∀ p ∈ Q, P ≤ (p : ℝ)) :
        (∑ p ∈ Q, 1/(p : ℝ)) ≤ (8*(B : ℝ))/(Real.log 2*P) :=
    …

    Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.blockCandidateRoot, OAI.JointDickman.candidateRootDifference