OAI/NumberTheory/EgyptianFractions/TerminalAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.TerminalAssembly.terminal_expansion_of_residue_supply line 14

   Source documentation

   The constructive terminal stage of the dense-family argument, with an explicit logarithmic length bound. The only remaining number-theoretic input is the asserted supply of divisor residues.

   theorem terminal_expansion_of_residue_supply
       (M U : ℕ) (D α S : ℝ) (hUM : U < M)
       (hD : 1 ≤ D) (hα : 0 < α) (hα1 : α < 1)
       (hS : 1 ≤ S) (hlogS : 1 ≤ Real.log S)
       (hU : (U : ℝ) ≤ Real.exp S)
       (hdiv : 2 ^ TerminalDepth.binaryExponent D S ∣ M)
       (hstep : ∀ u : ℕ, u ≤ U → S ^ D < (u : ℝ) →
         ∃ t z h : ℕ, 0 < t ∧ 0 < z ∧ t ∣ M ∧
           (h : ℝ) ≤ (u : ℝ) ^ α ∧ t + h = u * z) :
       ∀ u : ℕ, u ≤ U → ∃ l : List ℕ,
         (∀ n ∈ l, 2 ≤ n) ∧
         (l.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum = (u : ℚ) / M ∧
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.TerminalDepth.binaryExponent