OAI/Analysis/KadisonKastler/GraphScaleResolvent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Resolvents under a change of graph scale

Scaling the second graph coordinate gives an exact algebraic relation between every graph resolvent and the resolvent at scale one. This relation is obtained from orthogonal projection, before using spectral calculus or an unbounded modular operator.

  1. def OAI.KadisonKastler.graphCoordinateScale line 21
  2. theorem OAI.KadisonKastler.graphCoordinateScale_zero line 27
  3. theorem OAI.KadisonKastler.graphCoordinateScale_one line 31
  4. theorem OAI.KadisonKastler.graphCoordinateScale_vector line 34
  5. theorem OAI.KadisonKastler.graphCoordinateScale_mem line 45
  6. theorem OAI.KadisonKastler.scaled_residual_inner line 59
  7. theorem OAI.KadisonKastler.graphScale_projection_identity line 73
  8. def OAI.KadisonKastler.graphScaleDenominator line 104

    Source documentation

    The positive denominator relating the rescaled graph resolvents.

    def graphScaleDenominator (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (c : ℝ) : H →L[ℂ] H :=
…
  9. theorem OAI.KadisonKastler.graphResolvent_mul_scaleDenominator line 108