OAI/Combinatorics/ContingencyTables/Sampling/OriginalBoxPush.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transporting weighted sums through the original-table enumeration

  1. lemma OAI.ContingencyTables.OriginalBoxLaw.sum_tableAt line 13
  2. lemma OAI.ContingencyTables.OriginalBoxLaw.push_count line 23
  3. lemma OAI.ContingencyTables.OriginalBoxLaw.residualVector_law line 31

    Source documentation

    The literal correction vector is the integer residual law embedded in its enumerated box, so its total and zero weights are exact.

    lemma residualVector_law (p : IntegerLaw (Table r c) Q) (fallback : Table r c)
    (T : ℕ) (hQ : 0<Q) (hT : 0<T)
    (hdom : let _ : Nonempty (Table r c) := ⟨fallback⟩
…

    Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table