OAI/NumberTheory/JointDickman/Amplification/WeightedCandidateMultiplicity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.candidateMultiplicityMoment line 10
2. theorem OAI.JointDickman.candidateMultiplicityMoment_le_firstMass line 20

   Source documentation

   This is the exact point at which the previously proved tilted count enters the square estimate. No regularity probability is divided out.

   theorem candidateMultiplicityMoment_le_firstMass {B L T H M : ℕ} {τ C Q : ℝ}
       (χ : BlockCandidateIndex M → ℝ) (hχ : ∀ e, 0 ≤ χ e)
       (i t : Fin M) (hit : i < t)
       (hcount : ∀ A ∈ (auxiliaryPrimes B).powerset, ∀ D ∈ (auxiliaryPrimes B).powerset,
         BlockCandidateAdmissible B L T H τ C ((i,t),(A,D)) →
         RegularPrimeSet B L τ C A → RegularPrimeSet B L τ C D →
         tiltedCandidatePairCount B L T H τ C i t A D ≤ Q) :
       candidateMultiplicityMoment B L T H τ C χ i t ≤
         Q*candidateFirstPairMass B L T H τ C χ i t := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.tiltedCandidatePairCount, OAI.JointDickman.candidateMultiplicityMoment, OAI.JointDickman.candidateFirstPairMass