OAI/NumberTheory/EgyptianFractions/RestrictedRoughAsymptotic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.eventually_rough_divisor_card_subpower line 13

   Source documentation

   Uniform subpower bound for rough divisors of an arbitrary positive integer. The ambient integer may have small prime factors. The threshold and the finite family may both vary after the single eventual size threshold is chosen.

   theorem eventually_rough_divisor_card_subpower
       (A ε : ℝ) (hA : 0 < A) (hε : 0 < ε) :
       ∀ᶠ X : ℝ in atTop, ∀ n : ℕ, n ≠ 0 →
         Real.log (n : ℝ) ≤ A * Real.log X * Real.log (Real.log X) →
         ∀ R : ℝ, Real.log X ≤ R → ∀ s : Finset ℕ,
         (∀ d ∈ s, d ∣ n) → (∀ d ∈ s, (d : ℝ) ≤ X) →
         (∀ d ∈ s, ∀ p ∈ d.primeFactorsList, R ≤ (p : ℝ)) →
         (s.card : ℝ) ≤ X ^ ε := by
   …

2. theorem OAI.Problem337.eventually_card_rough_divisors_subpower line 32

   Source documentation

   The literal filtered-divisor-set version of the preceding uniform bound.

   theorem eventually_card_rough_divisors_subpower
       (A ε : ℝ) (hA : 0 < A) (hε : 0 < ε) :
       ∀ᶠ X : ℝ in atTop, ∀ n : ℕ, n ≠ 0 →
         Real.log (n : ℝ) ≤ A * Real.log X * Real.log (Real.log X) →
         ∀ R : ℝ, Real.log X ≤ R →
         ((n.divisors.filter (fun d : ℕ => (d : ℝ) ≤ X ∧
           ∀ p ∈ d.primeFactorsList, R ≤ (p : ℝ))).card : ℝ) ≤ X ^ ε := by
   …