TraceTransferBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the group approximation bound to every unitary

theorem OAI.KadisonKastler.unitary_transfer_bound_of_traceDense line 20

Source documentation

Uniform operator-norm bounds on the group elements extend to every unitary through the two finite traces and their strong continuity.

theorem unitary_transfer_bound_of_traceDense
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (hτM : FiniteVectorTrace τM) (hτN : FiniteVectorTrace τN)
    (J : Algebra M →ₗ[ℂ] E) (K : Algebra N →ₗ[ℂ] E)
    (hJ : ∀ a, ‖J a‖ = traceTwoNorm τM a)
    (hK : ∀ a, ‖K a‖ = traceTwoNorm τN a)
    (S : unitary (E →L[ℂ] E)) (θ : Algebra M →ₗ[ℂ] Algebra N)
    (hθ : ∀ a, K (θ a) = (S : E →L[ℂ] E) (J a))
    (hθU : ∀ u : unitary (Algebra M), θ u ∈ unitary (Algebra N))
    (ρ : I → unitary (Algebra M))
    (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
      ∃ i, traceTwoNorm τM ((u : Algebra M) - ρ i) < ε)
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.traceTwoNorm