OAI/Analysis/ModularRecovery/RealGraph.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Real Hilbert graphs and commutation with orthogonal projections.

  1. abbrev OAI.BoundedRecovery.HilbertPair line 18
  2. def OAI.BoundedRecovery.HilbertPair.pair line 22
  3. def OAI.BoundedRecovery.HilbertPair.inl line 24
  4. def OAI.BoundedRecovery.HilbertPair.inr line 28
  5. lemma OAI.BoundedRecovery.HilbertPair.inl_apply line 33
  6. lemma OAI.BoundedRecovery.HilbertPair.inr_apply line 35
  7. lemma OAI.BoundedRecovery.HilbertPair.fst_inl line 38
  8. lemma OAI.BoundedRecovery.HilbertPair.snd_inl line 40
  9. lemma OAI.BoundedRecovery.HilbertPair.fst_inr line 42
  10. lemma OAI.BoundedRecovery.HilbertPair.snd_inr line 44
  11. lemma OAI.BoundedRecovery.HilbertPair.inner_pair line 47
  12. lemma OAI.BoundedRecovery.HilbertPair.pair_add line 52
  13. lemma OAI.BoundedRecovery.HilbertPair.pair_smul line 54
  14. lemma OAI.BoundedRecovery.HilbertPair.norm_pair_le line 57
  15. lemma OAI.BoundedRecovery.HilbertPair.pair_eq_inl_add_inr line 63
  16. def OAI.BoundedRecovery.HilbertPair.diag line 66
  17. lemma OAI.BoundedRecovery.HilbertPair.diag_pair line 71
  18. lemma OAI.BoundedRecovery.HilbertPair.fst_diag line 78
  19. lemma OAI.BoundedRecovery.HilbertPair.snd_diag line 84
  20. lemma OAI.BoundedRecovery.HilbertPair.star_diag line 89
  21. lemma OAI.BoundedRecovery.HilbertPair.star_inl line 102
  22. lemma OAI.BoundedRecovery.HilbertPair.star_inr line 111
  23. def OAI.BoundedRecovery.orbitGraphMap line 122
  24. def OAI.BoundedRecovery.orbitGraph line 134
  25. lemma OAI.BoundedRecovery.orbitGraph_closed line 137
  26. lemma OAI.BoundedRecovery.orbitGraph_core_mem line 141
  27. lemma OAI.BoundedRecovery.orbitGraph_invariant line 146
  28. lemma OAI.BoundedRecovery.projection_commute_of_invariant line 155
  29. instance OAI.BoundedRecovery.orbitGraph_hasProjection line 171
  30. lemma OAI.BoundedRecovery.orbitGraph_projection_commute line 176
  31. lemma OAI.BoundedRecovery.orbitGraph_block_mem line 184
  32. def OAI.BoundedRecovery.graphBlock line 203
  33. lemma OAI.BoundedRecovery.graphBlock_mem line 208
  34. lemma OAI.BoundedRecovery.graphBlock_star line 211
  35. lemma OAI.BoundedRecovery.orbitGraph_rot_mem_orthogonal line 220
  36. lemma OAI.BoundedRecovery.projection_distance_le line 237
  37. lemma OAI.BoundedRecovery.projection_norm_le_distance_orthogonal line 244
  38. lemma OAI.BoundedRecovery.orbitGraph_projection_inl_tendsto line 251
  39. lemma OAI.BoundedRecovery.orbitGraph_projection_inr_tendsto line 275
  40. lemma OAI.BoundedRecovery.graphBlock_offdiag_xi line 302
  41. def OAI.BoundedRecovery.graphApproximant line 327
  42. lemma OAI.BoundedRecovery.graphApproximant_mem line 330
  43. lemma OAI.BoundedRecovery.graphApproximant_selfAdjoint line 335
  44. lemma OAI.BoundedRecovery.graphApproximant_xi line 342
  45. lemma OAI.BoundedRecovery.real_commutation line 353