TracialInputTransport.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Transport of the discharged tracial inputs

These are coordinate changes through actual star algebra equivalences. The concrete normal representation is retained as algebraic data; neither rounding nor existence of a right support is assumed in the concrete model.

theorem OAI.KadisonSimilarity.starAlgHom_preserves_nonneg line 21
Source documentation
A star homomorphism of C-star algebras preserves positivity.
```
theorem starAlgHom_preserves_nonneg (f : A →⋆ₐ[ℂ] B) {a : A} (ha : 0 ≤ a) : 0 ≤ f a := by
…
```
def OAI.KadisonSimilarity.transportedPositiveTrace line 27
Source documentation
Positive functional in the coordinates of the target algebra.
```
def transportedPositiveTrace (τ : A →ₚ[ℂ] ℂ) (e : A ≃⋆ₐ[ℂ] B) : B →ₚ[ℂ] ℂ :=
…
```
theorem OAI.KadisonSimilarity.transportedPositiveTrace_apply line 31
theorem OAI.KadisonSimilarity.transportedPositiveTrace_map line 34
theorem OAI.KadisonSimilarity.transportedPositiveTrace_tracial line 37

theorem OAI.KadisonSimilarity.preGNS_norm_map_eq line 45

Source documentation

Trace preservation is exactly the norm preservation needed for rounding.

theorem preGNS_norm_map_eq (τA : A →ₚ[ℂ] ℂ) (τB : B →ₚ[ℂ] ℂ)
    (e : A →⋆ₐ[ℂ] B) (hτ : ∀ a, τB (e a) = τA a) (a : A) :
    ‖τB.toPreGNS (e a)‖ = ‖τA.toPreGNS a‖ := by
…

theorem OAI.KadisonSimilarity.spectralProjectionRoundingInput_of_equiv line 52

Source documentation

Rounding is invariant under a trace-preserving star equivalence.

theorem spectralProjectionRoundingInput_of_equiv
    (τA : A →ₚ[ℂ] ℂ) (τB : B →ₚ[ℂ] ℂ) (e : A ≃⋆ₐ[ℂ] B)
    (hτ : ∀ a, τB (e a) = τA a) (rounding : SpectralProjectionRoundingInput τB) :
    SpectralProjectionRoundingInput τA := by
…

Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput

theorem OAI.KadisonSimilarity.tracialRightSupportInput_of_equiv line 70

Source documentation

Right supports transfer through the same actual algebraic equivalence.

theorem tracialRightSupportInput_of_equiv
    (τA : A → ℝ) (τB : B → ℝ) (e : A ≃⋆ₐ[ℂ] B) (hτ : ∀ a, τB (e a) = τA a)
    (q : A) (S : StarSubalgebra ℂ A)
    (support : TracialRightSupportInput τB (e q) (S.map e.toStarAlgHom)) :
    TracialRightSupportInput τA q S := by
…

Mentions: OAI.KadisonSimilarity.TracialRightSupportInput

def OAI.KadisonSimilarity.equivalenceOfConcreteRange line 101
Source documentation
A faithful normal realization with precisely this represented range supplies the star equivalence; no tracial input is needed for this step.
```
def equivalenceOfConcreteRange (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hinj : Function.Injective ρ) (hrange : ρ.range = P.toStarSubalgebra) :
    A ≃⋆ₐ[ℂ] P.toStarSubalgebra :=
…
```
theorem OAI.KadisonSimilarity.spectralProjectionRoundingInput_of_concrete_equiv line 117
Source documentation
The concrete spectral theorem discharges rounding after an actual faithful normal realization of the abstract algebra.
```
theorem spectralProjectionRoundingInput_of_concrete_equiv
    (τ : A →ₚ[ℂ] ℂ) (e : A ≃⋆ₐ[ℂ] P.toStarSubalgebra) :
    SpectralProjectionRoundingInput τ :=
…
```
Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput

theorem OAI.KadisonSimilarity.tracialRightSupportInput_of_concrete_equiv line 126

Source documentation

The concrete polar construction discharges right supports in the abstract algebra through that same faithful normal realization.

theorem tracialRightSupportInput_of_concrete_equiv
    (τ : A →ₚ[ℂ] ℂ) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (e : A ≃⋆ₐ[ℂ] P.toStarSubalgebra) (q : A) (hq : IsStarProjection q)
    (S : StarSubalgebra ℂ A) : TracialRightSupportInput (fun a => (τ a).re) q S := by
…

Mentions: OAI.KadisonSimilarity.TracialRightSupportInput

theorem OAI.KadisonSimilarity.spectralProjectionRoundingInput_of_concrete_range line 138
Source documentation
A faithful representation whose range is the stated von Neumann algebra supplies all the coordinates needed for spectral rounding.
```
theorem spectralProjectionRoundingInput_of_concrete_range
    (τ : A →ₚ[ℂ] ℂ) (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hinj : Function.Injective ρ) (hrange : ρ.range = P.toStarSubalgebra) :
    SpectralProjectionRoundingInput τ :=
…
```
Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput

theorem OAI.KadisonSimilarity.tracialRightSupportInput_of_concrete_range line 147

Source documentation

The same actual representation supplies the propagation right supports for every projection and every subalgebra.

theorem tracialRightSupportInput_of_concrete_range
    (τ : A →ₚ[ℂ] ℂ) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hinj : Function.Injective ρ)
    (hrange : ρ.range = P.toStarSubalgebra)
    (q : A) (hq : IsStarProjection q) (S : StarSubalgebra ℂ A) :
    TracialRightSupportInput (fun a => (τ a).re) q S :=
…

Mentions: OAI.KadisonSimilarity.TracialRightSupportInput