OAI/Combinatorics/ContingencyTables/Sampling/PhysicalLargeProfiles.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.PhysicalLargeProfiles.PhysicalAssignments line 14
2. def OAI.ContingencyTables.PhysicalLargeProfiles.physicalProfile line 17
3. lemma OAI.ContingencyTables.PhysicalLargeProfiles.joinedProfile_physical line 23
4. theorem OAI.ContingencyTables.PhysicalLargeProfiles.sum_joined_eq_physical line 42

   Source documentation

   The physical finite sum is independent of the order used to enumerate large cells in the recursive signature proof.

   theorem sum_joined_eq_physical {n : ℕ} (small : C → Bool) (M : C → ℕ)
       (e : Fin n ≃ LargeCell small) (z : SmallView small → ℕ)
       (F : (C×Bool → ℕ) → ℝ) :
       (∑ a : ((k : Fin n) → Fin (M (e k).val+1)),
         F (joinedProfile (fun k => M (e k).val) z a ∘ (physicalJoinEquiv small e).symm))=
         ∑ a : PhysicalAssignments small M, F (physicalProfile small M z a) := by
   …

   Mentions: OAI.ContingencyTables.PhysicalLargeProfiles.PhysicalAssignments, OAI.ContingencyTables.PhysicalLargeProfiles.physicalProfile