OAI/Probability/BinarySweep/Conditional/Placement.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.independent_event_weight line 13
  2. lemma OAI.BinaryCoordinateSweeps.conditionalWeight_factor line 25
  3. lemma OAI.BinaryCoordinateSweeps.sum_prod_grid line 35
  4. lemma OAI.BinaryCoordinateSweeps.conditionalNormalizer_eq_prod line 45
  5. abbrev OAI.BinaryCoordinateSweeps.ConditionalChoices line 71
  6. instance OAI.BinaryCoordinateSweeps.conditionalChoicesFintype line 74
  7. instance OAI.BinaryCoordinateSweeps.conditionalChoicesNonempty line 77
  8. def OAI.BinaryCoordinateSweeps.conditionalChoiceWeight line 82
  9. lemma OAI.BinaryCoordinateSweeps.conditionalChoiceWeight_nonneg line 86
  10. lemma OAI.BinaryCoordinateSweeps.conditionalChoiceWeight_sum line 91
  11. abbrev OAI.BinaryCoordinateSweeps.Placement line 104
  12. def OAI.BinaryCoordinateSweeps.placementBijection line 107
  13. def OAI.BinaryCoordinateSweeps.placementProbability line 112
  14. def OAI.BinaryCoordinateSweeps.bijectionKernel line 121
  15. lemma OAI.BinaryCoordinateSweeps.bijectionKernel_nonneg line 125
  16. lemma OAI.BinaryCoordinateSweeps.bijectionKernel_rowSum line 134
  17. lemma OAI.BinaryCoordinateSweeps.bijectionKernel_colSum line 140
  18. lemma OAI.BinaryCoordinateSweeps.placementProbability_eq_kernel line 151
  19. lemma OAI.BinaryCoordinateSweeps.placementProbability_nonneg line 161
  20. lemma OAI.BinaryCoordinateSweeps.placementProbability_rowSum line 168
  21. lemma OAI.BinaryCoordinateSweeps.placementProbability_colSum line 174
  22. lemma OAI.BinaryCoordinateSweeps.card_placement line 180
  23. def OAI.BinaryCoordinateSweeps.placementIdentification line 185
  24. def OAI.BinaryCoordinateSweeps.placementKernel line 189
  25. lemma OAI.BinaryCoordinateSweeps.placementKernel_nonneg line 193
  26. lemma OAI.BinaryCoordinateSweeps.placementKernel_rowSum line 197
  27. lemma OAI.BinaryCoordinateSweeps.placementKernel_colSum line 204
  28. def OAI.BinaryCoordinateSweeps.placementEdge line 208
  29. theorem OAI.BinaryCoordinateSweeps.placement_cycle_bound line 212