OAI/Analysis/ModularRecovery/CanonicalPolar.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Real continuous functional calculus and canonical polar operators.

  1. def OAI.BoundedRecovery.realRestriction line 20
  2. lemma OAI.BoundedRecovery.realRestriction_apply line 29
  3. lemma OAI.BoundedRecovery.realRestriction_continuous line 32
  4. lemma OAI.BoundedRecovery.realRestriction_star line 35
  5. lemma OAI.BoundedRecovery.realRestriction_selfAdjoint line 44
  6. lemma OAI.BoundedRecovery.realRestriction_cfcHom_commute line 49
  7. lemma OAI.BoundedRecovery.realRestriction_cfc_commute line 74
  8. lemma OAI.BoundedRecovery.realRestriction_sqrt_commute line 82
  9. lemma OAI.BoundedRecovery.selfAdjoint_denseRange line 88
  10. def OAI.BoundedRecovery.CyclicSeparatingData.K line 107
  11. def OAI.BoundedRecovery.CyclicSeparatingData.Q line 109
  12. lemma OAI.BoundedRecovery.CyclicSeparatingData.K_eq_mul line 111
  13. lemma OAI.BoundedRecovery.CyclicSeparatingData.K_positive line 115
  14. lemma OAI.BoundedRecovery.CyclicSeparatingData.K_real line 120
  15. lemma OAI.BoundedRecovery.CyclicSeparatingData.K_injective line 126
  16. lemma OAI.BoundedRecovery.CyclicSeparatingData.Q_positive line 135
  17. lemma OAI.BoundedRecovery.CyclicSeparatingData.Q_selfAdjoint line 136
  18. lemma OAI.BoundedRecovery.CyclicSeparatingData.Q_sq line 139
  19. lemma OAI.BoundedRecovery.CyclicSeparatingData.Q_commute_A line 142
  20. lemma OAI.BoundedRecovery.CyclicSeparatingData.Q_commute_B line 147
  21. lemma OAI.BoundedRecovery.CyclicSeparatingData.Q_injective line 152
  22. lemma OAI.BoundedRecovery.CyclicSeparatingData.Q_dense line 159
  23. lemma OAI.BoundedRecovery.CyclicSeparatingData.K_dense line 162
  24. lemma OAI.BoundedRecovery.CyclicSeparatingData.norm_B_eq_Q line 165
  25. def OAI.BoundedRecovery.CyclicSeparatingData.Banti line 176
  26. lemma OAI.BoundedRecovery.CyclicSeparatingData.Banti_apply line 182
  27. def OAI.BoundedRecovery.CyclicSeparatingData.Jcl line 184
  28. lemma OAI.BoundedRecovery.CyclicSeparatingData.Jcl_Q line 187
  29. lemma OAI.BoundedRecovery.CyclicSeparatingData.norm_Jcl line 192
  30. lemma OAI.BoundedRecovery.CyclicSeparatingData.Jcl_commute_Q line 197
  31. lemma OAI.BoundedRecovery.CyclicSeparatingData.Jcl_involutive line 203
  32. def OAI.BoundedRecovery.CyclicSeparatingData.J line 212