OAI/Probability/SwitchChain/CellProjectionTransport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.CellProjectionTransport.restrictedSetoid line 15
  2. def OAI.Problem315.CellProjectionTransport.restrict line 18
  3. theorem OAI.Problem315.CellProjectionTransport.restrict_apply line 22
  4. def OAI.Problem315.CellProjectionTransport.classEquiv line 27
  5. theorem OAI.Problem315.CellProjectionTransport.expectation_restrict line 39
  6. def OAI.Problem315.CellProjectionTransport.pull line 59
  7. theorem OAI.Problem315.CellProjectionTransport.pull_apply line 63
  8. theorem OAI.Problem315.CellProjectionTransport.pull_symm line 70
  9. def OAI.Problem315.CellProjectionTransport.equivClass line 77
  10. theorem OAI.Problem315.CellProjectionTransport.expectation_pull line 89
  11. theorem OAI.Problem315.CellProjectionTransport.inner_pull line 107
  12. theorem OAI.Problem315.CellProjectionTransport.norm_sq_pull line 112
  13. theorem OAI.Problem315.CellProjectionTransport.expectation_constant line 116
  14. theorem OAI.Problem315.CellProjectionTransport.sum_expectation line 123
  15. theorem OAI.Problem315.CellProjectionTransport.expectation_centered line 132
  16. theorem OAI.Problem315.CellProjectionTransport.sum_pull line 136
  17. def OAI.Problem315.CellProjectionTransport.graphSetoid line 141
  18. theorem OAI.Problem315.CellProjectionTransport.graph_expectation line 146
  19. theorem OAI.Problem315.CellProjectionTransport.graph_expectation_restrict line 155
  20. theorem OAI.Problem315.CellProjectionTransport.graph_expectation_equiv line 163