OAI/Combinatorics/ContingencyTables/Transport/BalancedCellFibres.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.BalancedCellFibres.Profiles line 14
2. abbrev OAI.ContingencyTables.BalancedCellFibres.Others line 15
3. def OAI.ContingencyTables.BalancedCellFibres.profile line 17
4. def OAI.ContingencyTables.BalancedCellFibres.fibre line 20
5. def OAI.ContingencyTables.BalancedCellFibres.join line 24
6. lemma OAI.ContingencyTables.BalancedCellFibres.join_at line 29
7. lemma OAI.ContingencyTables.BalancedCellFibres.join_other line 34
8. theorem OAI.ContingencyTables.BalancedCellFibres.fibre_eq_sum line 41

   Source documentation

   The fibre has no multiplicity: choosing the retained cell fixes that coordinate and leaves exactly the independent choices elsewhere.

   theorem fibre_eq_sum (M : C → ℕ) (F : (C×Bool → ℕ) → ℝ)
       (t : C) (k : Fin (M t+1)) :
       fibre M F t k=∑ a : Others M t,F (profile M (join M t k a)) := by
   …

   Mentions: OAI.ContingencyTables.BalancedCellFibres.fibre, OAI.ContingencyTables.BalancedCellFibres.Others, OAI.ContingencyTables.BalancedCellFibres.profile, OAI.ContingencyTables.BalancedCellFibres.join

9. theorem OAI.ContingencyTables.BalancedCellFibres.fibre_nonnegative line 56
10. theorem OAI.ContingencyTables.BalancedCellFibres.sum_fibre line 65

    Source documentation

    The actual one-cell fibres partition the full physical finite sum.

    theorem sum_fibre (M : C → ℕ) (F : (C×Bool → ℕ) → ℝ) (t : C) :
        (∑ k : Fin (M t+1),fibre M F t k)=∑ a : Profiles M,F (profile M a) := by
    …

    Mentions: OAI.ContingencyTables.BalancedCellFibres.fibre, OAI.ContingencyTables.BalancedCellFibres.Profiles, OAI.ContingencyTables.BalancedCellFibres.profile