OAI/Analysis/KadisonKastler/GraphResolventFunctionalCalculus.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Functional calculus for the bounded Tomita resolvent

The weighted scalar estimates apply to the graph resolvent because its spectrum is contained in [0,1]. All assertions here concern bounded operators; no unbounded functional calculus is assumed.

  1. theorem OAI.KadisonKastler.graphResolvent_spectrum_bounds line 20
  2. theorem OAI.KadisonKastler.regularizedLogScalar_continuousOn line 33
  3. theorem OAI.KadisonKastler.regularizedModularLog_eq_cfc line 43
  4. theorem OAI.KadisonKastler.graphResolventCutoff_eq_cfc line 75
  5. theorem OAI.KadisonKastler.regularizedModularLog_weighted_bound line 85

    Source documentation

    Endpoint weighting turns the logarithmic difference into a norm estimate.

    theorem regularizedModularLog_weighted_bound (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ‖((regularizedModularLog M J Ω ε).val - (regularizedModularLog M J Ω δ).val) *
      graphResolventCutoff M J Ω‖ ≤ |ε - δ| := by
…

    Mentions: OAI.KadisonKastler.regularizedModularLog, OAI.KadisonKastler.graphResolventCutoff