RelativeNormalFunctional.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normal functionals invariant under an irreducible finite inclusion

A compact slice of the operator ball preserves both a normal functional and the trace. Relative tracial averaging makes an element of that slice scalar, so the functional is its value at one times the trace.

theorem OAI.KadisonKastler.normal_invariant_functional_eq_trace line 21

theorem OAI.KadisonKastler.vector_state_eq_trace_of_relative_central line 116

Source documentation

A unit vector whose state is central over the irreducible subalgebra implements the unique normalized trace.

theorem vector_state_eq_trace_of_relative_central
    (M R : VonNeumannAlgebra H) (hRM : R ≤ M) (P : VonNeumannAlgebra J)
    (ρ : Algebra M ≃⋆ₐ[ℂ] Algebra P) (τ : TracialRepresentation P)
    (hρ : ∀ C : ℝ, Continuous (fun b : weakOperatorBall M C =>
      ofCLM (ρ ⟨b.val.toCLM, b.property.1⟩).val))
    (hirr : ∀ a : Algebra M, a.val ∈ R.commutant → ∃ c : ℂ, a = c • 1)
    (ξ : H) (hξ : ‖ξ‖ = 1)
    (hcentral : ∀ (r : Algebra R) (a : Algebra M),
      inner ℂ ξ ((coordinateInclusion hRM r * a).val ξ) =
      inner ℂ ξ ((a * coordinateInclusion hRM r).val ξ))
    (x : Algebra M) : inner ℂ ξ (x.val ξ) = τ.trace (ρ x) := by
…

Mentions: OAI.KadisonKastler.Algebra