Conjugating by the square root of a positive element in a C⋆-algebra

This file defines conjSqrt c a as sqrt c * a * sqrt c, and develops API for this operation.

Main declarations

• conjSqrt c: the map fun a => sqrt c * a * sqrt c, bundled as a continuous linear map,

noncomputable def CFC.conjSqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] (c : A) : A →L[ℝ] A

Conjugation by the square root of an element, i.e. sqrt c * a * sqrt c.

Equations

• CFC.conjSqrt c = { toLinearMap := LinearMap.mulLeftRight ℝ (CFC.sqrt c, CFC.sqrt c), cont := ⋯ }

@[simp]

theorem CFC.toLinearMap_conjSqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] (c : A) : ↑(conjSqrt c) = LinearMap.mulLeftRight ℝ (sqrt c, sqrt c)

theorem CFC.conjSqrt_apply {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] {c a : A} : (conjSqrt c) a = sqrt c * a * sqrt c

theorem CFC.conjSqrt_of_not_nonneg {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] {c a : A} (hc : ¬0 ≤ c) : (conjSqrt c) a = 0

theorem CFC.conjSqrt_monotone {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] {c : A} : Monotone ⇑(conjSqrt c)

theorem CFC.conjSqrt_le_conjSqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] {c a b : A} (h : a ≤ b) : (conjSqrt c) a ≤ (conjSqrt c) b

theorem CFC.isStrictlyPositive_conjSqrt_iff {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c a : A) (hc : IsStrictlyPositive c := by cfc_tac) : IsStrictlyPositive ((conjSqrt c) a) ↔ IsStrictlyPositive a

theorem CFC.ringInverse_conjSqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c a : A) (hc : IsStrictlyPositive c := by cfc_tac) : Ring.inverse ((conjSqrt c) a) = (conjSqrt (Ring.inverse c)) (Ring.inverse a)

theorem CFC.conjSqrt_ringInverse_conjSqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c a : A) (hc : IsStrictlyPositive c := by cfc_tac) : (conjSqrt (Ring.inverse c)) ((conjSqrt c) a) = a

theorem CFC.conjSqrt_conjSqrt_ringInverse {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c a : A) (hc : IsStrictlyPositive c := by cfc_tac) : (conjSqrt c) ((conjSqrt (Ring.inverse c)) a) = a

theorem CFC.conjSqrt_one {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c : A) (hc : 0 ≤ c := by cfc_tac) : (conjSqrt c) 1 = c

theorem CFC.conjSqrt_ringInverse_self {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c : A) (hc : IsStrictlyPositive c := by cfc_tac) : (conjSqrt (Ring.inverse c)) c = 1