OAI/Combinatorics/ContingencyTables/Sampling/AllSmallFibres.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.PhysicalCompletionFibres.completionFibre_subsingleton line 14

   Source documentation

   When every cell is retained, both views are fixed by the profile.

   theorem completionFibre_subsingleton (small : I → J → Bool) (B : I → J → ℕ)
       (r rbar : I → ℕ) (c cbar : J → ℕ) (z : SmallProfile small)
       (hsmall : ∀ i j,small i j=true) :
       Subsingleton (CompletionFibre small B r rbar c cbar z) := by
   …

   Mentions: OAI.ContingencyTables.PhysicalCompletionFibres.SmallProfile, OAI.ContingencyTables.PhysicalCompletionFibres.CompletionFibre

2. lemma OAI.ContingencyTables.SmallGraphProfiles.allSmall_of_no_large_rectangle line 42
3. lemma OAI.ContingencyTables.SmallGraphProfiles.paperFibre_card_allSmall line 58
4. lemma OAI.ContingencyTables.SmallGraphProfiles.stateWeight_allSmall line 65

   Source documentation

   No dense sampler or numerical integral is needed in this branch.

   lemma stateWeight_allSmall (hsmall : ∀ i j,paperSmall r c i j=true)
       (z : PaperStates r c) : stateWeight r c z=1 := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.stateWeight