OAI/NumberTheory/JointDickman/Arithmetic/ConditionalPrimeParameters.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.remainingPrimeParameter line 13
2. theorem OAI.JointDickman.remainingPrimeParameter_mem_Icc line 16
3. theorem OAI.JointDickman.unselected_parameter_error line 25
4. theorem OAI.JointDickman.remaining_parameter_total_error line 38
5. theorem OAI.JointDickman.auxiliary_selected_reciprocal_sum_small line 67

   Source documentation

   Omitting a coefficient of fixed exponential size costs o(1) in total reciprocal prime mass, uniformly in the coefficient.

   theorem auxiliary_selected_reciprocal_sum_small {κ : ℝ} (_hκ : 0 < κ) :
       ∀ᶠ B : ℕ in atTop, ∀ S : Finset ℕ, S ⊆ auxiliaryPrimes B →
         (∏ p ∈ S, p : ℕ) ≤ Real.exp (κ * B) → (∑ p ∈ S, 1 / (p : ℝ)) ≤ 1 := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes

6. theorem OAI.JointDickman.remaining_prime_regularity_loss line 100

   Source documentation

   Uniform regularity of the remaining indicators after any selected coefficient in the fixed exponential range.

   theorem remaining_prime_regularity_loss
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {κ : ℝ} (hκ : 0 < κ) :
       ∃ K : ℝ, 0 < K ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
         ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
           ∀ᶠ B : ℕ in atTop, ∀ (S : Finset ℕ) (C : ℝ), 0 ≤ C → S ⊆ auxiliaryPrimes B →
             (∏ p ∈ S, p : ℕ) ≤ Real.exp (κ * B) →
             primeRegularityFailureProbability B L τ C (remainingPrimeParameter S) ≤
               K * (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primeRegularityFailureProbability, OAI.JointDickman.remainingPrimeParameter