OAI/Combinatorics/ContingencyTables/Sampling/RepairFibres.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Joint state-completion repair injections, including fixed contexts

Full row and column views retain the large completion explicitly. Their finite fibre cardinalities therefore count states with the correct completion multiplicity. The target repair is a balanced full table.

  1. def OAI.ContingencyTables.RowColumnPair line 19
  2. instance OAI.ContingencyTables.rowColumnPairFinite line 23
  3. instance OAI.ContingencyTables.rowColumnPairFintype line 42
  4. def OAI.ContingencyTables.JointDefect line 45
  5. def OAI.ContingencyTables.ResidualTables line 51
  6. instance OAI.ContingencyTables.jointDefectFintype line 56
  7. instance OAI.ContingencyTables.residualTablesFintype line 60
  8. def OAI.ContingencyTables.jointRepair line 64
  9. theorem OAI.ContingencyTables.jointRepair_injective line 75
  10. theorem OAI.ContingencyTables.jointDefect_card_le line 85

    Source documentation

    Global typewise repair domination, retaining the large completion.

    theorem jointDefect_card_le (small : I → J → Bool) (r : I → ℕ) (c : J → ℕ)
    (rbar : I → ℕ) (cbar : J → ℕ) (s t : I×J)
    (hs : small s.1 s.2=true) (ht : small t.1 t.2=true) :
    Fintype.card (JointDefect small r c rbar cbar s t) ≤
      Fintype.card (ResidualTables small r c rbar cbar) :=
…

    Mentions: OAI.ContingencyTables.JointDefect, OAI.ContingencyTables.ResidualTables

  11. def OAI.ContingencyTables.JointDefectContext line 92
  12. def OAI.ContingencyTables.ResidualChild line 98
  13. instance OAI.ContingencyTables.jointDefectContextFintype line 104
  14. instance OAI.ContingencyTables.residualChildFintype line 110
  15. theorem OAI.ContingencyTables.conditional_jointDefect_card_le line 118

    Source documentation

    The entire fixed-prefix defect fibre maps into one fixed child. The child choice depends only on the ordered defect type.

    theorem conditional_jointDefect_card_le [LinearOrder I] [LinearOrder J]
    (small : I → J → Bool) (r : I → ℕ) (c : J → ℕ)
    (rbar : I → ℕ) (cbar : J → ℕ) (s t : I×J) (σ : I×J → ℕ) (l : ℕ)
    (hs : small s.1 s.2=true) (ht : small t.1 t.2=true) (hst : RowMajorBefore s t) :
    Fintype.card (JointDefectContext small r c rbar cbar s t σ l) ≤
      Fintype.card (ResidualChild small r c rbar cbar s σ (l-1+if t.1=s.1 then 1 else 0)) := by
…

    Mentions: OAI.ContingencyTables.RowMajorBefore, OAI.ContingencyTables.JointDefectContext, OAI.ContingencyTables.ResidualChild