OAI/NumberTheory/Ostmann/Arithmetic/LeafFrequencyBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sqrt_cost_sublinear line 13
2. theorem OAI.Ostmann.leaf_frequency_budget line 31
3. theorem OAI.Ostmann.leaf_frequency_budget_sublinear line 48

   Source documentation

   After the smooth factor exp(-r*Delta), summing the two histories' leaf frequencies costs exp(r*Delta + o(m)).

   theorem leaf_frequency_budget_sublinear (r : ℕ) (K ε : ℝ) (hε : 0 < ε) :
       ∃ M : ℝ, ∀ m : ℝ, M ≤ m → ∀ Δ : ℝ, ∀ V : ℕ,
         (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m) →
         (2 * (V : ℝ)) ^ (2 * r) * Real.exp (-(r : ℝ) * Δ + K) ≤
           Real.exp ((r : ℝ) * Δ + ε * m) := by
   …