OAI/Combinatorics/ContingencyTables/Dense/DenseAxisProposal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integer signed-coordinate proposals for the dense grid

  1. def OAI.ContingencyTables.GridBoundary.axisStep line 14

    Source documentation

    A signed step is rejected at the boundary of the declared finite grid.

    def axisStep (a : Grid (I := I) K) (i : I) (sign : Bool) : Option (Grid (I := I) K) :=
…

    Mentions: OAI.ContingencyTables.GridBoundary.Grid

  2. theorem OAI.ContingencyTables.GridBoundary.axisStep_sound line 30
  3. theorem OAI.ContingencyTables.GridBoundary.axisStep_complete line 57
  4. theorem OAI.ContingencyTables.GridBoundary.axisStep_some_iff line 98
  5. theorem OAI.ContingencyTables.GridBoundary.oriented_direction_unique line 103

    Source documentation

    Each neighbouring bin has exactly one signed-coordinate proposal.

    theorem oriented_direction_unique (a b : Grid (I := I) K) (i j : I) (s t : Bool)
…

    Mentions: OAI.ContingencyTables.GridBoundary.Grid