OAI/Combinatorics/ContingencyTables/Dense/DenseAxisBits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact proposal frequencies from a bounded fair-bit integer

  1. def OAI.ContingencyTables.GridBoundary.directionCodeEquiv line 13
  2. def OAI.ContingencyTables.GridBoundary.axisCodeStep line 16
  3. theorem OAI.ContingencyTables.GridBoundary.axisCodeStep_sound line 23
  4. theorem OAI.ContingencyTables.GridBoundary.axisCodeStep_unique line 29
  5. theorem OAI.ContingencyTables.GridBoundary.axisCodeStep_exists line 41
  6. theorem OAI.ContingencyTables.GridBoundary.axisCodeStep_count line 58

    Source documentation

    Every valid signed direction has exactly one fair-bit integer code; all unused codes and boundary steps are rejected.

    theorem axisCodeStep_count {q K M : ℕ} (hM : q * 2 ≤ M)
    (a b : Grid (I := Fin q) K) :
…

    Mentions: OAI.ContingencyTables.GridBoundary.Grid

  7. theorem OAI.ContingencyTables.GridBoundary.dense_proposal_code_bound line 73