OAI/NumberTheory/JointDickman/Arithmetic/SieveDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.closed_prime_interval_sum_le line 13

   Source documentation

   The possible prime at the lower endpoint costs at most 1 / log y.

   theorem closed_prime_interval_sum_le
       (hM : PublishedInputs.PrimeReciprocalMertensInput) :
       ∃ K : ℝ, 0 ≤ K ∧ ∀ (P : Finset ℕ) (y v : ℝ),
         (∀ p ∈ P, p.Prime) → 2 ≤ y → y ≤ v →
         (∑ p ∈ P.filter (fun p : ℕ => y ≤ (p : ℝ) ∧ (p : ℝ) ≤ v),
           1 / (p : ℝ)) ≤ Real.log (Real.log v / Real.log y) + K / Real.log y := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput

2. theorem OAI.JointDickman.sieveDimension_of_reciprocal_bound line 62

   Source documentation

   A fixed number of forbidden classes per prime has bounded dimension. The dimension 2*k is deliberately sufficient, rather than optimal.

   theorem sieveDimension_of_reciprocal_bound
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {k : ℝ} (hk : 0 < k) :
       ∃ A : ℝ, 0 ≤ A ∧ ∀ (P : Finset ℕ) (g : ℕ → ℝ) (z : ℝ),
         (∀ p ∈ P, p.Prime) →
         (∀ p ∈ P, 0 ≤ g p ∧ g p ≤ 1 / 2 ∧ g p ≤ k / (p : ℝ)) →
         SieveDimension P g (2 * k) A z := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.SieveDimension