OAI/Combinatorics/ContingencyTables/Transport/ChoiceContextEnumeration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallContextEnumeration.rawChoice line 22
2. def OAI.ContingencyTables.SmallContextEnumeration.earlierChoices line 25
3. lemma OAI.ContingencyTables.SmallContextEnumeration.earlierChoices_eq_iff line 29
4. def OAI.ContingencyTables.SmallContextEnumeration.ChoiceContext line 34
5. instance OAI.ContingencyTables.SmallContextEnumeration.choiceContextFintype line 38
6. def OAI.ContingencyTables.SmallContextEnumeration.choiceContextEquiv line 42
7. lemma OAI.ContingencyTables.SmallContextEnumeration.choice_fibre_sum line 58
8. lemma OAI.ContingencyTables.SmallContextEnumeration.prefixChoices_extension line 66
9. theorem OAI.ContingencyTables.SmallContextEnumeration.eliminate_context_eq_choice_fibre line 75

   Source documentation

   The child mass and every child moment are the actual finite fibre sums of balanced physical choices, retaining all large completions.

   theorem eliminate_context_eq_choice_fibre (small : I → J → Bool) (B : I → J → ℕ)
       (s : I×J) (hs : small s.1 s.2=true) (U : ℕ)
       (hB : ∀ i j,small i j=true → B i j=U)
       (τ : Earlier small s → Fin (U+1)) (k : Fin (U+1))
       {n : ℕ} (e : Fin n ≃ Later small s) (F : SmallProfile small → ℝ) :
       eliminate (widths (fun _ : Fin n => U))
         (fun p => F (assemble small s hs (prefixExtension small s U τ) U e p)) (childProfile U k.val)=
         ∑ x,fibreWeight (fibreWeight (fun x => F (rawChoice small U x))
           (earlierChoices small s U) τ) (fun x => x ⟨s,hs⟩) k x := by
   …

   Mentions: OAI.ContingencyTables.SmallContextEnumeration.rawChoice, OAI.ContingencyTables.SmallContextEnumeration.earlierChoices