OAI/NumberTheory/Ostmann/Arithmetic/NonbulkHarmonicBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.nonbulkCombinatorialCost line 12
2. theorem OAI.Ostmann.nonbulkCombinatorialCost_pos line 15
3. theorem OAI.Ostmann.eventual_nonbulk_depth_budget line 19
4. theorem OAI.Ostmann.scheduled_nonbulk_harmonic_bound line 36
5. theorem OAI.Ostmann.eventual_nonbulk_cost line 72

   Source documentation

   The threshold is uniform in the growing slot type and word count.

   theorem eventual_nonbulk_cost (n B k : ℕ) (hk : 0 < k) (c ε : ℝ)
       (_hc : 0 ≤ c) (hε : 0 < ε) (hbudget : 4 * c * B ≤ ε * (k : ℝ) ^ 4) :
       ∀ᶠ L : ℝ in atTop,
         nonbulkCombinatorialCost n B * Real.exp (c * L * (2 ^ n * B : ℕ)) ≤
           Real.exp (ε * (2 ^ n : ℕ) * (spectatorBulkCount k L : ℝ)) := by
   …

   Mentions: OAI.Ostmann.nonbulkCombinatorialCost, OAI.Ostmann.spectatorBulkCount

6. theorem OAI.Ostmann.eventual_scheduled_nonbulk_cost line 104