MarkedGreedyDensity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.MarkedGreedySteps.denominator_chain line 11
Source documentation
The concrete marked greedy trace obeys the unrestricted denominator chain.
```
theorem MarkedGreedySteps.denominator_chain {m R q Rf qf : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m R q L Rf qf) :
    GreedyDenominator m q → GreedyDenominator m qf := by
…
```
Mentions: OAI.Problem337.MarkedGreedySteps, OAI.Problem337.GreedyDenominator
theorem OAI.Problem337.MarkedGreedySteps.divisorDense line 21
Source documentation
Every denominator arising from the marked prefix has divisors at every scale.
```
theorem MarkedGreedySteps.divisorDense {m R q : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m (m - 1) m L R q) (hm : 2 ≤ m) :
    DivisorDense m q :=
…
```
Mentions: OAI.Problem337.MarkedGreedySteps, OAI.Problem337.DivisorDense

theorem OAI.Problem337.MarkedGreedySteps.grouped_tail line 28

Source documentation

An abstract rational-divisor supply turns the marked prefix remainder into an unmarked positive unit-fraction tail with the required grouping budget.

theorem MarkedGreedySteps.grouped_tail {m R q K B : ℕ} {L : List ℕ}
    (h : MarkedGreedySteps m (m - 1) m L R q) (hm : 2 ≤ m)
    (hK : 0 < K) (hRK : R * K ≤ q) (hsupply : HasRationalDivisorSupply m K B) :
    ∃ k : ℕ, ∃ n : Fin k → ℕ,
      (∀ i, 0 < n i) ∧ (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) = (R : ℚ) / q ∧
      (k : ℝ) ≤ (B : ℝ) *
        (Real.log ((R * K : ℕ) : ℝ) / (2 * Real.log (m : ℝ)) + 1) := by
…

Mentions: OAI.Problem337.MarkedGreedySteps, OAI.Problem337.HasRationalDivisorSupply