OAI/Combinatorics/UniformKServer/OffsetTable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.OffsetTable.assignment line 16
  2. def OAI.UniformKServer.OffsetTable.flow line 20
  3. def OAI.UniformKServer.OffsetTable.offset line 23
  4. abbrev OAI.UniformKServer.OffsetTable.State line 26
  5. def OAI.UniformKServer.OffsetTable.qrow line 28
  6. def OAI.UniformKServer.OffsetTable.next line 32
  7. def OAI.UniformKServer.OffsetTable.charge line 35
  8. def OAI.UniformKServer.OffsetTable.bitWidth line 38
  9. def OAI.UniformKServer.OffsetTable.counts line 40
  10. theorem OAI.UniformKServer.OffsetTable.computed_uniform line 44
  11. theorem OAI.UniformKServer.OffsetTable.rationalCost_eq line 55
  12. theorem OAI.UniformKServer.OffsetTable.row_facts line 66
  13. theorem OAI.UniformKServer.OffsetTable.error_bound line 81
  14. theorem OAI.UniformKServer.OffsetTable.construct line 94

    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) (A : ℚ)
    (H : ℕ) (hv : OffsetLP.Valid d u A (flow (H:=H) d u A) (offset d u A H)) (D : ℝ) (hD : 0 ≤ D) (hd : ∀ x y, (d.distance x y : ℝ) ≤ D) :
…

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.OffsetLP.Valid, OAI.UniformKServer.OffsetTable.flow, OAI.UniformKServer.OffsetTable.offset