OAI/Combinatorics/ContingencyTables/Transport/FlowClamp.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Binary flow magnitudes and a harmless total-domain clamp

Skew symmetry bounds a feasible entry between its two directed capacities. The executed list program clamps normalized entries to this interval. This is the identity on every valid flow and bounds every stored value even on unrelated raw program inputs.

  1. lemma OAI.ContingencyTables.FlowClamp.feasible_lower line 18
  2. lemma OAI.ContingencyTables.FlowClamp.residual_bounds line 24
  3. def OAI.ContingencyTables.FlowClamp.clamp line 31
  4. def OAI.ContingencyTables.FlowClamp.clampRealizer line 34
  5. theorem OAI.ContingencyTables.FlowClamp.polynomial_clamp line 42
  6. theorem OAI.ContingencyTables.FlowClamp.clamp_bounds line 56
  7. theorem OAI.ContingencyTables.FlowClamp.clamp_eq_normalize line 60
  8. theorem OAI.ContingencyTables.FlowClamp.clamp_feasible line 73