DominatedVectorRealization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Vector functionals dominated on a cyclic orbit are realized in that cyclic representation. The square root of the positive intertwiner supplies the vector, so no Radon--Nikodym theorem is assumed for this bounded case.

theorem OAI.KadisonSimilarity.vector_realization_of_intertwiner line 21

Source documentation

Pull a vector functional back along a bounded intertwiner by its absolute value. This is the bounded part of the standard-form construction.

theorem vector_realization_of_intertwiner
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (L : H →L[ℂ] K)
    (hL : ∀ a, L.comp (σ a) = (ρ a).comp L) (Ω : H) :
    ∃ η : H, ∀ a, inner ℂ η (σ a η) = inner ℂ (L Ω) (ρ a (L Ω)) := by
…

theorem OAI.KadisonSimilarity.vector_realization_of_cyclic_domination line 59

Source documentation

A norm bound on the dense cyclic orbit constructs the required bounded intertwiner and hence realizes the dominated vector functional.

theorem vector_realization_of_cyclic_domination
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (Ω : H) (ξ : K) (hΩ : DenseRange (fun a : A => σ a Ω))
    (hbound : ∃ C : ℝ, ∀ a : A, ‖ρ a ξ‖ ≤ C * ‖σ a Ω‖) :
    ∃ η : H, ∀ a, inner ℂ η (σ a η) = inner ℂ ξ (ρ a ξ) := by
…