ProjectionTraceContinuity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small trace projections act strongly as zero. The argument uses countable joins and geometric trace tails, rather than assuming normality of a star isomorphism between concrete von Neumann algebras.

theorem OAI.KadisonSimilarity.antitone_projection_tendsto_zero line 26

Source documentation

Decreasing projections with vanishing faithful trace converge strongly to zero in the original concrete representation.

theorem antitone_projection_tendsto_zero
    (M : VonNeumannAlgebra H) (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (hf : ∀ q, IsStarProjection q → (τ q).re = 0 → q = 0)
    (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
    (hanti : ∀ i j, i ≤ j → p i * p j = p j)
    (ht : Tendsto (fun n => (τ (p n)).re) atTop (𝓝 0)) (x : H) :
    Tendsto (fun n => (p n : H →L[ℂ] H) x) atTop (𝓝 0) := by
…

theorem OAI.KadisonSimilarity.geometric_projection_tendsto_zero line 42

Source documentation

A sequence of projections with a geometric trace bound acts strongly as zero, even in a different faithful concrete normal model.

theorem geometric_projection_tendsto_zero
    (M : VonNeumannAlgebra H) (N : VonNeumannAlgebra K)
    [IsClosed (N.toStarSubalgebra : Set (K →L[ℂ] K))]
    (e : M.toStarSubalgebra ≃⋆ₐ[ℂ] N.toStarSubalgebra)
    (υ : TracialRepresentation N)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ) (σ : N.toStarSubalgebra →ₚ[ℂ] ℂ)
    (hσ : ∀ b, σ b = υ.trace b) (he : ∀ a, σ (e a) = τ a)
    (hf : ∀ q, IsStarProjection q → (τ q).re = 0 → q = 0)
    (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
    (hpt : ∀ n, (τ (p n)).re ≤ (1 / 2 : ℝ) ^ n) (x : H) :
    Tendsto (fun n => (p n : H →L[ℂ] H) x) atTop (𝓝 0) := by
…

theorem OAI.KadisonSimilarity.projection_tendsto_zero_of_trace_tendsto_zero line 96

Source documentation

Vanishing trace of arbitrary projections forces strong convergence to zero. A hypothetical fixed violation supplies a geometric-trace sequence, which contradicts the preceding countable-join argument.

theorem projection_tendsto_zero_of_trace_tendsto_zero
    (M : VonNeumannAlgebra H) (N : VonNeumannAlgebra K)
    [IsClosed (N.toStarSubalgebra : Set (K →L[ℂ] K))]
    (e : M.toStarSubalgebra ≃⋆ₐ[ℂ] N.toStarSubalgebra)
    (υ : TracialRepresentation N)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ) (σ : N.toStarSubalgebra →ₚ[ℂ] ℂ)
    (hσ : ∀ b, σ b = υ.trace b) (he : ∀ a, σ (e a) = τ a)
    (hf : ∀ q, IsStarProjection q → (τ q).re = 0 → q = 0)
    (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
…