MarkedGreedy.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.marked_ceiling_spec line 8

Source documentation

The integer ceiling of q/R, presented without rational rounding.

theorem marked_ceiling_spec (R q : ℕ) (hR : 0 < R) (hRq : R < q) :
    ∃ a : ℕ, 2 ≤ a ∧ a ≤ q ∧ (a - 1) * R < q ∧ q ≤ a * R := by
…

theorem OAI.Problem337.marked_greedy_step_data line 30

Source documentation

One marked greedy step avoids the prescribed denominator, with an unreduced numerator.

theorem marked_greedy_step_data (m R q : ℕ)
    (hm : 4 ≤ m) (hR : 0 < R) (hRq : R < q) :
    ∃ n c : ℕ, 2 ≤ n ∧ n ≠ m ∧ n ≤ q + 1 ∧
      q ≤ n * R ∧ n * R = q + c ∧ c < q ∧ c < 2 * R ∧
      (n ≠ m + 1 → c < R) ∧
      (R : ℚ) / q = 1 / (n : ℚ) + (c : ℚ) / (n * q : ℕ) ∧
      (c : ℚ) / (n * q : ℕ) < 1 / (n : ℚ) := by
…

theorem OAI.Problem337.marked_greedy_square line 87

Source documentation

The ordinary steps square the size of the remainder.

theorem marked_greedy_square (R q n c : ℕ) (hR : 0 < R) (hq : 0 < q)
    (hn : 0 < n) (heq : n * R = q + c) (hc : c < R) :
    (c : ℚ) / (n * q : ℕ) < ((R : ℚ) / q) ^ 2 := by
…

inductive OAI.Problem337.MarkedGreedySteps line 107

Source documentation

A finite trace of unreduced marked greedy steps.

inductive MarkedGreedySteps (m : ℕ) : ℕ → ℕ → List ℕ → ℕ → ℕ → Prop
  | nil (R q : ℕ) : MarkedGreedySteps m R q [] R q
  | cons (R q n c : ℕ) (L : List ℕ) (Rf qf : ℕ)
      (hn : 2 ≤ n) (hnm : n ≠ m) (hnq : n ≤ q + 1)
      (heq : n * R = q + c) (hcq : c < q) (hcR : c < 2 * R)
      (hord : n ≠ m + 1 → c < R)
      (tail : MarkedGreedySteps m c (n * q) L Rf qf) :
      MarkedGreedySteps m R q (n :: L) Rf qf

/-- The process stops by the threshold, since each active step increases the denominator. -/

theorem OAI.Problem337.exists_marked_greedy_steps line 117

Source documentation

The process stops by the threshold, since each active step increases the denominator.

theorem exists_marked_greedy_steps (m T R q : ℕ) (hm : 4 ≤ m)
    (hq : 0 < q) (hRq : R < q) (hbound : q < T ^ 2) :
    ∃ L : List ℕ, ∃ Rf qf : ℕ, MarkedGreedySteps m R q L Rf qf ∧
      (Rf = 0 ∨ T ≤ qf) ∧ qf < T ^ 2 := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.MarkedGreedySteps.invariants line 137

Source documentation

Every chosen denominator is above the preceding threshold; the numerator remains small.

theorem MarkedGreedySteps.invariants {m R q Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m R q L Rf qf) (t : ℕ)
    (ht : 1 ≤ t) (hq : 0 < q) (hgap : t * R < q)
    (hsmall : R < 2 * m) (hphase : R < m ∨ m < t) :
    qf > 0 ∧ t * Rf < qf ∧ Rf < 2 * m ∧
      (∀ n ∈ L, t < n ∧ n ≠ m) ∧ L.Pairwise (· < ·) ∧
      (∀ n ∈ L, n * Rf < qf) := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.MarkedGreedySteps.denominator line 181
Source documentation
The unreduced denominator is exactly the initial one times the chosen denominators.
```
theorem MarkedGreedySteps.denominator {m R q Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m R q L Rf qf) : qf = q * L.prod := by
…
```
Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.MarkedGreedySteps.sum line 189

