The square root inside a closed *-subalgebra

theorem CommutingRepetition.Density.cfc_mem_of_isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) (hcl : IsClosed ↑s) {A : H →L[ℂ] H} (hsa : IsSelfAdjoint A) (hA : A ∈ s) (f : ℝ → ℝ) : cfc f A ∈ s

The continuous functional calculus of a self-adjoint element of a norm-closed *-subalgebra stays inside it.

theorem CommutingRepetition.Density.exists_sqrt_mem_of_isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) (hcl : IsClosed ↑s) {A : H →L[ℂ] H} (h0 : 0 ≤ A) (hA : A ∈ s) : ∃ r ∈ s, IsSelfAdjoint r ∧ r * r = A

A positive element of a norm-closed *-subalgebra has a self-adjoint square root inside it.

The restricted Loewner order

theorem CommutingRepetition.Density.coe_le_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) [hcl : IsClosed ↑s] (a b : ↥s) : a ≤ b ↔ ↑a ≤ ↑b

theorem CommutingRepetition.Density.coe_nonneg_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) [hcl : IsClosed ↑s] (a : ↥s) : 0 ≤ a ↔ 0 ≤ ↑a

instance CommutingRepetition.Density.instStarOrderedRing {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) [hcl : IsClosed ↑s] : StarOrderedRing ↥s

A norm-closed *-subalgebra of B(H) is a StarOrderedRing for the restricted Loewner order.

Positive functionals from vectors

theorem CommutingRepetition.Density.inner_nonneg_of_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →L[ℂ] H} (h0 : 0 ≤ T) (ξ : H) : 0 ≤ inner ℂ ξ (T ξ)

noncomputable def CommutingRepetition.Density.subVecState {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) [hcl : IsClosed ↑s] {c : ℝ} (hc : 0 ≤ c) (ξ : H) : ↥s →ₚ[ℂ] ℂ

The scaled vector functional a ↦ c·⟪ξ, a ξ⟫ on a closed *-subalgebra.

Equations

• CommutingRepetition.Density.subVecState s hc ξ = PositiveLinearMap.mk₀ { toFun := fun (a : ↥s) => ↑c * inner ℂ ξ (↑a ξ), map_add' := ⋯, map_smul' := ⋯ } ⋯

theorem CommutingRepetition.Density.subVecState_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) [hcl : IsClosed ↑s] {c : ℝ} (hc : 0 ≤ c) (ξ : H) (a : ↥s) : (subVecState s hc ξ) a = ↑c * inner ℂ ξ (↑a ξ)

noncomputable def CommutingRepetition.Density.subBobState {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) [hcl : IsClosed ↑s] (ξ : H) {B : H →L[ℂ] H} (hB : 0 ≤ B) (hcom : ∀ a ∈ s, Commute a B) : ↥s →ₚ[ℂ] ℂ

Bob's functional a ↦ ⟪ξ, a (B ξ)⟫ for a positive B commuting with s.

Equations

• CommutingRepetition.Density.subBobState s ξ hB hcom = PositiveLinearMap.mk₀ { toFun := fun (a : ↥s) => inner ℂ ξ (↑a (B ξ)), map_add' := ⋯, map_smul' := ⋯ } ⋯

theorem CommutingRepetition.Density.subBobState_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : StarSubalgebra ℂ (H →L[ℂ] H)) [hcl : IsClosed ↑s] (ξ : H) {B : H →L[ℂ] H} (hB : 0 ≤ B) (hcom : ∀ a ∈ s, Commute a B) (a : ↥s) : (subBobState s ξ hB hcom) a = inner ℂ ξ (↑a (B ξ))