OAI/Analysis/KadisonKastler/GraphScaleFunctionalCalculus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Bounded functional calculus formula for every graph scale

  1. def OAI.KadisonKastler.graphScaleScalar line 15
  2. theorem OAI.KadisonKastler.graphScaleScalar_pos line 17
  3. theorem OAI.KadisonKastler.graphScaleDenominator_eq_cfc line 25
  4. def OAI.KadisonKastler.graphScaleInverse line 37
  5. theorem OAI.KadisonKastler.graphScaleInverse_continuousOn line 41
  6. theorem OAI.KadisonKastler.graphScaleDenominator_mul_inverse line 49
  7. theorem OAI.KadisonKastler.graphResolvent_eq_mul_scaleInverse line 63
  8. theorem OAI.KadisonKastler.graphResolvent_eq_cfc_scale line 73

    Source documentation

    An arbitrary nonzero graph scale is a bounded rational function of the scale-one resolvent.

    theorem graphResolvent_eq_cfc_scale (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    {c : ℝ} (hc : c ≠ 0) :
    graphResolvent M J Ω c =
      cfc (fun s => s / graphScaleScalar c s) (graphResolvent M J Ω 1) := by
…

    Mentions: OAI.KadisonKastler.graphResolvent, OAI.KadisonKastler.graphScaleScalar