OAI/Combinatorics/UniformKServer/AutomaticTable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.AutomaticTable.assignment line 10
2. def OAI.UniformKServer.AutomaticTable.flow line 14
3. def OAI.UniformKServer.AutomaticTable.coefficient line 17
4. abbrev OAI.UniformKServer.AutomaticTable.State line 20
5. def OAI.UniformKServer.AutomaticTable.qrow line 22
6. def OAI.UniformKServer.AutomaticTable.next line 26
7. def OAI.UniformKServer.AutomaticTable.charge line 29
8. def OAI.UniformKServer.AutomaticTable.bitWidth line 32
9. def OAI.UniformKServer.AutomaticTable.counts line 34
10. theorem OAI.UniformKServer.AutomaticTable.flow_valid line 38
11. theorem OAI.UniformKServer.AutomaticTable.rationalCost_eq line 45
12. theorem OAI.UniformKServer.AutomaticTable.row_facts line 56
13. theorem OAI.UniformKServer.AutomaticTable.error_bound line 70
14. theorem OAI.UniformKServer.AutomaticTable.construct line 83

    Source documentation

    Total deterministic construction, exact-bit legal realization, and the finite-word inequality of source Proposition finite-table. The sharp coefficient is deliberately exposed as optimization against real feasible flows, not assumed from an unproved companion theorem.

    theorem construct {n k : ℕ} [NeZero k] (d : RationalMetric n) (u : Config n k)
        (H : ℕ) (D : ℝ) (hD : 0 ≤ D) (hd : ∀ x y, (d.distance x y : ℝ) ≤ D) :
        0 ≤ coefficient d u H ∧
        (∀ (F : BoundedFlow n k H ℝ) (a : ℝ), Valid d u F a →
          (coefficient d u H : ℝ) ≤ a) ∧
        (k * H^2 ≤ 2^(bitWidth k H)) ∧
        (∀ b, k * H^2 ≤ 2^b → bitWidth k H ≤ b) ∧
        ∃ hN : ∀ s r, ∑ j, counts d u H s r j = 2^(bitWidth k H),
          (∀ s r coins, BitSampling.row (counts d u H s r) (hN s r) coins ∈ labels s.2 r) ∧
          (∀ w : List (Fin n), w.length ≤ H →
            BitSampling.mean (BitSampling.runCost (counts d u H) hN next
              (fun s r j => (charge d s r j : ℝ)) ([],u) w) ≤
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.AutomaticTable.coefficient, OAI.UniformKServer.AutomaticTable.bitWidth, OAI.UniformKServer.AutomaticTable.counts, OAI.UniformKServer.BitSampling.row, OAI.UniformKServer.BitSampling.mean, OAI.UniformKServer.BitSampling.runCost, OAI.UniformKServer.AutomaticTable.next, OAI.UniformKServer.AutomaticTable.charge