OAI/NumberTheory/EgyptianFractions/SmallPrimeSelectedClass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMoment.small_prime_selected_prefix_sum_bound line 15

   Source documentation

   The selected-prime-prefix form of the small class estimate. The prefix crosses sqrt(Y) at a prime p whose logarithm is below 4 log(S); its size and smoothness are conclusions, not additional hypotheses on the class.

   theorem small_prime_selected_prefix_sum_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ᶠ S : ℝ in atTop,
         ∀ (v R Y : ℝ), S / (2 * Real.log S) ≤ v →
         1 ≤ Y → v / 2 ≤ Real.log Y → ∀ (N : ℕ),
         ∀ (A : Finset ℕ) (w : ℕ → ℝ), A ⊆ Finset.Icc 1 ⌊Y⌋₊ →
         (∀ h ∈ A, w (N + h) ≤ Real.exp R) →
         (∀ h ∈ A, ∃ d p : ℕ, 0 < d ∧ 0 < p ∧ d ∣ N + h ∧
           (d : ℝ) ≤ Real.sqrt Y ∧ Real.sqrt Y < (d : ℝ) * p ∧
           (∀ ℓ : ℕ, ℓ.Prime → ℓ ∣ d → ℓ ≤ p) ∧
           Real.log (p : ℝ) < v ^ (15 / 16 : ℝ) ∧
           Real.log (p : ℝ) < 4 * Real.log S) →
         (∑ h ∈ A, w (N + h)) ≤
   …

   Mentions: OAI.Problem337.v