OAI/NumberTheory/JointDickman/Counting/CoefficientDigitEvents.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.primeDigitMass line 12
2. theorem OAI.JointDickman.primeDigitMass_nonneg line 16
3. theorem OAI.JointDickman.prime_digit_test_bound line 20
4. def OAI.JointDickman.coefficientDigitTest line 44
5. theorem OAI.JointDickman.coefficient_digit_single_bound line 52
6. def OAI.JointDickman.CoefficientDigitEvent line 76
7. theorem OAI.JointDickman.coefficient_digit_event_bound line 82

   Source documentation

   Uniform in every exposed first-digit family and its resulting candidate list. No independence between that list and its endpoint types is assumed.

   theorem coefficient_digit_event_bound {B L T H M : ℕ} {τ C : ℝ}
       [∀ p : auxiliaryPrimes B, NeZero p.val]
       (hB : 2 ≤ B) (hT : (T : ℝ) ≤ Real.exp B) (hM : (M : ℝ) ≤ Real.exp B)
       (hP : 0 < auxiliaryCutoff B) (I : Finset (BlockCandidateIndex M))
       (he : ∀ e ∈ I, BlockCandidateAdmissible B L T H τ C e)
       (r : ∀ p : auxiliaryPrimes B, ZMod p.val) :
       finiteProbability (primeDigitMass B) (CoefficientDigitEvent B I r) ≤
         12*(I.card : ℝ)*(B : ℝ)/(Real.log 2*auxiliaryCutoff B) := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.finiteProbability, OAI.JointDickman.primeDigitMass, OAI.JointDickman.CoefficientDigitEvent