MarkedGreedyLength.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.MarkedGreedySteps.remainder_le_pow_count line 9

Source documentation

Each ordinary step squares the remainder; we count only these steps.

theorem MarkedGreedySteps.remainder_le_pow_count {m R q Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m R q L Rf qf) (hq : 0 < q)
    (a : ℚ) (ha : 0 ≤ a) (hstart : (R : ℚ) / q ≤ a) :
    (Rf : ℚ) / qf ≤ a ^ (2 ^ (L.filter (fun n => n ≠ m + 1)).length) := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.length_le_filter_ne_add_one line 46
Source documentation
In a duplicate-free list, discarding one specified value loses at most one term.
```
theorem length_le_filter_ne_add_one (L : List ℕ) (c : ℕ) (hL : L.Nodup) :
    L.length ≤ (L.filter (fun n => n ≠ c)).length + 1 := by
…
```

theorem OAI.Problem337.MarkedGreedySteps.remainder_le_half_pow_length line 67

Source documentation

A duplicate-free marked trace has at most one non-squaring step.

theorem MarkedGreedySteps.remainder_le_half_pow_length {m R q Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m R q L Rf qf) (hq : 0 < q)
    (hL : L.Nodup) (hstart : (R : ℚ) / q ≤ (1 / 2 : ℚ)) :
    (Rf : ℚ) / qf ≤ (1 / 2 : ℚ) ^ (2 ^ (L.length - 1)) := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.MarkedGreedySteps.length_lt_loglog line 80

Source documentation

A marked greedy trace with a last active denominator below T has the sharp double-logarithmic prefix length bound.

theorem MarkedGreedySteps.length_lt_loglog {m R q T : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m (m - 1) m L R q) (hm : 4 ≤ m)
    (hL : L.Nodup) (hT : 2 ≤ T)
    (hactive : L ≠ [] → m * L.dropLast.prod < T) :
    (L.length : ℝ) < 3 + Real.log (Real.log (T : ℝ) / Real.log 2) / Real.log 2 := by
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.exists_marked_greedy_prefix_short line 130

Source documentation

The marked greedy prefix, now including its quantitative term budget.

theorem exists_marked_greedy_prefix_short (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.length : ℝ) < 3 + Real.log (Real.log (T : ℝ) / Real.log 2) / Real.log 2 := by
…

Mentions: OAI.Problem337.MarkedGreedySteps