OAI/Combinatorics/ContingencyTables/Counting/CompanionMultiplierAgreement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Only canonical pair entries affect the executed chain

The finite matrix stores one entry per pair of labels. Values of the mathematical multiplier on arbitrary noncanonical coordinate pairs do not affect any weight call, acceptance decision, or capped return.

  1. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.rationalMultiplier_congr line 21
  2. def OAI.ContingencyTables.CompanionMultiplierAgreement.Agree line 32
  3. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.agree_on_pairs line 35
  4. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.multiplier_eq line 43
  5. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.evaluatedWeight_eq line 48
  6. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.acceptance_eq line 57
  7. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.step_eq line 68
  8. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.arithmeticFinish_eq line 78
  9. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.arithmeticStep_eq line 88
  10. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.recordedWalk_eq line 98
  11. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.return_eq line 108
  12. lemma OAI.ContingencyTables.CompanionMultiplierAgreement.returns_eq line 118