theorem CommutingRepetition.StdTracialAlgebra.inner_J_right (M : StdTracialAlgebra) (v w : M.H) : inner ℂ v (M.J w) = (starRingEnd ℂ) (inner ℂ (M.J v) w)

theorem CommutingRepetition.StdTracialAlgebra.inner_conjJ (M : StdTracialAlgebra) (G : M.H →L[ℂ] M.H) (ξ η : M.H) : inner ℂ ξ ((M.conjJ G) η) = (starRingEnd ℂ) (inner ℂ (M.J ξ) (G (M.J η)))

theorem CommutingRepetition.StdTracialAlgebra.conjJ_conjJ (M : StdTracialAlgebra) (G : M.H →L[ℂ] M.H) : M.conjJ (M.conjJ G) = G

theorem CommutingRepetition.StdTracialAlgebra.conjJ_zero (M : StdTracialAlgebra) : M.conjJ 0 = 0

theorem CommutingRepetition.StdTracialAlgebra.conjJ_add (M : StdTracialAlgebra) (G G' : M.H →L[ℂ] M.H) : M.conjJ (G + G') = M.conjJ G + M.conjJ G'

theorem CommutingRepetition.StdTracialAlgebra.conjJ_mul (M : StdTracialAlgebra) (G G' : M.H →L[ℂ] M.H) : M.conjJ (G * G') = M.conjJ G * M.conjJ G'

theorem CommutingRepetition.StdTracialAlgebra.conjJ_real_smul (M : StdTracialAlgebra) (c : ℝ) (G : M.H →L[ℂ] M.H) : M.conjJ (c • G) = c • M.conjJ G

theorem CommutingRepetition.StdTracialAlgebra.conjJ_star (M : StdTracialAlgebra) (G : M.H →L[ℂ] M.H) : M.conjJ (star G) = star (M.conjJ G)

theorem CommutingRepetition.StdTracialAlgebra.conjJ_isSelfAdjoint (M : StdTracialAlgebra) {E : M.H →L[ℂ] M.H} (hE : IsSelfAdjoint E) : IsSelfAdjoint (M.conjJ E)

noncomputable def CommutingRepetition.StdTracialAlgebra.conjJHom (M : StdTracialAlgebra) : (M.H →L[ℂ] M.H) →⋆ₐ[ℝ] M.H →L[ℂ] M.H

G ↦ J G J as a unital real star-algebra homomorphism.

Equations

• M.conjJHom = { toFun := M.conjJ, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

theorem CommutingRepetition.StdTracialAlgebra.conjJHom_apply (M : StdTracialAlgebra) (G : M.H →L[ℂ] M.H) : M.conjJHom G = M.conjJ G

theorem CommutingRepetition.StdTracialAlgebra.norm_conjJ_le (M : StdTracialAlgebra) (G : M.H →L[ℂ] M.H) : ‖M.conjJ G‖ ≤ ‖G‖

theorem CommutingRepetition.StdTracialAlgebra.continuous_conjJHom (M : StdTracialAlgebra) : Continuous ⇑M.conjJHom

theorem CommutingRepetition.StdTracialAlgebra.conjJ_cfc (M : StdTracialAlgebra) {E : M.H →L[ℂ] M.H} (hE : IsSelfAdjoint E) {f : ℝ → ℝ} (hf : Continuous f) : M.conjJ (cfc f E) = cfc f (M.conjJ E)

Conjugation by J commutes with the real continuous functional calculus.

theorem CommutingRepetition.StdTracialAlgebra.ν_conjJ (M : StdTracialAlgebra) {E : M.H →L[ℂ] M.H} (hE : IsSelfAdjoint E) (ξ : M.H) : BorelCalc.ν (M.conjJ E) ⋯ ξ = BorelCalc.ν E hE (M.J ξ)

The spectral measure of J E J at ξ is the spectral measure of E at J ξ.

theorem CommutingRepetition.StdTracialAlgebra.bfc_conjJ (M : StdTracialAlgebra) {E : M.H →L[ℂ] M.H} (hE : IsSelfAdjoint E) (g : ℝ → ℝ) : BorelCalc.bfc (M.conjJ E) ⋯ g = M.conjJ (BorelCalc.bfc E hE g)

Conjugation by J commutes with the Borel functional calculus.

theorem CommutingRepetition.StdTracialAlgebra.P_conjJ (M : StdTracialAlgebra) {E : M.H →L[ℂ] M.H} (hE : IsSelfAdjoint E) (I : Set ℝ) : BorelCalc.P (M.conjJ E) ⋯ I = M.conjJ (BorelCalc.P E hE I)

Conjugation by J commutes with the spectral projections.

theorem CommutingRepetition.StdTracialAlgebra.conjJ_apply_traceVector (M : StdTracialAlgebra) {T : M.H →L[ℂ] M.H} (hT : T ∈ M.vnAlg) : (M.conjJ T) M.traceVector = (star T) M.traceVector

theorem CommutingRepetition.StdTracialAlgebra.conjJ_apply_traceVector_of_sa (M : StdTracialAlgebra) {T : M.H →L[ℂ] M.H} (hT : T ∈ M.vnAlg) (hsa : IsSelfAdjoint T) : (M.conjJ T) M.traceVector = T M.traceVector