OAI/Combinatorics/ContingencyTables/Rooted/RootedTreeFeasibleMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedTreeMarginal.tableAssignment_unit line 18
2. theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_exact_ge_one_at_table line 67

   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) (R : RootedCompletion.Selection A.T) (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 R alpha t (tableAssignment A Y hY t).val := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarExact

3. theorem OAI.ContingencyTables.RootedTreeMarginal.upper_tree_endpoint line 90

   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) (R : RootedCompletion.Selection A.T) (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 R alpha t (10*A.d*A.b t.1 t.2+A.b t.1 t.2) := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarExact

4. theorem OAI.ContingencyTables.RootedTreeMarginal.lower_tree_endpoint line 107

   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) (R : RootedCompletion.Selection A.T) (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 R alpha t (10*A.d*A.b t.1 t.2) := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarExact