OAI/NumberTheory/JointDickman/Amplification/TrimmedCandidateRoots.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.arithmeticCandidateHit line 10
2. def OAI.JointDickman.trimmedCandidatePrimeHit line 14
3. theorem OAI.JointDickman.arithmetic_candidate_hit_eq_trimmed line 22

   Source documentation

   The finite exclusions used here are explicit arithmetic events. Outside them, the original quotient prime sets equal the trimmed residue model.

   theorem arithmetic_candidate_hit_eq_trimmed {B L T H M p u : ℕ} {τ C : ℝ}
       [Fact p.Prime] (I : Finset (BlockCandidateIndex M))
       (m : BlockCandidateIndex M → ℕ) (hp : p ∈ auxiliaryPrimes B)
       (he : ∀ e ∈ I, BlockCandidateAdmissible B L T H τ C e)
       (heq : ∀ e ∈ I, candidateHigh e*candidateLow e*m e+candidateLow e =
         candidateQuotient e*(u+(e.1.1.val+1)))
       (hforce : ∀ e ∈ I, ¬ CandidateForcedWitness B e
         (fun i => coefficientPrimeSet B (u+(i.val+1))))
       (hcoeff : ∀ e ∈ I, p ∈ candidateCoefficientPrimes B e → ¬ p ∣ m e) :
       arithmeticCandidateHit I p m = trimmedCandidatePrimeHit B I p
         (blockPrimeHit M p (u : ZMod p)) (u : ZMod p) := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateQuotient, OAI.JointDickman.CandidateForcedWitness, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.candidateCoefficientPrimes, OAI.JointDickman.arithmeticCandidateHit, OAI.JointDickman.trimmedCandidatePrimeHit, OAI.JointDickman.blockPrimeHit