OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperChildMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual exposure child masses retain all physical completions

  1. theorem OAI.ContingencyTables.SmallContextEnumeration.eliminate_context_eq_child_card line 18
  2. theorem OAI.ContingencyTables.SmallContextEnumeration.firstPaper_child_mass line 37

    Source documentation

    In the paper's actual parameters, no extra capacity hypothesis is needed for the literal conditional completion count.

    theorem firstPaper_child_mass (r : I → ℕ) (c : J → ℕ)
    (s : I×J) (hs : paperSmall r c s.1 s.2=true) (σ : I×J → ℕ)
    (hσ : ∀ a : Earlier (paperSmall r c) s,
      σ a.val.val ≤ (dimensionAllowance (I := I) (J := J))^20)
…