OAI/Combinatorics/ContingencyTables/Dense/GridCutFlow.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

From geometric cut faces to Metropolis cut flow

  1. theorem OAI.ContingencyTables.GridBoundary.edge_not_reverse line 16
  2. theorem OAI.ContingencyTables.GridBoundary.cutEdge_eq line 27
  3. def OAI.ContingencyTables.GridBoundary.cutPair line 36
  4. theorem OAI.ContingencyTables.GridBoundary.cutPair_neighbor line 45
  5. theorem OAI.ContingencyTables.GridBoundary.cutPair_weight line 52
  6. theorem OAI.ContingencyTables.GridBoundary.cutPair_injective line 59
  7. theorem OAI.ContingencyTables.GridBoundary.selected_sum_eq_filter line 79
  8. theorem OAI.ContingencyTables.GridBoundary.cut_faces_le_neighbor_flow line 88

    Source documentation

    Every geometric cut face contributes its weight once to the actual ordered cut flow. An injection suffices; no exterior or duplicate face is counted in the conductance lower bound.

    theorem cut_faces_le_neighbor_flow (Q : (Fin q → ℤ) → Prop)
    (w : Grid (I := Fin q) K → ℝ) (hw : ∀ a, 0 ≤ w a) :
…

    Mentions: OAI.ContingencyTables.GridBoundary.Grid