OAI/Analysis/ModularRecovery/SpectralCalculus.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Unitary spectral characters, spectral support, and half-exponential bounds.

  1. lemma OAI.BoundedRecovery.spectralCharacter_apply line 18
  2. lemma OAI.BoundedRecovery.spectralCharacter_zero line 21
  3. lemma OAI.BoundedRecovery.spectralCharacter_add line 25
  4. lemma OAI.BoundedRecovery.spectralCharacter_norm line 30
  5. lemma OAI.BoundedRecovery.spectralCharacter_star line 33
  6. lemma OAI.BoundedRecovery.spectralCharacter_sub_norm_le line 37
  7. lemma OAI.BoundedRecovery.RealSpectralCalculus.unitary_zero line 55
  8. lemma OAI.BoundedRecovery.RealSpectralCalculus.unitary_add line 58
  9. lemma OAI.BoundedRecovery.RealSpectralCalculus.unitary_star line 62
  10. lemma OAI.BoundedRecovery.RealSpectralCalculus.unitary_neg_mul line 66
  11. lemma OAI.BoundedRecovery.RealSpectralCalculus.unitary_mul_neg line 70
  12. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_unitary_apply line 74
  13. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_calculus_le line 85
  14. def OAI.BoundedRecovery.RealSpectralCalculus.calculusCLM line 88
  15. lemma OAI.BoundedRecovery.RealSpectralCalculus.calculusCLM_apply line 95
  16. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_calculus_apply_le line 98
  17. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.zero line 104
  18. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.mono line 109
  19. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.add line 114
  20. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.smul line 120
  21. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.calculus line 125
  22. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.unitary line 133
  23. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.congr line 137
  24. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.fixed line 143
  25. lemma OAI.BoundedRecovery.RealSpectralCalculus.support_calculus_apply line 148
  26. lemma OAI.BoundedRecovery.RealSpectralCalculus.continuous_character_mul line 161
  27. lemma OAI.BoundedRecovery.RealSpectralCalculus.continuous_unitary_apply_compact line 191
  28. lemma OAI.BoundedRecovery.RealSpectralCalculus.continuous_unitary_apply line 198
  29. lemma OAI.BoundedRecovery.RealSpectralCalculus.continuous_unitary_apply_varying line 216
  30. def OAI.BoundedRecovery.RealSpectralCalculus.upperHalfExponential line 235
  31. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_upperHalfExponential_le line 243
  32. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.halfGraph line 251
  33. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_halfGraph_le line 263