OAI/Analysis/KadisonKastler/GraphIdentificationIndependence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Independence of the auxiliary graph identification

Changing the antiunitary used to identify the second graph coordinate conjugates the graph projection by a diagonal unitary whose first entry is the identity. Its first compression is therefore unchanged.

  1. def OAI.KadisonKastler.graphIdentificationUnitary line 20
  2. theorem OAI.KadisonKastler.graphIdentificationUnitary_vector line 24
  3. theorem OAI.KadisonKastler.graphIdentificationUnitary_mem line 43
  4. theorem OAI.KadisonKastler.graphIdentificationUnitary_star_mem line 58
  5. theorem OAI.KadisonKastler.graphProjection_identification_transport line 78
  6. theorem OAI.KadisonKastler.graphResolvent_identification_independent line 95

    Source documentation

    The graph resolvent does not depend on the auxiliary antiunitary.

    theorem graphResolvent_identification_independent (J K : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ) :
    graphResolvent M J Ω c = graphResolvent M K Ω c := by
…

    Mentions: OAI.KadisonKastler.graphResolvent