OAI/Combinatorics/ContingencyTables/Transport/BalancedPhysicalPartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.BalancedCellFibres.SmallProfiles line 14
2. def OAI.ContingencyTables.BalancedCellFibres.partition line 17
3. def OAI.ContingencyTables.BalancedCellFibres.smallDisplay line 30
4. lemma OAI.ContingencyTables.BalancedCellFibres.partition_profile line 33
5. theorem OAI.ContingencyTables.BalancedCellFibres.sum_eq_small_large line 47

   Source documentation

   This exact finite product split removes all artificial labels and enumerations from the companion's terminal normalizer.

   theorem sum_eq_small_large (small : C → Bool) (M : C → ℕ)
       (F : (C×Bool → ℕ) → ℝ) :
       (∑ a : Profiles M,F (profile M a))=
         ∑ s : SmallProfiles small M,∑ a : PhysicalAssignments small M,
           F (physicalProfile small M (smallDisplay small M s) a) := by
   …

   Mentions: OAI.ContingencyTables.BalancedCellFibres.Profiles, OAI.ContingencyTables.BalancedCellFibres.profile, OAI.ContingencyTables.BalancedCellFibres.SmallProfiles, OAI.ContingencyTables.BalancedCellFibres.smallDisplay