OAI/Probability/FreeIsing/Conditioning/CopyDifference.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.CopyDifference.pullback line 12
  2. theorem OAI.Problem367.CopyDifference.pullback_ae line 16
  3. theorem OAI.Problem367.CopyDifference.norm_pullback line 21
  4. theorem OAI.Problem367.CopyDifference.pullback_comp line 26
  5. def OAI.Problem367.CopyDifference.operator line 33
  6. theorem OAI.Problem367.CopyDifference.operator_ae line 37
  7. theorem OAI.Problem367.CopyDifference.norm_operator_apply_le line 44
  8. theorem OAI.Problem367.CopyDifference.norm_operator_le line 51
  9. theorem OAI.Problem367.CopyDifference.operator_eq_zero_of_ae_const line 56
  10. theorem OAI.Problem367.CopyDifference.operator_eq_zero_iff line 66
  11. theorem OAI.Problem367.CopyDifference.intertwines line 83
  12. def OAI.Problem367.CopyDifference.rangeClosure line 107
  13. instance OAI.Problem367.CopyDifference.rangeClosure_completeSpace line 110
  14. def OAI.Problem367.CopyDifference.toRangeClosure line 115
  15. theorem OAI.Problem367.CopyDifference.coe_toRangeClosure line 119
  16. theorem OAI.Problem367.CopyDifference.denseRange_toRangeClosure line 122
  17. theorem OAI.Problem367.CopyDifference.mapsTo_rangeClosure line 129
  18. def OAI.Problem367.CopyDifference.restrictToRangeClosure line 137
  19. theorem OAI.Problem367.CopyDifference.intertwines_toRangeClosure line 141
  20. theorem OAI.Problem367.CopyDifference.isSelfAdjoint_restrictToRangeClosure line 156