OAI/Combinatorics/ContingencyTables/Sampling/SmallResidualTotals.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Conservation makes the residual-total test redundant

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.pattern_view_totals line 16
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.pattern_small_totals line 29
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.padded_residual_totals line 50
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.profileFeasible_of_lineTests line 74

    Source documentation

    The executable tests need bounds, a local pattern and the row/column inequalities, with equality on small incident margins. No completion enumeration or additional residual-total oracle is necessary.

    theorem profileFeasible_of_lineTests (r : I → ℕ) (c : J → ℕ)
    (htotal : (∑ i,r i)=∑ j,c j) (z : SmallProfile (paperSmall r c))
    (hb : ∀ a,z a ≤ stateCapacity r c a.1.val.1 a.1.val.2)
    (hp : Pattern (paperSmall r c) (stateCapacity r c) z)
    (hr : ∀ i,smallRow (paperSmall r c) (smallView (paperSmall r c) z false) i≤r i ∧
      (r i<(dimensionAllowance (I := I) (J := J))^20 →
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.stateCapacity, OAI.ContingencyTables.SmallGraphProfiles.Pattern

  5. lemma OAI.ContingencyTables.SmallGraphProfiles.profileFeasible_lineTests line 100