OAI/Combinatorics/ContingencyTables/Counting/CompanionTerminalRegions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Literal infeasible physical profiles lie in the terminal far or near regions

  1. lemma OAI.ContingencyTables.CompanionTerminalRegions.physicalRow_eq_table line 17
  2. lemma OAI.ContingencyTables.CompanionTerminalRegions.physicalColumn_eq_table line 23
  3. def OAI.ContingencyTables.CompanionTerminalRegions.integerDeviation line 33
  4. lemma OAI.ContingencyTables.CompanionTerminalRegions.deviation_eq_integer line 37
  5. lemma OAI.ContingencyTables.CompanionTerminalRegions.nonTree_bounded line 52
  6. lemma OAI.ContingencyTables.CompanionTerminalRegions.treePenalty_nonnegative line 60
  7. lemma OAI.ContingencyTables.CompanionTerminalRegions.rootPenalty_nonnegative line 72
  8. lemma OAI.ContingencyTables.CompanionTerminalRegions.root_deviation_le_penalty line 80
  9. lemma OAI.ContingencyTables.CompanionTerminalRegions.tree_distance_le_penalty line 94
  10. lemma OAI.ContingencyTables.CompanionTerminalRegions.margins_of_small_penalty line 125

    Source documentation

    Positive mass and penalty below one force every literal margin to hold: nonroots are exact indicators and root discrepancies are integral.

    lemma margins_of_small_penalty (A : Instance I J) (alpha : ℝ)
    (a : Profiles (cellWidth A)) (hw : 0 < actualWeight A alpha a)
    (hp : actualPenalty A a < 1) :
    (∀ i,(∑ j,physicalTable A a i j)=A.r i) ∧
      (∀ j,(∑ i,physicalTable A a i j)=A.c j) := by
…
  11. theorem OAI.ContingencyTables.CompanionTerminalRegions.infeasible_in_far_or_near line 155