OAI/NumberTheory/EgyptianFractions/SmallPrimeRankin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMoment.small_prime_smooth_tail_bound line 11

   Source documentation

   The small-prime smooth-prefix tail estimate from the divisor-moment proof. The constant is absolute and the finite set of prefixes is arbitrary.

   theorem small_prime_smooth_tail_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (S v : ℝ), 1 ≤ S → ∀ (N : ℕ),
         (N : ℝ) ≤ S ^ (4 : ℕ) + 1 → ∀ s : Finset ℕ,
         (∀ n ∈ s, n ∈ N.smoothNumbers) →
         (∀ n ∈ s, Real.exp (v / 5) ≤ (n : ℝ)) →
         (∑ n ∈ s, (1 : ℝ) / n) ≤ Real.exp (-v / 50 + C * S ^ (2 / 5 : ℝ)) := by
   …

   Mentions: OAI.Problem337.v

2. theorem OAI.Problem337.DivisorMoment.small_prime_factor_tail_bound line 61

   Source documentation

   A cutoff phrased directly in terms of prime factors, without a smooth-number index.

   theorem small_prime_factor_tail_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (S v : ℝ), 1 ≤ S → ∀ s : Finset ℕ,
         (∀ n ∈ s, ∀ p ∈ n.primeFactorsList, (p : ℝ) < S ^ (4 : ℕ)) →
         (∀ n ∈ s, Real.exp (v / 5) ≤ (n : ℝ)) →
         (∑ n ∈ s, (1 : ℝ) / n) ≤ Real.exp (-v / 50 + C * S ^ (2 / 5 : ℝ)) := by
   …

   Mentions: OAI.Problem337.v