FiniteNormalState.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Normal states and the remaining tracial averaging step

A normal state faithful on central projections is faithful on positive central elements. The property passes to its actual central corner. Composing such a state with a faithful normal positive central averaging map gives a faithful normal tracial state. Constructing that map from finiteness is a separate remaining theorem; no such map is postulated here.

lemma OAI.BoundedHochschild.KadisonRingrose.positive_contraction_zero_mul line 31
Source documentation
A positive functional vanishing on a positive contraction annihilates its left multiples.
```
lemma positive_contraction_zero_mul (ψ : M →ₚ[ℂ] ℂ) {c : M}
    (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (hψc : ψ c = 0) (b : M) : ψ (c * b) = 0 := by
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.exists_null_support_projection line 44
Source documentation
The support projection of a null positive contraction is null for a normal functional.
```
lemma exists_null_support_projection (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ) {c : M}
    (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (hψc : ψ c = 0) :
    ∃ r : M, IsSupportProjection c r ∧ ψ r = 0 := by
…
```
Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.IsSupportProjection

theorem OAI.BoundedHochschild.KadisonRingrose.normal_state_faithful_on_positive_center line 64

Source documentation

Normality upgrades faithfulness on central projections to positive central elements.

theorem normal_state_faithful_on_positive_center (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (hfaith : ∀ p : M, IsStarProjection p → (∀ a : M, p * a = a * p) → ψ p = 0 → p = 0)
    {a : M} (ha : 0 ≤ a) (hcentral : ∀ b : M, a * b = b * a) (hψa : ψ a = 0) :
    a = 0 := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual

theorem OAI.BoundedHochschild.KadisonRingrose.central_faithful_state_on_corner line 91

Source documentation

A state faithful on the central subprojections of p induces a normal state faithful on all central projections of the actual corner pMp.

theorem central_faithful_state_on_corner (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (hp : IsStarProjection p) (hc : ∀ a : M, p * a = a * p)
    (hstate : HasCentralFaithfulNormalState e p) :
    ∃ ψ : Corner p hp →ₚ[ℂ] ℂ,
      TraceInPredual (cornerPredualEquiv p hp e) ψ ∧ ψ 1 = 1 ∧
      ∀ q : Corner p hp, IsStarProjection q →
        (∀ a : Corner p hp, q * a = a * q) → ψ q = 0 → q = 0 := by
…

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

theorem OAI.BoundedHochschild.KadisonRingrose.tracial_state_of_normal_center_average line 113

Source documentation

Actual normal central averaging data convert a center-faithful state into a faithful normal trace. The existence of this averaging map is the remaining finite-algebra input.

theorem tracial_state_of_normal_center_average (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ) (hψ1 : ψ 1 = 1)
    (hfaith : ∀ p : M, IsStarProjection p → (∀ a : M, p * a = a * p) → ψ p = 0 → p = 0)
    (E : M →L[ℂ] M) (hEnormal : HasPreadjoint e E)
    (hEpositive : ∀ a : M, 0 ≤ a → 0 ≤ E a) (hE1 : E 1 = 1)
    (hEcentral : ∀ a b : M, E a * b = b * E a)
    (hEtracial : ∀ a b : M, E (a * b) = E (b * a))
    (hEfaithful : ∀ a : M, E (star a * a) = 0 → a = 0) :
    ∃ τ : M →ₚ[ℂ] ℂ, TraceInPredual e τ ∧ τ 1 = 1 ∧
      (∀ a b : M, τ (a * b) = τ (b * a)) ∧
      (∀ a : M, τ (star a * a) = 0 → a = 0) := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.HasPreadjoint