OAI/Analysis/ModularRecovery/CanonicalGraph.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

The closed graph and block operators of a cyclic separating vector.

  1. structure OAI.BoundedRecovery.CyclicSeparatingData line 18
  2. def OAI.BoundedRecovery.CyclicSeparatingData.coreMap line 30
  3. def OAI.BoundedRecovery.CyclicSeparatingData.graph line 43
  4. lemma OAI.BoundedRecovery.CyclicSeparatingData.core_mem_graph line 46
  5. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_isClosed line 50
  6. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_inner_commutant line 53
  7. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_vertical line 70
  8. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_swap line 79
  9. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_horizontal line 92
  10. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_twist line 95
  11. lemma OAI.BoundedRecovery.projection_commute_real line 124
  12. def OAI.BoundedRecovery.HilbertPair.swapR line 142
  13. lemma OAI.BoundedRecovery.HilbertPair.swapR_pair line 150
  14. lemma OAI.BoundedRecovery.HilbertPair.star_swapR line 152
  15. def OAI.BoundedRecovery.HilbertPair.twistR line 163
  16. lemma OAI.BoundedRecovery.HilbertPair.twistR_pair line 174
  17. lemma OAI.BoundedRecovery.HilbertPair.star_twistR line 176
  18. instance OAI.BoundedRecovery.CyclicSeparatingData.graph_hasProjection line 195
  19. lemma OAI.BoundedRecovery.CyclicSeparatingData.projection_swap line 199
  20. lemma OAI.BoundedRecovery.CyclicSeparatingData.projection_twist line 207
  21. def OAI.BoundedRecovery.CyclicSeparatingData.diagonalBlock line 215
  22. def OAI.BoundedRecovery.CyclicSeparatingData.offDiagonalBlock line 218
  23. lemma OAI.BoundedRecovery.CyclicSeparatingData.projection_inl line 221
  24. lemma OAI.BoundedRecovery.CyclicSeparatingData.projection_inr line 225
  25. lemma OAI.BoundedRecovery.CyclicSeparatingData.projection_pair line 230
  26. lemma OAI.BoundedRecovery.CyclicSeparatingData.blocks_I line 237
  27. lemma OAI.BoundedRecovery.realLinear_smul_complex line 257
  28. lemma OAI.BoundedRecovery.realLinear_smul_conj line 266
  29. def OAI.BoundedRecovery.CyclicSeparatingData.A line 278
  30. def OAI.BoundedRecovery.CyclicSeparatingData.B line 284
  31. lemma OAI.BoundedRecovery.CyclicSeparatingData.A_apply line 286
  32. lemma OAI.BoundedRecovery.CyclicSeparatingData.B_apply line 287
  33. lemma OAI.BoundedRecovery.CyclicSeparatingData.A_symmetric_real line 289
  34. lemma OAI.BoundedRecovery.CyclicSeparatingData.B_symmetric_real line 297
  35. lemma OAI.BoundedRecovery.CyclicSeparatingData.A_selfAdjoint line 305
  36. lemma OAI.BoundedRecovery.CyclicSeparatingData.B_selfAdjoint line 314
  37. lemma OAI.BoundedRecovery.CyclicSeparatingData.A_positive line 317
  38. lemma OAI.BoundedRecovery.CyclicSeparatingData.A_norm_le line 327
  39. lemma OAI.BoundedRecovery.CyclicSeparatingData.A_le_one line 336
  40. lemma OAI.BoundedRecovery.CyclicSeparatingData.blocks_idempotent line 339
  41. lemma OAI.BoundedRecovery.CyclicSeparatingData.A_injective line 347
  42. lemma OAI.BoundedRecovery.CyclicSeparatingData.B_injective line 370