OAI/NumberTheory/EgyptianFractions/DenseExpansion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.reciprocal_sum_map_mul line 8

   Source documentation

   Scaling every unit denominator divides the represented rational by the same scale. Repetitions in the list are allowed.

   theorem reciprocal_sum_map_mul (ds : List ℕ) (g : ℕ) :
       ((ds.map (fun d : ℕ => g * d)).map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum =
         (ds.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum / (g : ℚ) := by
   …

2. theorem OAI.Problem337.dense_expansion_of_lists line 22

   Source documentation

   The dense-family additive argument for rational unit-fraction lists. The lists supplied for good numerators may contain repeated denominators; distinctification can be applied after adjoining a greedy prefix.

   theorem dense_expansion_of_lists
       (X : ℝ) (a C M L : ℕ) (G : Finset ℕ)
       (ha : 0 < a) (hC : 0 < C) (hM : 0 < M) (hX : 4 < X)
       (haM : ((a * M : ℕ) : ℝ) ≤ X)
       (hdense : ((Finset.Icc 1 ⌊X⌋₊ \ G).card : ℝ) ≤ X / 8)
       (hG : ∀ u ∈ G, ∃ ds : List ℕ,
         (∀ d ∈ ds, 2 ≤ d) ∧ ds.length ≤ L ∧
         (ds.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum =
           (u : ℚ) / ((M * C : ℕ) : ℚ)) :
       ∃ ds : List ℕ, (∀ d ∈ ds, 2 ≤ d) ∧ ds.length ≤ 2 * L ∧
         (ds.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum = (a : ℚ) / (C : ℚ) := by
   …