MarkedPrefixBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.quantitative_marked_prefix_of_short_list line 14

Source documentation

Translate the finite marked greedy list into the exact finite-set contract consumed by the quantitative endgame.

theorem quantitative_marked_prefix_of_short_list
    (m K R q : ℕ) (L : List ℕ) (hm : 4 ≤ m) (hK : m ≤ K)
    (htrace : MarkedGreedySteps m (m - 1) m L R q)
    (hpair : L.Pairwise (· < ·)) (hlist : ∀ d ∈ L, 2 ≤ d ∧ d ≠ m)
    (hq : 0 < q) (hR : R < 2 * m)
    (hsum : (1 : ℚ) = 1 / (m : ℚ) +
      (L.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum + (R : ℚ) / (q : ℚ))
    (hstop : R = 0 ∨ 2 * m * K ≤ q)
    (hmarker : m * R < q) (hfinal : ∀ d ∈ L, d * R < q)
    (hlen : (L.length : ℝ) ≤ 3 +
      (Real.log (Real.log (2 * (m : ℝ) * (K : ℝ))) - Real.log (Real.log 2)) /
        Real.log 2) :
…

Mentions: OAI.Problem337.MarkedGreedySteps

theorem OAI.Problem337.hasQuantitativeMarkedPrefix_of_le line 61
Source documentation
The complete marked greedy construction discharges the prefix prerequisite for every multiplier at least as large as the marker.
```
theorem hasQuantitativeMarkedPrefix_of_le (m K : ℕ) (hm : 4 ≤ m) (hK : m ≤ K) :
    HasQuantitativeMarkedPrefix m K := by
…
```
Mentions: OAI.Problem337.HasQuantitativeMarkedPrefix