OAI/Analysis/ModularRecovery/PolarCutoff.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Continuous functional calculus and bounded polar truncation in C*-algebras.

  1. def OAI.BoundedRecovery.cutoffFunction line 16
  2. lemma OAI.BoundedRecovery.cutoffFunction_continuous line 18
  3. lemma OAI.BoundedRecovery.cutoffFunction_nonneg line 24
  4. lemma OAI.BoundedRecovery.cutoffFunction_le_one line 28
  5. lemma OAI.BoundedRecovery.cutoffFunction_eq_one line 32
  6. lemma OAI.BoundedRecovery.cutoffFunction_norm_bound line 36
  7. lemma OAI.BoundedRecovery.cutoffFunction_error_bound line 50
  8. def OAI.BoundedRecovery.polarCutoff line 74
  9. lemma OAI.BoundedRecovery.polarCutoff_square line 76
  10. lemma OAI.BoundedRecovery.polarCutoff_error_square line 90
  11. lemma OAI.BoundedRecovery.norm_polarCutoff_le line 110
  12. lemma OAI.BoundedRecovery.polarCutoff_error_le line 123
  13. def OAI.BoundedRecovery.cutoffLeftFunction line 144
  14. def OAI.BoundedRecovery.cutoffRightFunction line 147
  15. lemma OAI.BoundedRecovery.cutoffLeftFunction_continuous line 150
  16. lemma OAI.BoundedRecovery.cutoffRightFunction_continuous line 157
  17. lemma OAI.BoundedRecovery.cutoffLeftFunction_sq line 163
  18. lemma OAI.BoundedRecovery.cutoffRightFunction_sq line 169
  19. lemma OAI.BoundedRecovery.cutoffLeftFunction_mul_right line 175
  20. lemma OAI.BoundedRecovery.cutoff_right_loss line 187
  21. lemma OAI.BoundedRecovery.cutoff_left_loss line 203
  22. def OAI.BoundedRecovery.cutoffLeft line 216
  23. def OAI.BoundedRecovery.cutoffRight line 219
  24. lemma OAI.BoundedRecovery.cutoffLeft_mul_right line 222
  25. lemma OAI.BoundedRecovery.cutoffRight_loss line 235
  26. lemma OAI.BoundedRecovery.cutoffLeft_loss line 261