OAI/Combinatorics/ContingencyTables/Transport/InitialDefectChoices.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Actual remaining label choices for an initial defect

The hole and full pair are removed before the remaining row labels are chosen. This gives the finite combinatorial space underlying the exact local initialization brackets, including two removed labels in one cell.

  1. def OAI.ContingencyTables.InitialDefectChoices.Local line 21
  2. def OAI.ContingencyTables.InitialDefectChoices.encode line 24
  3. lemma OAI.ContingencyTables.InitialDefectChoices.encode_full line 31
  4. lemma OAI.ContingencyTables.InitialDefectChoices.encode_hole line 37
  5. lemma OAI.ContingencyTables.InitialDefectChoices.encode_false line 43
  6. lemma OAI.ContingencyTables.InitialDefectChoices.encode_true line 50
  7. lemma OAI.ContingencyTables.InitialDefectChoices.encode_defect line 56
  8. def OAI.ContingencyTables.InitialDefectChoices.defectEquivChoices line 71
  9. lemma OAI.ContingencyTables.InitialDefectChoices.fiber_eq_sum line 112
  10. theorem OAI.ContingencyTables.InitialDefectChoices.local_card_balance line 126

    Source documentation

    There are exactly b-u-v remaining labels in each cell. This proof uses distinct physical labels, so the coinciding-cell case is included.

    theorem local_card_balance (hpq : p≠q) (c : C) :
    Fintype.card (Local b p q c)+(if p.1=c then 1 else 0)+(if q.1=c then 1 else 0)=b c := by
…

    Mentions: OAI.ContingencyTables.InitialDefectChoices.Local

  11. lemma OAI.ContingencyTables.InitialDefectChoices.local_card line 147
  12. def OAI.ContingencyTables.InitialDefectChoices.chosen line 152
  13. lemma OAI.ContingencyTables.InitialDefectChoices.chosen_ne line 156
  14. lemma OAI.ContingencyTables.InitialDefectChoices.encode_row line 162
  15. lemma OAI.ContingencyTables.InitialDefectChoices.row_count line 179
  16. lemma OAI.ContingencyTables.InitialDefectChoices.column_count line 209
  17. def OAI.ContingencyTables.InitialDefectChoices.localWeight line 220
  18. lemma OAI.ContingencyTables.InitialDefectChoices.sum_localWeight line 225
  19. lemma OAI.ContingencyTables.InitialDefectChoices.firstLift_encode line 235
  20. theorem OAI.ContingencyTables.InitialDefectChoices.slotDefect_constant line 255

    Source documentation

    The source bracket product is the actual finite defect normalizer, with no assumption about where its missing and full labels lie.

    theorem slotDefect_constant (hpq : p≠q) (M : ℝ) :
    slotDefect pairs (LabelledFactorial.firstLift (group (InitialTransversals.cell b))
      (fun _ => M) (InitialTransversals.denominator b)) ∅ (TwoLiftStates.pair p) (TwoLiftStates.pair q)=
      M*∏ c,InitializationBrackets.bracket (b c) (if p.1=c then 1 else 0) (if q.1=c then 1 else 0) := by
…

    Mentions: OAI.ContingencyTables.LabelledFactorial.firstLift, OAI.ContingencyTables.InitialTransversals.cell, OAI.ContingencyTables.InitialTransversals.denominator, OAI.ContingencyTables.TwoLiftStates.pair, OAI.ContingencyTables.InitializationBrackets.bracket