OAI/Combinatorics/UniformKServer/BitPaths.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.BitSampling.mean line 8
2. def OAI.UniformKServer.BitSampling.runCost line 11
3. def OAI.UniformKServer.BitSampling.rowCost line 20
4. theorem OAI.UniformKServer.BitSampling.mean_equiv line 26
5. theorem OAI.UniformKServer.BitSampling.mean_add line 31
6. theorem OAI.UniformKServer.BitSampling.mean_const line 35
7. theorem OAI.UniformKServer.BitSampling.mean_prod line 40
8. theorem OAI.UniformKServer.BitSampling.mean_row line 45
9. theorem OAI.UniformKServer.BitSampling.bit_path_mean_proof line 51
10. theorem OAI.UniformKServer.BitSampling.bit_path_mean line 82

    Source comment

    The full finite tape has exactly b fresh unbiased bits per request.

    theorem bit_path_mean {S R : Type*} {k b : ℕ} (N : S → R → Fin k → ℕ)
        (hN : ∀ s r, ∑ j, N s r j = 2^b) (next : S → R → Fin k → S)
        (charge : S → R → Fin k → ℝ) (s : S) (w : List R) :
        mean (runCost N hN next charge s w) = rowCost (b:=b) N next charge s w := by
    …

    Mentions: OAI.UniformKServer.BitSampling.mean, OAI.UniformKServer.BitSampling.runCost, OAI.UniformKServer.BitSampling.rowCost