OAI/Analysis/KadisonKastler/ModularPhaseFunctionalCalculus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Weighted norm convergence of the modular phases

Complex continuous functional calculus turns the scalar phase bound into an operator bound on the dense range of R(1-R).

  1. def OAI.KadisonKastler.modularPhaseScalar line 18
  2. theorem OAI.KadisonKastler.regularizedLogScalar_complex_continuousOn line 21
  3. theorem OAI.KadisonKastler.modularPhaseScalar_continuousOn line 30
  4. theorem OAI.KadisonKastler.regularizedModularGroup_eq_cfc line 37
  5. theorem OAI.KadisonKastler.graphResolventCutoff_eq_complex_cfc line 59
  6. theorem OAI.KadisonKastler.regularizedModularGroup_weighted_bound line 66

    Source documentation

    A bound uniform in the spectral parameter, after the dense cutoff.

    theorem regularizedModularGroup_weighted_bound (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (t : ℝ) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ‖((regularizedModularGroup M J Ω ε (Multiplicative.ofAdd t) : H →L[ℂ] H) -
      (regularizedModularGroup M J Ω δ (Multiplicative.ofAdd t) : H →L[ℂ] H)) *
      graphResolventCutoff M J Ω‖ ≤ |t| * |ε - δ| := by
…

    Mentions: OAI.KadisonKastler.regularizedModularGroup, OAI.KadisonKastler.graphResolventCutoff

  7. theorem OAI.KadisonKastler.regularizedModularGroup_cutoff_apply_bound line 87