OriginalTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Generator.Tracial.traceFreeHilbertVector_tendsto_of_strong line 35
Source documentation
Strong convergence in the original representation implies trace-vector convergence in the constructed representation. No norm bound or ambient Hilbert-space separability is assumed. The finite-vector formula is already proved for the faithful normalized trace of an original II₁ factor.
```
theorem traceFreeHilbertVector_tendsto_of_strong
    {I : Type*} (l : Filter I) (a : I → M.toStarSubalgebra) (x : M.toStarSubalgebra)
    (ha : ∀ v : H, Tendsto (fun i => (a i).val v) l (𝓝 (x.val v))) :
    Tendsto (fun i => π (a i) Ω) l (𝓝 (π x Ω)) := by
…
```

theorem OAI.Generator.Tracial.traceFreeHilbert_mem_of_wstar line 64

Source documentation

Forward closure transport, with the actual conditional expectation used to pass from trace-vector closure back to bounded-algebra membership.

theorem traceFreeHilbert_mem_of_wstar
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (hAM : A ≤ M.toStarSubalgebra)
    (Q : VonNeumannAlgebra K) (hQR : Q ≤ R)
    (hAQ : ∀ a : M.toStarSubalgebra, a.val ∈ A → π a ∈ Q)
    (x : M.toStarSubalgebra) (hx : x.val ∈ wstar (A : Set (H →L[ℂ] H))) :
    π x ∈ Q := by
…

Mentions: OAI.Generator.Tracial.Q, OAI.Generator.wstar

theorem OAI.Generator.Tracial.traceFreeHilbert_preimage_wotClosed line 84
Source documentation
The preimage of a represented von Neumann subalgebra is genuinely WOT closed, proved from the actual constructed representation.
```
theorem traceFreeHilbert_preimage_wotClosed
    (Q : VonNeumannAlgebra K) (hQR : Q ≤ R) :
    WOTClosed (concretePreimage (e).toStarAlgHom Q.toStarSubalgebra) := by
…
```
Mentions: OAI.Generator.Tracial.Q, OAI.Generator.WOTClosed, OAI.Generator.concretePreimage