TraceHilbertExtension.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

An ambient extension of the finite factor trace representation

Extend the scalar trace state by Hahn–Banach, form its GNS representation, and compress to the original trace Hilbert space. This supplies the contractive ambient map required to transport finite tracial injectivity.

def OAI.KadisonKastler.traceFreePositiveFunctional line 53
Source documentation
The constructed trace as a positive linear functional.
```
def traceFreePositiveFunctional : Algebra M →ₚ[ℂ] ℂ where
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.exists_traceFree_state_extension line 68
Source documentation
Only the scalar state extension is used; it carries no operator-algebra conclusion.
```
theorem exists_traceFree_state_extension :
    ∃ σ : (H →L[ℂ] H) →ₚ[ℂ] ℂ, σ 1 = 1 ∧
      ∀ a : Algebra M, σ a.val = τ a := by
…
```
Mentions: OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.traceStatePreEmbedding line 79
Source documentation
The algebraic trace Hilbert space embeds in the extended state's GNS space.
```
def traceStatePreEmbedding : E →ₗ[ℂ] σ.GNS where
…
```
theorem OAI.KadisonKastler.traceStatePreEmbedding_norm line 85

def OAI.KadisonKastler.traceStateEmbedding line 100

Source documentation

Completion of the trace-state isometry.

def traceStateEmbedding (hσ : ∀ a : Algebra M, σ a.val =
      traceFreeTrace (M := M) hfactor hdiff hfinite hunit a) : K →ₗᵢ[ℂ] σ.GNS :=
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.traceStateEmbedding_inclusion line 106
theorem OAI.KadisonKastler.traceStateEmbedding_intertwines line 114
Source documentation
The extended state's representation agrees with the trace representation on its subspace.
```
theorem traceStateEmbedding_intertwines
    (hσ : ∀ a : Algebra M, σ a.val =
      traceFreeTrace (M := M) hfactor hdiff hfinite hunit a) (a : Algebra M) (x : K) :
…
```
Mentions: OAI.KadisonKastler.Algebra

def OAI.KadisonKastler.traceFreeAmbientExtension line 135

Source documentation

Compress the ambient GNS representation to the canonical trace space.

def traceFreeAmbientExtension (hσ : ∀ a : Algebra M, σ a.val =
      traceFreeTrace (M := M) hfactor hdiff hfinite hunit a) : (H →L[ℂ] H) →ₗ[ℂ] (K →L[ℂ] K) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.traceFreeAmbientExtension_norm line 149
theorem OAI.KadisonKastler.traceFreeAmbientExtension_agrees line 173
theorem OAI.KadisonKastler.exists_traceFreeAmbientExtension line 187
Source documentation
An actual contractive ambient extension of the trace representation.
```
theorem exists_traceFreeAmbientExtension :
    ∃ R : (H →L[ℂ] H) →ₗ[ℂ] (K →L[ℂ] K),
      (∀ T, ‖R T‖ ≤ ‖T‖) ∧ ∀ a : Algebra M, R a.val = π a := by
…
```
Mentions: OAI.KadisonKastler.Algebra