OAI/Combinatorics/UniformKServer/ExecutableDyadic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.ExecutableDyadic.numerators line 9
2. def OAI.UniformKServer.ExecutableDyadic.rationalCost line 13
3. theorem OAI.UniformKServer.ExecutableDyadic.natFloor_cast line 18
4. theorem OAI.UniformKServer.ExecutableDyadic.numerators_repr line 21
5. theorem OAI.UniformKServer.ExecutableDyadic.numerators_sum line 42
6. theorem OAI.UniformKServer.ExecutableDyadic.rationalCost_cast line 51
7. theorem OAI.UniformKServer.ExecutableDyadic.rationalCost_bounds line 59
8. theorem OAI.UniformKServer.ExecutableDyadic.rowCost_bound line 86
9. theorem OAI.UniformKServer.ExecutableDyadic.finite_bit_perturbation line 162

   Source documentation

   Exact executable downward rounding and finite-bit realization, with the source's full-horizon error bound; every history/state is included.

   theorem finite_bit_perturbation {S R : Type*} {k : ℕ}
       (q : S → R → Fin k → ℚ) (hq : ∀ s r j, 0 ≤ q s r j)
       (hs : ∀ s r, ∑ j, q s r j = 1) (reserve : S → R → Fin k)
       (b : ℕ) (next : S → R → Fin k → S) (charge : S → R → Fin k → ℚ)
       (hn : ∀ s r j, 0 ≤ charge s r j) (D : ℝ) (hD : 0 ≤ D)
       (hd : ∀ s r j, (charge s r j : ℝ) ≤ D) :
       ∃ hN : ∀ s r, ∑ j, numerators (q s r) (reserve s r) (2^b) j = 2^b,
         (∀ s r j, j ≠ reserve s r → q s r j = 0 →
           numerators (q s r) (reserve s r) (2^b) j = 0) ∧
         (∀ s w, BitSampling.mean
           (BitSampling.runCost (fun s r => numerators (q s r) (reserve s r) (2^b))
             hN next (fun s r j => (charge s r j : ℝ)) s w) ≤
   …

   Mentions: OAI.UniformKServer.ExecutableDyadic.numerators, OAI.UniformKServer.BitSampling.mean, OAI.UniformKServer.BitSampling.runCost