OAI/Combinatorics/UniformKServer/DyadicRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.roundedRow line 8

    Source documentation

    Downward rounding at every label other than the reserved allowed label. The reserved label receives the remainder, exactly as in Section 02.

    noncomputable def roundedRow {k : ℕ} (q : Fin k → ℝ) (j₀ : Fin k) (B : ℕ)
    (j : Fin k) : ℝ :=
…
  2. theorem OAI.UniformKServer.floor_fraction_bounds line 15
  3. theorem OAI.UniformKServer.round_row_sum line 31
  4. theorem OAI.UniformKServer.round_row_nonneg line 47
  5. def OAI.UniformKServer.rowLoss line 64
  6. theorem OAI.UniformKServer.rowLoss_bounds line 68
  7. theorem OAI.UniformKServer.round_reserve line 83
  8. theorem OAI.UniformKServer.round_row_expectation line 92