GNSProjectionContinuity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Projection continuity in the original representation follows from faithfulness and normality of the chosen trace's native GNS range.

theorem OAI.KadisonSimilarity.projection_tendsto_zero_of_normal_geometry line 23

Source documentation

Projection continuity for a faithful normal tracial geometry.

theorem projection_tendsto_zero_of_normal_geometry
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (M : VonNeumannAlgebra H) (G : TracialCornerGeometry M.toStarSubalgebra E)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ) (hτ : ∀ a, τ a = G.trace a)
    (h1 : G.trace 1 = 1) (hf : Function.Injective G.vector)
    (N : VonNeumannAlgebra E) (hN : G.left.range = N.toStarSubalgebra)
    (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
    (ht : Tendsto (fun n => (τ (p n)).re) atTop (𝓝 0)) (x : H) :
    Tendsto (fun n => (p n : H →L[ℂ] H) x) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry

theorem OAI.KadisonSimilarity.projection_tendsto_zero_of_normal_gns line 56

Source documentation

Vanishing trace of projections implies strong convergence in the original representation, using the faithful normal GNS model.

theorem projection_tendsto_zero_of_normal_gns
    (M : VonNeumannAlgebra H) (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (h1 : τ 1 = 1) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (hf : ∀ a, τ (star a * a) = 0 → a = 0) (hN : HasNormalGNS τ)
    (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
    (ht : Tendsto (fun n => (τ (p n)).re) atTop (𝓝 0)) (x : H) :
    Tendsto (fun n => (p n : H →L[ℂ] H) x) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonSimilarity.HasNormalGNS