OAI/Combinatorics/ContingencyTables/Sampling/SmallContextEnumeration.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Physical enumeration of a balanced exposure child

Every later small-cell choice occurs once, with the retained prefix fixed. The large-cell capacities remain the original capacities throughout.

  1. def OAI.ContingencyTables.SmallContextEnumeration.splitChoices line 24
  2. lemma OAI.ContingencyTables.SmallContextEnumeration.splitChoices_prefix line 30
  3. lemma OAI.ContingencyTables.SmallContextEnumeration.splitChoices_special line 40
  4. lemma OAI.ContingencyTables.SmallContextEnumeration.splitChoices_later line 50
  5. def OAI.ContingencyTables.SmallContextEnumeration.choiceProfile line 60
  6. lemma OAI.ContingencyTables.SmallContextEnumeration.choiceProfile_balanced line 70
  7. def OAI.ContingencyTables.SmallContextEnumeration.prefixChoices line 81
  8. def OAI.ContingencyTables.SmallContextEnumeration.balancedContext line 86
  9. lemma OAI.ContingencyTables.SmallContextEnumeration.balanced_false_determines line 101
  10. def OAI.ContingencyTables.SmallContextEnumeration.suffixChoices line 123
  11. def OAI.ContingencyTables.SmallContextEnumeration.balancedContextEquiv line 132
  12. def OAI.ContingencyTables.SmallContextEnumeration.prefixRaw line 163
  13. def OAI.ContingencyTables.SmallContextEnumeration.reindexChoices line 166
  14. lemma OAI.ContingencyTables.SmallContextEnumeration.embedding_coordinate_apply line 174
  15. lemma OAI.ContingencyTables.SmallContextEnumeration.physical_embedding_eq line 181
  16. theorem OAI.ContingencyTables.SmallContextEnumeration.eliminate_context_eq_balanced_mass line 234

    Source documentation

    The recursive transport child is the literal sum over physical bounded balanced profiles, retaining every large completion multiplicity.

    theorem eliminate_context_eq_balanced_mass (small : I → J → Bool) (B : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ)
    (s : I×J) (hs : small s.1 s.2=true) (σ : I×J → ℕ) (U : ℕ)
    (hB : ∀ i j, small i j=true → B i j=U)
    (hσ : ∀ a : Earlier small s, σ a.val.val ≤ U) (k : Fin (U+1))
    {n : ℕ} (e : Fin n ≃ Later small s) :
    eliminate (widths (fun _ : Fin n => U))
      (contextHard small B r c L _ (contextEquiv small s hs e U) (prefixRaw small s σ U))
      (childProfile U k.val)=
      ∑ z : BalancedProfiles small B s σ k.val, hardMarginal small B r c L (naturalProfile z.val) := by
…

    Mentions: OAI.ContingencyTables.SmallContextEnumeration.prefixRaw