OAI/Combinatorics/ContingencyTables/Rooted/TreeFeasibleMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.TreeMarginalSignature.lower_nonpositive line 15
2. lemma OAI.ContingencyTables.TreeMarginalSignature.upper_ge_capacity line 20
3. def OAI.ContingencyTables.TreeMarginalSignature.tableAssignment line 32
4. lemma OAI.ContingencyTables.TreeMarginalSignature.tableAssignment_row line 47
5. lemma OAI.ContingencyTables.TreeMarginalSignature.tableAssignment_column line 60
6. theorem OAI.ContingencyTables.TreeMarginalSignature.tableAssignment_unit line 73
7. theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_exact_ge_one_at_table line 118

   Source documentation

   A feasible table supplies an actual unit summand at its retained physical coordinate. No endpoint-mass oracle is assumed.

   theorem scalar_exact_ge_one_at_table (A : Instance I J) (alpha : ℝ)
       (Y : I → J → ℤ) (hY : ∀ i j,0 ≤ Y i j ∧ Y i j ≤ A.b i j)
       (hr : ∀ i,(∑ j,Y i j)=A.r i) (hc : ∀ j,(∑ i,Y i j)=A.c j) (t : I×J) :
       1 ≤ scalarExact A alpha t (tableAssignment A Y hY t).val := by
   …

   Mentions: OAI.ContingencyTables.TreeMarginalSignature.scalarExact, OAI.ContingencyTables.TreeMarginalSignature.tableAssignment

8. lemma OAI.ContingencyTables.TreeMarginalSignature.tableAssignment_tree_index line 139
9. theorem OAI.ContingencyTables.TreeMarginalSignature.upper_tree_endpoint line 151

   Source documentation

   Tight upper-cell attainment supplies the endpoint on the right of every lower exterior tree value.

   theorem upper_tree_endpoint (A : Instance I J) (alpha : ℝ) (t : I×J)
       (ht : A.T.Adj (.inl t.1) (.inr t.2))
       (Y : I → J → ℤ) (hY : ∀ i j,0 ≤ Y i j ∧ Y i j ≤ A.b i j)
       (hr : ∀ i,(∑ j,Y i j)=A.r i) (hc : ∀ j,(∑ i,Y i j)=A.c j)
       (hy : Y t.1 t.2=(A.b t.1 t.2:ℤ)) :
       1 ≤ scalarExact A alpha t (10*A.d*A.b t.1 t.2+A.b t.1 t.2) := by
   …

   Mentions: OAI.ContingencyTables.TreeMarginalSignature.scalarExact

10. theorem OAI.ContingencyTables.TreeMarginalSignature.lower_tree_endpoint line 168

    Source documentation

    Tight lower-cell attainment supplies the endpoint on the left of every upper exterior tree value.

    theorem lower_tree_endpoint (A : Instance I J) (alpha : ℝ) (t : I×J)
        (ht : A.T.Adj (.inl t.1) (.inr t.2))
        (Y : I → J → ℤ) (hY : ∀ i j,0 ≤ Y i j ∧ Y i j ≤ A.b i j)
        (hr : ∀ i,(∑ j,Y i j)=A.r i) (hc : ∀ j,(∑ i,Y i j)=A.c j)
        (hy : Y t.1 t.2=0) :
        1 ≤ scalarExact A alpha t (10*A.d*A.b t.1 t.2) := by
    …

    Mentions: OAI.ContingencyTables.TreeMarginalSignature.scalarExact