OAI/Analysis/KadisonKastler/PositiveReferenceHaagerup.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Haagerup witnesses at positive references

The spatial coisometries scale on every vector. Positivity identifies the new reference's polar conjugation with the old one, so the constructed modular-product-state argument applies again at the new reference.

  1. def OAI.KadisonKastler.UniversalModularCoisometries line 26

    Source documentation

    A concrete all-vector coisometry property; the spatial product below supplies it by the already constructed remote matrix sequences.

    def UniversalModularCoisometries (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) : Prop :=
…
  2. theorem OAI.KadisonKastler.haagerup_witnesses_of_polar_coisometries line 34
  3. theorem OAI.KadisonKastler.positive_reference_haagerup_witnesses line 60
  4. theorem OAI.KadisonKastler.positive_reference_noncollinear_projection_witness line 75
  5. theorem OAI.KadisonKastler.PointedMatrixSites.spatial_universal_modular_coisometries line 107