GreedyPreparation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.PreparedGreedyPrefix line 10
Source documentation
A prefix ending either at zero or at a denominator in the target window.
```
def PreparedGreedyPrefix (a b : ℕ) (T : ℝ) (N : ℕ) : Prop :=
…
```

theorem OAI.Problem337.ordinary_greedy_step_bounded line 18

Source documentation

A greedy step decreases the numerator and squares the remaining value.

theorem ordinary_greedy_step_bounded (a b : ℕ) (ha : 0 < a) (hab : a < b) :
    ∃ z c : ℕ, 2 ≤ z ∧ z ≤ b ∧ c < a ∧
      (a : ℚ) / (b : ℚ) = (1 : ℚ) / (z : ℚ) +
        (c : ℚ) / ((b * z : ℕ) : ℚ) ∧
      (c : ℝ) / ((b * z : ℕ) : ℝ) ≤ ((a : ℝ) / (b : ℝ)) ^ 2 ∧
      (c : ℝ) / ((b * z : ℕ) : ℝ) < 1 / 2 := by
…

theorem OAI.Problem337.greedy_preparation_of_squaring line 67

Source documentation

The finite stopping argument needs only the squaring estimate for a greedy step.

theorem greedy_preparation_of_squaring
    (step : ∀ a b : ℕ, 0 < a → a < b →
      ∃ z c : ℕ, 2 ≤ z ∧ z ≤ b ∧ c < a ∧
        (a : ℚ) / (b : ℚ) = (1 : ℚ) / (z : ℚ) +
          (c : ℚ) / ((b * z : ℕ) : ℚ) ∧
        (c : ℝ) / ((b * z : ℕ) : ℝ) ≤ ((a : ℝ) / (b : ℝ)) ^ 2)
    (N : ℕ) :
    ∀ (a b : ℕ) (T u : ℝ), 0 < a → a < b → 1 < T →
      (b : ℝ) < T ^ 2 → 0 ≤ u → (a : ℝ) / (b : ℝ) ≤ u →
      T * u ^ (2 ^ N) ≤ 1 → PreparedGreedyPrefix a b T N := by
…

Mentions: OAI.Problem337.PreparedGreedyPrefix

theorem OAI.Problem337.PreparedGreedyPrefix.prepend line 135

Source documentation

Prefixes may be prefixed by a single valid unit-fraction step.

theorem PreparedGreedyPrefix.prepend {a b z c N : ℕ} {T : ℝ}
    (h : PreparedGreedyPrefix c (b * z) T N) (hz : 2 ≤ z) (hca : c ≤ a)
    (hsplit : (a : ℚ) / (b : ℚ) = (1 : ℚ) / (z : ℚ) +
      (c : ℚ) / ((b * z : ℕ) : ℚ)) : PreparedGreedyPrefix a b T (N + 1) := by
…

Mentions: OAI.Problem337.PreparedGreedyPrefix

theorem OAI.Problem337.greedy_preparation_power line 153
Source documentation
Quantitative denominator preparation: N+1 steps suffice as soon as T ≤ 2^(2^N). No reduction of the remaining fraction is performed.
```
theorem greedy_preparation_power (a b N : ℕ) (T : ℝ)
    (ha : 0 < a) (hab : a < b) (hbT : (b : ℝ) < T)
    (hTcap : T ≤ (2 : ℝ) ^ (2 ^ N)) : PreparedGreedyPrefix a b T (N + 1) := by
…
```
Mentions: OAI.Problem337.PreparedGreedyPrefix

theorem OAI.Problem337.greedy_preparation line 190

Source documentation

Equivalent stopping bound in the form convenient for logarithmic budgets.

theorem greedy_preparation (a b N : ℕ) (T : ℝ)
    (ha : 0 < a) (hab : a < b) (hbT : (b : ℝ) < T)
    (hcap : T * (1 / 2 : ℝ) ^ (2 ^ N) ≤ 1) :
    PreparedGreedyPrefix a b T (N + 1) := by
…

Mentions: OAI.Problem337.PreparedGreedyPrefix