OAI/NumberTheory/EgyptianFractions/PrimeFactorPrefix.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.list_product_crossing line 10

   Source documentation

   A finite product crosses any threshold lying between its initial multiplier and its final value. No monotonicity assumptions on the factors are needed.

   theorem list_product_crossing (l : List ℕ) (d : ℕ) (y : ℝ)
       (hdy : (d : ℝ) ≤ y) (hy : y < (d * l.prod : ℕ)) :
       ∃ a : List ℕ, ∃ p : ℕ, ∃ b : List ℕ,
         l = a ++ p :: b ∧ (d * a.prod : ℕ) ≤ y ∧ y < (d * a.prod * p : ℕ) := by
   …

2. theorem OAI.Problem337.prime_factor_prefix line 30

   Source documentation

   The longest sorted prime-factor prefix below a real threshold. The two prime-factor separation statements allow the smooth and rough parts of the divisor-moment argument to be estimated independently.

   theorem prime_factor_prefix (n : ℕ) (y : ℝ) (hy : 1 ≤ y) (hyn : y < n) :
       ∃ d p : ℕ, 0 < d ∧ p.Prime ∧ d ∣ n ∧
         (d : ℝ) ≤ y ∧ y < (d * p : ℕ) ∧ p ∣ n / d ∧
         (∀ q : ℕ, q.Prime → q ∣ d → q ≤ p) ∧
         (∀ q : ℕ, q.Prime → q ∣ n / d → p ≤ q) := by
   …