OAI/Combinatorics/ContingencyTables/Machines/GeometricRuntime.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

From per-attempt geometric failure to physical expected runtime

  1. lemma OAI.ContingencyTables.GeometricRuntime.block_geometric line 11
  2. theorem OAI.ContingencyTables.GeometricRuntime.expected_time_bound line 35

    Source documentation

    A real tail is required to be summable, rather than assigning a default value to a divergent infinite sum.

    theorem expected_time_bound (tail : ℕ → ℝ) (T : ℕ) (hT : 0<T)
    (ρ : ℝ) (hρ : 0≤ρ) (hρ1 : ρ<1)
    (h0 : ∀ t,0≤tail t) (hmono : Antitone tail)
    (hstep : ∀ N,tail (N*T)≤ρ^N) :
    Summable tail ∧ (∑' t,tail t)≤(T:ℝ)/(1-ρ) := by
…
  3. theorem OAI.ContingencyTables.GeometricRuntime.expected_time_half line 47