OAI/Probability/SwitchChain/DisjointCrossCellEquiv.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.DisjointMarginal.jointCrossEquiv line 16
  2. def OAI.Problem315.DisjointMarginal.degreeCellCrossEquiv line 24
  3. abbrev OAI.Problem315.DisjointMarginal.CrossCell line 31
  4. def OAI.Problem315.DisjointMarginal.stateCellCrossEquiv line 35
  5. theorem OAI.Problem315.DisjointMarginal.stateCellCrossEquiv_left line 39
  6. theorem OAI.Problem315.DisjointMarginal.stateCellCrossEquiv_right line 43
  7. theorem OAI.Problem315.DisjointMarginal.stateCellCrossEquiv_matrix line 47
  8. theorem OAI.Problem315.DisjointMarginal.sameFiber_left_iff_crossCell_right line 51
  9. theorem OAI.Problem315.DisjointMarginal.sameFiber_right_iff_crossCell_left line 57
  10. theorem OAI.Problem315.PairFibers.expectation_ker_pullback line 68
  11. theorem OAI.Problem315.DisjointMarginal.expectation_stateLeftData_crossCell line 97
  12. theorem OAI.Problem315.DisjointMarginal.expectation_stateRightData_crossCell line 108
  13. theorem OAI.Problem315.PairResampling.expectation_eq_subtype_key line 125
  14. theorem OAI.Problem315.DisjointMarginal.expectation_leftPair_eq_stateRightData line 157
  15. theorem OAI.Problem315.DisjointMarginal.expectation_rightPair_eq_stateLeftData line 166