TracialHilbertConjugation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Constructing tracial conjugation on a Hilbert completion

The adjoint operation is an isometry for a faithful trace. Its extension to any dense trace-Hilbert realization is an involutive conjugate-linear isometry; no standard-form conjugation is postulated.

def OAI.KadisonKastler.starVectorMap line 20
def OAI.KadisonKastler.tracialStarIsometry line 24
Source documentation
The adjoint map extends isometrically to the trace Hilbert space.
```
def tracialStarIsometry (τ : FaithfulTracialState A) (J : A →ₗ[ℂ] E)
    (hJ : ∀ a, ‖J a‖ = traceTwoNorm τ a) (hdense : DenseRange J) : E →ₗᵢ⋆[ℂ] E :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.tracialStarIsometry_embedding line 31
theorem OAI.KadisonKastler.tracialStarIsometry_involutive line 36
def OAI.KadisonKastler.tracialHilbertConjugation line 50
Source documentation
The constructed involution, packaged as a conjugate-linear isometric equivalence.
```
def tracialHilbertConjugation (τ : FaithfulTracialState A) (J : A →ₗ[ℂ] E)
    (hJ : ∀ a, ‖J a‖ = traceTwoNorm τ a) (hdense : DenseRange J) : E ≃ₗᵢ⋆[ℂ] E :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.tracialHilbertConjugation_embedding line 56
theorem OAI.KadisonKastler.tracialHilbertConjugation_involutive line 61