OAI/Combinatorics/ContingencyTables/Transport/InitialTransversals.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The initial transversal sum is an actual finite row-label choice sum

For every cell, a choice of row labels gives exactly one paired transversal. Its factorial weight is the local factorial weight used in the evaluated initialization brackets.

  1. abbrev OAI.ContingencyTables.InitialTransversals.Copy line 22
  2. def OAI.ContingencyTables.InitialTransversals.cell line 24
  3. def OAI.ContingencyTables.InitialTransversals.encode line 26
  4. lemma OAI.ContingencyTables.InitialTransversals.encode_false line 30
  5. lemma OAI.ContingencyTables.InitialTransversals.encode_true line 34
  6. lemma OAI.ContingencyTables.InitialTransversals.encode_plain line 37
  7. def OAI.ContingencyTables.InitialTransversals.plainEquivChoices line 44
  8. lemma OAI.ContingencyTables.InitialTransversals.width_cell line 62
  9. lemma OAI.ContingencyTables.InitialTransversals.row_count line 76
  10. lemma OAI.ContingencyTables.InitialTransversals.column_count line 93
  11. def OAI.ContingencyTables.InitialTransversals.denominator line 99
  12. lemma OAI.ContingencyTables.InitialTransversals.firstLift_encode line 101
  13. theorem OAI.ContingencyTables.InitialTransversals.slotTotal_constant line 119

    Source documentation

    The actual paired-transversal total at a constant raw completion count M is exactly the manuscript's M*product(b+1).

    theorem slotTotal_constant (M : ℝ) :
    slotTotal pairs (firstLift (group (cell b)) (fun _ => M) (denominator b)) ∅=
      M*∏ c, ((b c:ℝ)+1) := by
…

    Mentions: OAI.ContingencyTables.InitialTransversals.cell, OAI.ContingencyTables.InitialTransversals.denominator