OAI/Combinatorics/ContingencyTables/Transport/BalancedCompletionMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.SmallGraphProfiles.balanced_fibre_views_eq line 17
2. def OAI.ContingencyTables.SmallGraphProfiles.balancedFibreTable line 29
3. abbrev OAI.ContingencyTables.SmallGraphProfiles.BalancedJoint line 39
4. def OAI.ContingencyTables.SmallGraphProfiles.balancedJointTable line 45
5. lemma OAI.ContingencyTables.SmallGraphProfiles.balancedJointTable_injective line 51
6. lemma OAI.ContingencyTables.SmallGraphProfiles.word_mass_eq_balancedJoint_card line 68
7. theorem OAI.ContingencyTables.SmallGraphProfiles.word_mass_le_padded_count line 79

   Source documentation

   This inequality retains all large-cell multiplicities and counts every balanced word exactly once.

   theorem word_mass_le_padded_count (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L U : ℕ)
       (hB : ∀ i j,small i j=true → B i j=U) :
       (∑ a,wordWeight small B r c L U a) ≤
         (Fintype.card (Table (fun i => r i+rowLargeCount small i*L)
           (fun j => c j+columnLargeCount small j*L)):ℝ) := by
   …

   Mentions: OAI.ContingencyTables.Table