OAI/Combinatorics/ContingencyTables/Rooted/RootedTerminalRegions.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedTerminalRegions.rootPenalty_nonnegative line 20
2. lemma OAI.ContingencyTables.RootedTerminalRegions.root_deviation_le_penalty line 27
3. lemma OAI.ContingencyTables.RootedTerminalRegions.tree_distance_le_penalty line 41
4. lemma OAI.ContingencyTables.RootedTerminalRegions.margins_of_small_penalty line 72

   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) (R : RootedCompletion.Selection A.T) (alpha : ℝ)
       (a : Profiles (cellWidth A)) (hw : 0 < actualWeight A R alpha a)
       (hp : actualPenalty A R a < 1) :
       (∀ i,(∑ j,physicalTable A a i j)=A.r i) ∧
         (∀ j,(∑ i,physicalTable A a i j)=A.c j) := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection

5. theorem OAI.ContingencyTables.RootedTerminalRegions.infeasible_in_far_or_near line 108