OAI/Combinatorics/ContingencyTables/Machines/QuadraticPrefixRuntime.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.QuadraticPrefixRuntime.weighted_geometric line 12
2. theorem OAI.ContingencyTables.QuadraticPrefixRuntime.quadratic_bound line 21

   Source documentation

   Quadratic simulation overhead preserves a finite expected running time. The small prefactor δ is retained through the entire estimate.

   theorem quadratic_bound (f : ℕ → ℝ) (T : ℕ) (hT : 0<T) (δ : ℝ) (hδ : 0≤δ)
       (h0 : ∀ t,0≤f t) (hm : Antitone f) (hstart : f 0≤δ)
       (hstep : ∀ N,f (T*(N+1)^2)≤δ*(1/2:ℝ)^N) :
       Summable f ∧ (∑' t,f t)≤11*δ*T := by
   …

3. theorem OAI.ContingencyTables.QuadraticPrefixRuntime.expected_time line 64

   Source documentation

   A bounded cheap prefix followed by a rare quadratic-cost correction.

   theorem expected_time (tail : ℕ → ℝ) (S T : ℕ) (hT : 0<T) (δ : ℝ) (hδ : 0≤δ)
       (h0 : ∀ t,0≤tail t) (h1 : ∀ t,tail t≤1) (hm : Antitone tail)
       (hgate : tail S≤δ)
       (hstep : ∀ N,tail (S+T*(N+1)^2)≤δ*(1/2:ℝ)^N) :
       Summable tail ∧ (∑' t,tail t)≤S+11*δ*T := by
   …