OAI/Combinatorics/ContingencyTables/Transport/RationalProducts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite product laws for the independent bounded offset draws

  1. def OAI.ContingencyTables.FirstSuccess.piLaw line 15
  2. theorem OAI.ContingencyTables.FirstSuccess.variation_pi_succ line 23
  3. theorem OAI.ContingencyTables.FirstSuccess.variation_pi line 39

    Source documentation

    Errors in independent coordinate draws add before any success test or deterministic table completion is applied.

    theorem variation_pi {n : ℕ} (α : Fin n → Type*) [∀ i, Fintype (α i)]
    (p q : ∀ i, RationalLaw (α i)) :
    variation (piLaw p) (piLaw q) ≤ ∑ i, variation (p i) (q i) := by
…

    Mentions: OAI.ContingencyTables.FirstSuccess.variation, OAI.ContingencyTables.FirstSuccess.piLaw