OAI/NumberTheory/EgyptianFractions/SmallPrimeClass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMoment.divisor_class_sum_le_exp line 13

   Source documentation

   A constant pointwise bound and a reciprocal sum over admissible prefix divisors control the corresponding class in a translated short interval.

   theorem divisor_class_sum_le_exp
       (N : ℕ) (Y R T : ℝ) (A D : Finset ℕ) (w : ℕ → ℝ)
       (hY : 0 ≤ Y) (hA : A ⊆ Finset.Ioc N (N + ⌊Y⌋₊))
       (hassign : ∀ n ∈ A, ∃ d ∈ D, d ∣ n)
       (hweight : ∀ n ∈ A, w n ≤ Real.exp R)
       (hD : ∀ d ∈ D, 0 < d ∧ (d : ℝ) ≤ Y)
       (htail : (∑ d ∈ D, 1 / (d : ℝ)) ≤ Real.exp T) :
       (∑ n ∈ A, w n) ≤ 2 * Y * Real.exp (T + R) := by
   …

   Mentions: OAI.Problem337.D

2. theorem OAI.Problem337.DivisorMoment.shifted_divisor_class_sum_le_exp line 43

   Source documentation

   The same bound with the short interval indexed by its displacement h. No choice or uniqueness of the prefix divisor is required.

   theorem shifted_divisor_class_sum_le_exp
       (N : ℕ) (Y R T : ℝ) (A D : Finset ℕ) (w : ℕ → ℝ)
       (hY : 0 ≤ Y) (hA : A ⊆ Finset.Icc 1 ⌊Y⌋₊)
       (hassign : ∀ h ∈ A, ∃ d ∈ D, d ∣ N + h)
       (hweight : ∀ h ∈ A, w (N + h) ≤ Real.exp R)
       (hD : ∀ d ∈ D, 0 < d ∧ (d : ℝ) ≤ Y)
       (htail : (∑ d ∈ D, 1 / (d : ℝ)) ≤ Real.exp T) :
       (∑ h ∈ A, w (N + h)) ≤ 2 * Y * Real.exp (T + R) := by
   …

   Mentions: OAI.Problem337.D

3. theorem OAI.Problem337.DivisorMoment.small_prime_class_sum_bound line 77

   Source documentation

   The actual small-prime class estimate. The admissible prefixes are positive divisors at most Y, smooth below P, and larger than exp(v/5). The exponential saving is uniform in the interval origin, its real length, the finite class, and the pointwise bound R.

   theorem small_prime_class_sum_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (S v R Y : ℝ), 1 ≤ S → 0 ≤ Y →
         ∀ (N P : ℕ), (P : ℝ) ≤ S ^ (4 : ℕ) + 1 →
         ∀ (A : Finset ℕ) (w : ℕ → ℝ),
         A ⊆ Finset.Ioc N (N + ⌊Y⌋₊) →
         (∀ n ∈ A, w n ≤ Real.exp R) →
         (∀ n ∈ A, ∃ d : ℕ, 0 < d ∧ (d : ℝ) ≤ Y ∧ d ∣ n ∧
           d ∈ P.smoothNumbers ∧ Real.exp (v / 5) ≤ (d : ℝ)) →
         (∑ n ∈ A, w n) ≤
           2 * Y * Real.exp (-v / 50 + C * S ^ (2 / 5 : ℝ) + R) := by
   …

   Mentions: OAI.Problem337.v

4. theorem OAI.Problem337.DivisorMoment.small_prime_class_shifted_sum_bound line 111

   Source documentation

   Displacement-indexed small-prime class estimate used in the moment sum over 1 ≤ h ≤ Y.

   theorem small_prime_class_shifted_sum_bound :
       ∃ C : ℝ, 0 < C ∧ ∀ (S v R Y : ℝ), 1 ≤ S → 0 ≤ Y →
         ∀ (N P : ℕ), (P : ℝ) ≤ S ^ (4 : ℕ) + 1 →
         ∀ (A : Finset ℕ) (w : ℕ → ℝ), A ⊆ Finset.Icc 1 ⌊Y⌋₊ →
         (∀ h ∈ A, w (N + h) ≤ Real.exp R) →
         (∀ h ∈ A, ∃ d : ℕ, 0 < d ∧ (d : ℝ) ≤ Y ∧ d ∣ N + h ∧
           d ∈ P.smoothNumbers ∧ Real.exp (v / 5) ≤ (d : ℝ)) →
         (∑ h ∈ A, w (N + h)) ≤
           2 * Y * Real.exp (-v / 50 + C * S ^ (2 / 5 : ℝ) + R) := by
   …

   Mentions: OAI.Problem337.v