MarkedBudget.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.marked_loglog_tendsto line 10

theorem OAI.Problem337.marked_group_budget line 15

Source documentation

Convert the supply's size budget into the short grouping budget.

theorem marked_group_budget (K G : ℕ → ℝ)
    (hK : ∀ δ : ℝ, 0 < δ → ∀ᶠ m : ℕ in atTop,
      Real.log (K m) ≤ (32 / Real.log 2 + δ) * Real.log (m : ℝ) *
        Real.log (Real.log (m : ℝ)))
    (hG : ∀ᶠ m : ℕ in atTop,
      G m ≤ (Real.log (K m) + Real.log (2 * (m : ℝ))) /
        (2 * Real.log (m : ℝ)) + 2) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
      G m ≤ (16 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)) := by
…

theorem OAI.Problem337.eventually_log_add_const_le_mul line 48
Source documentation
Elementary error absorption used after taking a second logarithm.
```
theorem eventually_log_add_const_le_mul (C ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop, Real.log x + C ≤ ε * x := by
…
```

theorem OAI.Problem337.marked_prefix_budget line 61

Source documentation

Convert the greedy stopping-time formula and supply size into the prefix coefficient. A fixed coarse supply bound suffices for this part.

theorem marked_prefix_budget (K J : ℕ → ℝ)
    (hKpositive : ∀ᶠ m : ℕ in atTop, 1 ≤ K m)
    (hK : ∀ᶠ m : ℕ in atTop,
      Real.log (K m) ≤ (32 / Real.log 2 + 1) * Real.log (m : ℝ) *
        Real.log (Real.log (m : ℝ)))
    (hJ : ∀ᶠ m : ℕ in atTop,
      J m ≤ 3 + (Real.log (Real.log (2 * (m : ℝ) * K m)) -
        Real.log (Real.log 2)) / Real.log 2) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ m : ℕ in atTop,
      J m ≤ (1 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)) := by
…