OAI/NumberTheory/EgyptianFractions/RationalDivisorSupplyBridge.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.HasRationalDivisorSum.to_list line 11

   Source documentation

   Convert the finite-indexed supply API to the list API consumed by grouping.

   theorem HasRationalDivisorSum.to_list {K B : ℕ} {x : ℚ}
       (h : HasRationalDivisorSum K x B) :
       ∃ terms : List (ℕ × ℕ), terms.length ≤ B ∧
         (∀ et ∈ terms, 0 < et.1 ∧ et.1 ∣ K ∧ 0 < et.2) ∧
         (terms.map (fun et => (et.1 : ℚ) / (et.2 : ℚ))).sum = x := by
   …

   Mentions: OAI.Problem337.HasRationalDivisorSum

2. theorem OAI.Problem337.rational_divisor_supply_bridge line 25

   Source documentation

   The algebraic odd-integer supply interface directly feeds the canonical unit-fraction grouping construction.

   theorem rational_divisor_supply_bridge {m K B : ℕ}
       (h : ∀ s : ℕ, 1 ≤ s → s ≤ m ^ 4 → HasRationalDivisorSum K (s : ℚ) B) :
       HasRationalDivisorSupply m K B := by
   …

   Mentions: OAI.Problem337.HasRationalDivisorSum, OAI.Problem337.HasRationalDivisorSupply

3. theorem OAI.Problem337.rational_divisor_supply_from_odd line 31
4. theorem OAI.Problem337.rational_divisor_supply_from_triples line 38
5. theorem OAI.Problem337.eventually_rational_divisor_supply_from_odd line 49

   Source documentation

   Eventual form convenient for the quantitative marked-length reduction.

   theorem eventually_rational_divisor_supply_from_odd (K : ℕ → ℕ) {N : ℕ}
       (hN : 1 ≤ N) (hfactorial : ∀ᶠ m : ℕ in Filter.atTop, N.factorial ∣ K m)
       (hodd : ∀ᶠ m : ℕ in Filter.atTop, ∀ u : ℕ, N ≤ u → u ≤ m ^ 4 → Odd u →
         HasRationalDivisorSum (K m) (u : ℚ) 15) :
       ∀ᶠ m : ℕ in Filter.atTop, HasRationalDivisorSupply m (K m) 16 := by
   …

   Mentions: OAI.Problem337.HasRationalDivisorSum, OAI.Problem337.HasRationalDivisorSupply