FiniteNormalOrbit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform normal-state decay along unitary orbits

Ringrose, Lectures on the trace in a finite von Neumann algebra, Lemma 5.2, for positive normal functionals. This is the specialization needed for the normal-state orbit used in constructing a trace.

theorem OAI.BoundedHochschild.KadisonRingrose.normal_positive_subequivalent_tendsto_zero line 30

Source documentation

A normal positive functional vanishes along projections subequivalent to an orthogonal sequence in a finite algebra.

theorem normal_positive_subequivalent_tendsto_zero (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (p q : ℕ → M) (hp : ∀ n, IsStarProjection (p n))
    (hq : ∀ n, IsStarProjection (q n))
    (horth : ∀ i j, i ≠ j → q i * q j = 0)
    (hembed : ∀ n, ∃ v : PartialIso M, v.initial = p n ∧ v.final ≤ q n) :
    Tendsto (fun n => ψ (p n)) atTop (𝓝 0) := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual

theorem OAI.BoundedHochschild.KadisonRingrose.normal_positive_unitary_orbit_tendsto_zero line 48

Source documentation

Choosing a different unitary at each index still gives normal-state decay.

theorem normal_positive_unitary_orbit_tendsto_zero (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (q : ℕ → M) (hq : ∀ n, IsStarProjection (q n))
    (horth : ∀ i j, i ≠ j → q i * q j = 0) (u : ℕ → unitary M) :
    Tendsto (fun n => ψ ((u n : M) * q n * star (u n : M))) atTop (𝓝 0) := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual

theorem OAI.BoundedHochschild.KadisonRingrose.normal_positive_uniform_unitary_orbit line 83

Source documentation

Normal positive functionals are uniformly small on every unitary conjugate of the terms of an orthogonal projection sequence in a finite algebra.

theorem normal_positive_uniform_unitary_orbit (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (q : ℕ → M) (hq : ∀ n, IsStarProjection (q n))
    (horth : ∀ i j, i ≠ j → q i * q j = 0) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n in atTop, ∀ u : unitary M, ‖ψ ((u : M) * q n * star (u : M))‖ < ε := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual