OAI/NumberTheory/JointDickman/Probability/AmplificationFirstMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.amplificationNarrowPairs line 13
2. theorem OAI.JointDickman.amplificationNarrowPairs_subset line 16
3. theorem OAI.JointDickman.amplificationNarrowPairs_sum line 23
4. theorem OAI.JointDickman.amplification_lower_c_mass line 40
5. theorem OAI.JointDickman.amplification_first_moment_lower line 60

   Source documentation

   The size-and-ratio event has a positive B-normalized first moment, uniformly in every admissible amplification scale T.

   theorem amplification_first_moment_lower
       (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput) :
       ∃ d : ℝ, 0 < d ∧ ∀ᶠ B : ℕ in atTop, ∀ T : ℕ,
         0 < T → (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
         d ≤ (B : ℝ) * (∑ ac ∈ amplificationCoefficientPairs B T,
           primeProductMass (auxiliaryPrimes B) (1 / 2) ac.1 *
             primeProductMass (auxiliaryPrimes B) (1 / 2) ac.2) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.amplificationCoefficientPairs, OAI.JointDickman.primeProductMass, OAI.JointDickman.auxiliaryPrimes