Source documentation

Telescoping the successive unreduced fraction identities.

theorem MarkedGreedySteps.sum {m R q Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m R q L Rf qf) (hq : 0 < q) :
    (R : ℚ) / q = (L.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum + (Rf : ℚ) / qf := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.exists_marked_greedy_prefix line 208

Source documentation

The marked greedy prefix, with all arithmetic conclusions except its length estimate.

theorem exists_marked_greedy_prefix (m T : ℕ) (hm : 4 ≤ m) (hT : 2 * m ^ 2 ≤ T) :
    ∃ L : List ℕ, ∃ R q : ℕ,
      MarkedGreedySteps m (m - 1) m L R q ∧
      L.Pairwise (· < ·) ∧ (∀ n ∈ L, 2 ≤ n ∧ n ≠ m) ∧
      q = m * L.prod ∧ 0 < q ∧ R < 2 * m ∧
      (1 : ℚ) = 1 / (m : ℚ) + (L.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum + (R : ℚ) / q ∧
      q < T ^ 2 ∧ (R = 0 ∨ T ≤ q) ∧
      m * R < q ∧ (∀ n ∈ L, n * R < q) := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.exists_marked_greedy_steps_bounded line 245

Source documentation

Stopping also records that the denominator before the last step is below the threshold.

theorem exists_marked_greedy_steps_bounded (m T R q : ℕ) (hm : 4 ≤ m)
    (hq : 0 < q) (hRq : R < q) (hbound : q < T ^ 2) :
    ∃ L : List ℕ, ∃ Rf qf : ℕ, MarkedGreedySteps m R q L Rf qf ∧
      (Rf = 0 ∨ T ≤ qf) ∧ qf < T ^ 2 ∧
      (L ≠ [] → q * L.dropLast.prod < T) := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.MarkedGreedySteps.first line 273

Source documentation

Every nonempty marked trace starts by removing one half.

theorem MarkedGreedySteps.first {m n Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m (m - 1) m (n :: L) Rf qf) (hm : 4 ≤ m) :
    n = 2 ∧ MarkedGreedySteps m (m - 2) (2 * m) L Rf qf := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.MarkedGreedySteps.split line 292

Source documentation

A trace can be cut at any chosen prefix.

theorem MarkedGreedySteps.split {m R q Rf qf : ℕ} {A B : List ℕ}
    (h : MarkedGreedySteps m R q (A ++ B) Rf qf) :
    ∃ Ri qi : ℕ, MarkedGreedySteps m R q A Ri qi ∧
      MarkedGreedySteps m Ri qi B Rf qf := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.MarkedGreedySteps.penultimate line 305

Source documentation

The state before the final step has a positive numerator.

theorem MarkedGreedySteps.penultimate {m R q Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m R q L Rf qf) (hL : L ≠ []) :
    ∃ Ri qi : ℕ, MarkedGreedySteps m R q L.dropLast Ri qi ∧
      0 < Ri ∧ 0 < qi ∧ qi = q * L.dropLast.prod := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.exists_marked_greedy_prefix_bounded line 319

Source documentation

The full arithmetic prefix contract also recording the final active state.

theorem exists_marked_greedy_prefix_bounded (m T : ℕ) (hm : 4 ≤ m) (hT : 2 * m ^ 2 ≤ T) :
    ∃ L : List ℕ, ∃ R q : ℕ,
      MarkedGreedySteps m (m - 1) m L R q ∧
      L.Pairwise (· < ·) ∧ (∀ n ∈ L, 2 ≤ n ∧ n ≠ m) ∧
      q = m * L.prod ∧ 0 < q ∧ R < 2 * m ∧
      (1 : ℚ) = 1 / (m : ℚ) + (L.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum + (R : ℚ) / q ∧
      q < T ^ 2 ∧ (R = 0 ∨ T ≤ q) ∧
      m * R < q ∧ (∀ n ∈ L, n * R < q) ∧
      (L ≠ [] → m * L.dropLast.prod < T) := by
…

Mentions: OAI.Problem337.MarkedGreedySteps