OAI/Probability/SwitchChain/TripleCountLaw.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.TripleCountLaw.Triple line 10
  2. def OAI.Problem315.TripleCountLaw.weight line 13
  3. abbrev OAI.Problem315.TripleCountLaw.Fiber line 16
  4. def OAI.Problem315.TripleCountLaw.fiberEquiv line 19
  5. theorem OAI.Problem315.TripleCountLaw.fiberEquiv_coordinate_zero line 48
  6. theorem OAI.Problem315.TripleCountLaw.fiberEquiv_coordinate_one line 53
  7. theorem OAI.Problem315.TripleCountLaw.fiberEquiv_coordinate_two line 58
  8. theorem OAI.Problem315.TripleCountLaw.weight_pos line 63
  9. theorem OAI.Problem315.TripleCountLaw.weight_fiberEquiv line 66
  10. def OAI.Problem315.TripleCountLaw.conditionalAverage line 75
  11. theorem OAI.Problem315.TripleCountLaw.conditionalAverage_reindex line 80
  12. def OAI.Problem315.TripleCountLaw.rowSum line 95
  13. theorem OAI.Problem315.TripleCountLaw.rowSum_fiberEquiv line 98
  14. theorem OAI.Problem315.TripleCountLaw.conditionalAverage_rowSum line 106
  15. theorem OAI.Problem315.TripleCountLaw.fiber_nonempty line 128
  16. theorem OAI.Problem315.TripleCountLaw.fiber_weight_sum_pos line 132
  17. def OAI.Problem315.TripleCountLaw.totalWeight line 138
  18. theorem OAI.Problem315.TripleCountLaw.totalWeight_pos line 140
  19. def OAI.Problem315.TripleCountLaw.probability line 145
  20. theorem OAI.Problem315.TripleCountLaw.probability_pos line 148
  21. theorem OAI.Problem315.TripleCountLaw.probability_sum line 151
  22. theorem OAI.Problem315.TripleCountLaw.sum_fiber_eq_indicator line 156
  23. theorem OAI.Problem315.TripleCountLaw.normalized_conditionalAverage line 164
  24. theorem OAI.Problem315.TripleCountLaw.marginal_pos line 175
  25. theorem OAI.Problem315.TripleCountLaw.normalized_conditional_rowSum line 182