OAI/Analysis/KadisonKastler/TomitaResolventDenseRange.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The dense range used for logarithmic approximation

The product R(1-R) of the graph resolvent and its complement has dense range. This is the precise dense set on which the weighted scalar estimates apply.

  1. theorem OAI.KadisonKastler.selfAdjoint_denseRange line 18
  2. theorem OAI.KadisonKastler.graphResolvent_injective line 28
  3. theorem OAI.KadisonKastler.one_sub_graphResolvent_injective line 37
  4. def OAI.KadisonKastler.graphResolventCutoff line 46

    Source documentation

    This product kills both singular endpoints and still has dense range.

    def graphResolventCutoff (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) : H →L[ℂ] H :=
…
  5. theorem OAI.KadisonKastler.graphResolventCutoff_selfAdjoint line 49
  6. theorem OAI.KadisonKastler.graphResolventCutoff_dense line 57