TerminalRecursion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.TerminalDescent.UnitList line 9
Source documentation
Unit-fraction lists in the intermediate construction may repeat denominators.
```
def UnitList (x : ℚ) (s : List ℕ) : Prop :=
…
```
lemma OAI.Problem337.TerminalDescent.reciprocal_sum_scale line 12
lemma OAI.Problem337.TerminalDescent.UnitList.scale line 21
lemma OAI.Problem337.TerminalDescent.unitList_zero line 30

lemma OAI.Problem337.TerminalDescent.log_potential_step line 33

Source documentation

A power-saving step contracts the logarithmic potential.

lemma log_potential_step {u h q : ℝ} (hu : 0 < u) (hh : 0 < h)
    (hq : 0 ≤ q) (hstep : h ≤ u ^ q) (N : ℕ) :
    q ^ N * Real.log h ≤ q ^ (N + 1) * Real.log u := by
…

theorem OAI.Problem337.TerminalDescent.short_unit_list_of_descent line 45

Source documentation

Terminal descent: each residue step adds one unit fraction; the logarithmic contraction gives an explicit upper bound on the depth.

theorem short_unit_list_of_descent
    (M T U B : ℕ) (hT : 0 < T) (q : ℝ) (hq : 0 ≤ q)
    (hbase : ∀ u : ℕ, u ≤ U → u ≤ T →
      ∃ s : List ℕ, UnitList ((u : ℚ) / (M : ℚ)) s ∧ s.length ≤ B)
    (hstep : ∀ u : ℕ, u ≤ U → T < u →
      ∃ a z h : ℕ, 0 < a ∧ 0 < z ∧ h ≤ U ∧
        (h : ℝ) ≤ (u : ℝ) ^ q ∧
        (u : ℚ) / (M : ℚ) = (1 : ℚ) / (a : ℚ) +
          ((h : ℚ) / (M : ℚ)) / (z : ℚ)) :
    ∀ N u : ℕ, u ≤ U →
      q ^ N * Real.log (u : ℝ) ≤ Real.log (T : ℝ) →
      ∃ s : List ℕ, UnitList ((u : ℚ) / (M : ℚ)) s ∧ s.length ≤ B + N := by
…

Mentions: OAI.Problem337.TerminalDescent.UnitList