OAI/NumberTheory/JointDickman/Amplification/RegularAmplificationMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.fairRegularAmplificationAt line 14
2. def OAI.JointDickman.fairRegularAmplificationMass line 22
3. theorem OAI.JointDickman.fairRegularAmplificationAt_complement line 27
4. theorem OAI.JointDickman.fairRegularAmplificationMass_complement line 48
5. theorem OAI.JointDickman.regular_amplification_first_moment_lower line 67

   Source documentation

   The first moment remains bounded below after choosing the tail cutoff sufficiently large, uniformly in every larger cutoff.

   theorem regular_amplification_first_moment_lower
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput) :
       ∃ d : ℝ, 0 < d ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
         ∃ C₀ : ℝ, 0 ≤ C₀ ∧ ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T : ℕ), C₀ ≤ C →
           0 < T → (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
           d ≤ (B : ℝ) * fairRegularAmplificationMass B L T τ C := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.fairRegularAmplificationMass