OAI/NumberTheory/EgyptianFractions/MarkedConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.marked_distinct_tail_of_list line 13

   Source documentation

   The list interface produced by grouping can be cleaned up at fixed length.

   theorem marked_distinct_tail_of_list (l : List ℕ) {x : ℚ}
       (hx : 0 < x) (hxone : x < 1) (hl : ∀ d ∈ l, 0 < d)
       (hsum : (l.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum = x) :
       ∃ n : Fin l.length → ℕ, IsEgyptianExpansion x n := by
   …

   Mentions: OAI.Problem337.IsEgyptianExpansion

2. theorem OAI.Problem337.marked_expansion_from_rational_supply line 30

   Source documentation

   The qualitative assembly step of the quantitative marked construction. Only the prefix and the rational-divisor supply remain as inputs.

   theorem marked_expansion_from_rational_supply
       (m q K R : ℕ) (p : Finset ℕ)
       (hm : 2 ≤ m) (hq : 0 < q) (hK : 0 < K)
       (hR : R < 2 * m) (hRKq : R * K ≤ q)
       (hdensity : HasMarkedDivisorDensity m q)
       (hsupply : HasRationalDivisorSupply m K 16)
       (hp : ∀ d ∈ p, 1 ≤ d) (hmarker : m ∈ p)
       (hsum : (∑ d ∈ p, (1 : ℚ) / (d : ℚ)) + (R : ℚ) / (q : ℚ) = 1)
       (hsmall : ∀ d ∈ p, (R : ℚ) / (q : ℚ) < 1 / (d : ℚ)) :
       ∃ t k : ℕ, ∃ n : Fin k → ℕ,
         k = p.card + t ∧ IsOneExpansion n ∧ (∃ i, n i = m) ∧
         (t : ℝ) ≤ 16 * ((Real.log (K : ℝ) + Real.log (2 * (m : ℝ))) /
   …

   Mentions: OAI.Problem337.HasMarkedDivisorDensity, OAI.Problem337.HasRationalDivisorSupply, OAI.Problem337.IsOneExpansion