OAI/Combinatorics/ContingencyTables/Transport/BalancedBox.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed-total, finite-box balanced marginal closure

The display and positivity hypotheses of integer marginalization follow from the box-valid total slice. Positivity of the marginal permits induction over every finite family of balanced pairs before the equality limit.

  1. def OAI.ContingencyTables.BalancedBox.InBox line 20
  2. def OAI.ContingencyTables.BalancedBox.PositiveSlice line 22
  3. def OAI.ContingencyTables.BalancedBox.RemovalSlice line 25
  4. lemma OAI.ContingencyTables.BalancedBox.profile_inBox line 30
  5. lemma OAI.ContingencyTables.BalancedBox.profile_total line 39
  6. theorem OAI.ContingencyTables.BalancedBox.marginal_removal_slice line 45

    Source documentation

    One balanced pair preserves the exact box-valid integer signature.

    theorem marginal_removal_slice (F : ((I ⊕ Bool) → ℕ) → ℝ) (m : I → ℕ) (R M : ℕ)
    (hM : 2 ≤ M) (hpos : PositiveSlice F (profile m M M) (R+M))
    (hsig : RemovalSlice F (profile m M M) (R+M)) :
    RemovalSlice (marginal F M) m R := by
…

    Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice, OAI.ContingencyTables.BalancedBox.RemovalSlice

  7. theorem OAI.ContingencyTables.BalancedBox.marginal_positive_slice line 63

    Source documentation

    The finite sum stays strictly positive on precisely its required total slice. This is the induction input for the next balanced pair.

    theorem marginal_positive_slice (F : ((I ⊕ Bool) → ℕ) → ℝ) (m : I → ℕ) (R M : ℕ)
    (hpos : PositiveSlice F (profile m M M) (R+M)) :
    PositiveSlice (marginal F M) m R := by
…

    Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice