OAI/Probability/SwitchChain/CrossCellMoments.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.CrossCellMoments.Cell line 15
  2. instance OAI.Problem315.CrossCellMoments.cellFintype line 20
  3. theorem OAI.Problem315.CrossCellMoments.sum_cell line 23
  4. def OAI.Problem315.CrossCellMoments.offCenter line 45
  5. theorem OAI.Problem315.CrossCellMoments.offCenter_boolean line 48
  6. theorem OAI.Problem315.CrossCellMoments.sum_cell_two_product line 53
  7. theorem OAI.Problem315.CrossCellMoments.card_cell_two line 67
  8. def OAI.Problem315.CrossCellMoments.average line 75
  9. theorem OAI.Problem315.CrossCellMoments.average_product_eq line 79
  10. theorem OAI.Problem315.CrossCellMoments.average_offCenter_product line 87
  11. theorem OAI.Problem315.CrossCellMoments.sum_first_fiber line 94
  12. def OAI.Problem315.CrossCellMoments.conditionalRight line 103
  13. theorem OAI.Problem315.CrossCellMoments.conditionalRight_eq_table line 111
  14. theorem OAI.Problem315.CrossCellMoments.conditionalRight_two line 123
  15. theorem OAI.Problem315.CrossCellMoments.conditionalRight_two_span line 132
  16. theorem OAI.Problem315.CrossCellMoments.covariance_rank_one line 142
  17. theorem OAI.Problem315.CrossCellMoments.sum_second_fiber line 160
  18. def OAI.Problem315.CrossCellMoments.conditionalLeft line 169
  19. theorem OAI.Problem315.CrossCellMoments.conditionalLeft_eq_table line 177
  20. theorem OAI.Problem315.CrossCellMoments.conditionalLeft_two line 189
  21. theorem OAI.Problem315.CrossCellMoments.conditionalLeft_two_span line 208
  22. theorem OAI.Problem315.CrossCellMoments.offCenter_disjoint line 219
  23. theorem OAI.Problem315.CrossCellMoments.offCenter_disjoint_symm line 232
  24. theorem OAI.Problem315.CrossCellMoments.exists_center_of_both_offCenter line 237