OAI/NumberTheory/JointDickman/Amplification/CandidateMultiplicityAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.tiltedCandidatePairCount line 13
2. theorem OAI.JointDickman.tiltedCandidatePairCount_le_classes line 20

   Source documentation

   The finite grid cover can be averaged without dropping either regularity indicator. The opposite orientation is averaged in the opposite order.

   theorem tiltedCandidatePairCount_le_classes
       {B L T H M : ℕ} {τ C K : ℝ} (hB : 5 ≤ B) (hL : 3 ≤ L)
       (hT : (T : ℝ) ≤ Real.exp B) (i t : Fin M) (A D : Finset ℕ)
       (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B) (hK : 0 ≤ K)
       (hsmall : ∀ U V : Finset ℕ, RegularPrimeSet B L τ C U → RegularPrimeSet B L τ C V →
         ((smallCandidateAlternatives B L T H τ C i t A D U V).card : ℝ) ≤ K) :
       tiltedCandidatePairCount B L T H τ C i t A D ≤ K +
         ∑ k ∈ Icc 4 L,
           (regularTiltAverage B L τ C D (fun V =>
             tiltedAllLargeLowPairCount B L k (t.val-i.val) τ C (1/(L : ℝ)) A D V) +
           regularTiltAverage B L τ C A (fun U =>
             tiltedAllLargeHighPairCount B L k (t.val-i.val) τ C (1/(L : ℝ)) D A U)) := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.smallCandidateAlternatives, OAI.JointDickman.tiltedCandidatePairCount, OAI.JointDickman.regularTiltAverage, OAI.JointDickman.tiltedAllLargeLowPairCount, OAI.JointDickman.tiltedAllLargeHighPairCount