OAI/Analysis/ModularRecovery/TomitaResolvent.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Resolvents of the half-exponential and the closed Tomita graph.

  1. def OAI.BoundedRecovery.halfResolvent line 18
  2. lemma OAI.BoundedRecovery.halfResolvent_apply line 32
  3. lemma OAI.BoundedRecovery.halfResolvent_selfAdjoint line 35
  4. lemma OAI.BoundedRecovery.halfResolvent_cutoff_norm line 41
  5. lemma OAI.BoundedRecovery.RealSpectralCalculus.tendsto_calculus_of_compact_eventual line 53
  6. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfResolvent_cutoff_tendsto line 85
  7. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_iff_resolvent line 108
  8. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_isClosed line 140
  9. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_resolvent line 147
  10. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_unique line 153
  11. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_add line 157
  12. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_sub line 161
  13. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_symmetric line 165
  14. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_adjoint_iff line 183
  15. lemma OAI.BoundedRecovery.antiunitary_inner line 213
  16. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_nonneg line 235
  17. lemma OAI.BoundedRecovery.StandardModularData.J_inner_flip line 265
  18. lemma OAI.BoundedRecovery.StandardModularData.tomita_graph_inner_xi line 270
  19. lemma OAI.BoundedRecovery.StandardModularData.halfGraph_xi_Jxi line 281
  20. lemma OAI.BoundedRecovery.StandardModularData.halfGraph_Jxi_xi line 294
  21. lemma OAI.BoundedRecovery.StandardModularData.J_fixes_xi line 304
  22. lemma OAI.BoundedRecovery.StandardModularData.halfGraph_xi line 314
  23. lemma OAI.BoundedRecovery.StandardModularData.halfResolvent_xi line 318
  24. def OAI.BoundedRecovery.realMultiplier line 337
  25. lemma OAI.BoundedRecovery.realMultiplier_apply line 344
  26. def OAI.BoundedRecovery.regularizedQuotient line 347
  27. lemma OAI.BoundedRecovery.regularizedQuotient_remainder line 367
  28. lemma OAI.BoundedRecovery.exists_multiplier_approx line 378
  29. lemma OAI.BoundedRecovery.RealSpectralCalculus.kernel_of_separated_zero line 417
  30. def OAI.BoundedRecovery.centeredHalfResolvent line 446
  31. lemma OAI.BoundedRecovery.centeredHalfResolvent_apply line 463
  32. lemma OAI.BoundedRecovery.centeredHalfResolvent_zero line 466
  33. lemma OAI.BoundedRecovery.centeredHalfResolvent_strictAnti line 469
  34. lemma OAI.BoundedRecovery.centeredHalfResolvent_separated line 477
  35. lemma OAI.BoundedRecovery.realMultiplier_centeredHalfResolvent line 497
  36. lemma OAI.BoundedRecovery.StandardModularData.xi_spectralSupport line 507
  37. lemma OAI.BoundedRecovery.StandardModularData.fixes_xi line 515
  38. lemma OAI.BoundedRecovery.StandardModularData.tomita_graph_swap line 530
  39. lemma OAI.BoundedRecovery.StandardModularData.halfGraph_flip line 544
  40. lemma OAI.BoundedRecovery.StandardModularData.halfResolvent_J line 557
  41. lemma OAI.BoundedRecovery.StandardModularData.commutant_halfGraph line 563
  42. lemma OAI.BoundedRecovery.exp_eq_sq_exp_half line 591
  43. def OAI.BoundedRecovery.modularResolvent line 596
  44. def OAI.BoundedRecovery.modularMixedResolvent line 604
  45. lemma OAI.BoundedRecovery.RealSpectralCalculus.modularResolvent_halfGraph line 618
  46. lemma OAI.BoundedRecovery.RealSpectralCalculus.modularMixedResolvent_halfGraph line 639