OAI/Analysis/ModularRecovery/CanonicalCalculus.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Interval functional calculus, logarithmic pullback, and nondegeneracy.

  1. abbrev OAI.BoundedRecovery.UnitInterval line 18
  2. def OAI.BoundedRecovery.intervalCoordinate line 20
  3. def OAI.BoundedRecovery.intervalWeight line 21
  4. lemma OAI.BoundedRecovery.CyclicSeparatingData.spectrum_A_interval line 25
  5. def OAI.BoundedRecovery.CyclicSeparatingData.intervalCalculus line 31
  6. lemma OAI.BoundedRecovery.CyclicSeparatingData.intervalCalculus_continuous line 36
  7. lemma OAI.BoundedRecovery.CyclicSeparatingData.intervalCalculus_coordinate line 40
  8. lemma OAI.BoundedRecovery.CyclicSeparatingData.intervalCalculus_weight line 48
  9. lemma OAI.BoundedRecovery.CyclicSeparatingData.intervalCalculus_nonneg line 52
  10. lemma OAI.BoundedRecovery.CyclicSeparatingData.intervalCalculus_norm_le line 56
  11. def OAI.BoundedRecovery.intervalLogit line 67
  12. lemma OAI.BoundedRecovery.intervalLogit_continuousAt line 69
  13. lemma OAI.BoundedRecovery.norm_weightedPullback_le line 75
  14. lemma OAI.BoundedRecovery.weightedPullback_continuous line 80
  15. def OAI.BoundedRecovery.weightedPullback line 101
  16. lemma OAI.BoundedRecovery.weightedPullback_apply line 104
  17. lemma OAI.BoundedRecovery.weightedPullback_one line 107
  18. lemma OAI.BoundedRecovery.weightedPullback_zero line 108
  19. lemma OAI.BoundedRecovery.weightedPullback_add line 109
  20. lemma OAI.BoundedRecovery.weightedPullback_smul line 111
  21. lemma OAI.BoundedRecovery.weightedPullback_mul line 113
  22. lemma OAI.BoundedRecovery.weightedPullback_star line 118
  23. lemma OAI.BoundedRecovery.complex_star_mul_self_le_of_norm_le line 124
  24. lemma OAI.BoundedRecovery.weightedPullback_square_le line 129
  25. lemma OAI.BoundedRecovery.norm_apply_le_of_star_mul_self_le line 141
  26. def OAI.BoundedRecovery.CyclicSeparatingData.weightedCalculus line 153
  27. lemma OAI.BoundedRecovery.CyclicSeparatingData.norm_weightedCalculus_apply_le line 156
  28. def OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp line 174
  29. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_K line 177
  30. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_mul_K line 183
  31. lemma OAI.BoundedRecovery.CyclicSeparatingData.norm_logCalculusOp_le line 186
  32. lemma OAI.BoundedRecovery.CyclicSeparatingData.ext_of_mul_K line 192
  33. lemma OAI.BoundedRecovery.CyclicSeparatingData.intervalCalculus_commute line 198
  34. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_commute_interval line 202
  35. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_commute_K line 210
  36. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_one line 214
  37. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_zero line 219
  38. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_add line 225
  39. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_smul line 231
  40. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_mul line 237
  41. lemma OAI.BoundedRecovery.CyclicSeparatingData.K_selfAdjoint line 249
  42. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculusOp_star line 252
  43. def OAI.BoundedRecovery.CyclicSeparatingData.logCalculus line 261
  44. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculus_weighted line 272
  45. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculus_eq_interval line 275
  46. lemma OAI.BoundedRecovery.intervalWeight_norm line 292
  47. lemma OAI.BoundedRecovery.bandMultiplier_hasCompactSupport line 299
  48. lemma OAI.BoundedRecovery.exists_compact_weight_approx line 305
  49. lemma OAI.BoundedRecovery.CyclicSeparatingData.logCalculus_nondegenerate line 350
  50. def OAI.BoundedRecovery.CyclicSeparatingData.D line 381