RareBranchRuntime.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The correction probability absorbs the cost of finite tabulation

lemma OAI.ContingencyTables.RareBranchRuntime.linear_le_square_add line 12
Source documentation
The coefficient in a fixed exponential running-time bound need not be smaller than the coefficient used in the sampler's precision schedule.
```
lemma linear_le_square_add (k s : ℕ) : k * s ≤ s ^ 2 + k ^ 2 := by
…
```
lemma OAI.ContingencyTables.RareBranchRuntime.dyadic_linear_bound line 17
theorem OAI.ContingencyTables.RareBranchRuntime.polynomial_tabulation_bound line 25
Source documentation
A polynomial in an exponential tabulation size remains affordable after multiplying by the rare-branch probability 2⁻ᴰ.
```
theorem polynomial_tabulation_bound (p : Polynomial ℕ) (A s a D : ℕ)
    (hD : s^2≤D) :
    p.eval (A*2^(a*s))≤2^D*(p.eval A*2^((a*p.natDegree)^2)) := by
…
```
lemma OAI.ContingencyTables.RareBranchRuntime.square_le_precision line 37
theorem OAI.ContingencyTables.RareBranchRuntime.correction_tabulation_bound line 44
Source documentation
The manuscript's precision d⁶ b² absorbs any fixed polynomial of the grid size 2^(10*d*b), up to a constant and a polynomial factor.
```
theorem correction_tabulation_bound (p : Polynomial ℕ) (A d b : ℕ)
    (hd : 1≤d) :
    p.eval (A*2^(10*(d*b)))≤
      2^(d^6*b^2)*(p.eval A*2^((10*p.natDegree)^2)) :=
…
```
theorem OAI.ContingencyTables.RareBranchRuntime.expected_correction_cost line 50

theorem OAI.ContingencyTables.RareBranchRuntime.expected_branch_time line 60

Source documentation

A finite ordinary prefix followed by a rare correction adds only the probability-weighted correction tail to the expected physical runtime.

theorem expected_branch_time (tail correction : ℕ → ℝ) (S : ℕ) (delta : ℝ)
    (h0 : ∀ n,0≤tail n) (h1 : ∀ n,tail n≤1)
    (hc : Summable correction)
    (hafter : ∀ n,tail (n+S)≤delta*correction n) :
    Summable tail ∧ (∑' n,tail n)≤(S:ℝ)+delta*(∑' n,correction n) := by
…