OAI/Combinatorics/ContingencyTables/Transport/RowMajorPrefixFibres.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Row-major word prefixes are the literal physical exposure contexts

  1. def OAI.ContingencyTables.RowMajorEnumeration.wordChoices line 20
  2. def OAI.ContingencyTables.RowMajorEnumeration.earlierWordChoices line 27
  3. lemma OAI.ContingencyTables.RowMajorEnumeration.earlierEnumeration_cell line 35
  4. lemma OAI.ContingencyTables.RowMajorEnumeration.wordChoices_prefix line 39
  5. lemma OAI.ContingencyTables.RowMajorEnumeration.wordChoices_current line 50
  6. lemma OAI.ContingencyTables.RowMajorEnumeration.word_fibre_sum line 55
  7. theorem OAI.ContingencyTables.RowMajorEnumeration.eliminate_context_eq_word_fibre line 80

    Source documentation

    Both zeroth and first moments in the finite prefix variance are exactly the moments used by the proved physical transport inequality.

    theorem eliminate_context_eq_word_fibre (small : I → J → Bool) (B : I → J → ℕ)
    (U : ℕ) (hB : ∀ i j,small i j=true → B i j=U)
    (k : Fin (Fintype.card (Cells small))) (τ : Fin k.val → Fin (U+1)) (j : Fin (U+1))
    (F : SmallProfile small → ℝ) :
    let s := (enumeration small k).val
…

    Mentions: OAI.ContingencyTables.RowMajorEnumeration.enumeration