FiniteTracialDecomposition.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Unconditional scalar traces on finite central pieces

Trace-free normal states, orbit compactness, and the isometric fixed-point argument discharge the local tracial-cut input to central decomposition.

theorem OAI.BoundedHochschild.KadisonRingrose.faithful_normal_trace_of_center_state line 29

Source documentation

A center-faithful normal state on a finite von Neumann algebra gives an actual faithful normal tracial state.

theorem faithful_normal_trace_of_center_state (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (hψ1 : ψ 1 = 1)
    (hfaith : ∀ p : M, IsStarProjection p → (∀ a : M, p * a = a * p) → ψ p = 0 → p = 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.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual

theorem OAI.BoundedHochschild.KadisonRingrose.localTracialCutInput line 44
Source documentation
The local scalar-trace input is now a theorem, with no averaging input.
```
theorem localTracialCutInput (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    LocalTracialCutInput M := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.LocalTracialCutInput
theorem OAI.BoundedHochschild.KadisonRingrose.centralDecompositionInput line 62
Source documentation
The central decomposition needed by the main theorem is unconditional.
```
theorem centralDecompositionInput (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    CentralDecompositionInput M :=
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.CentralDecompositionInput

theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_classical_vanishing line 67

Source documentation

Only the classical non-type-II₁ vanishing input remains here.

theorem primitive_of_classical_vanishing (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hclassical : ClassicalVanishingInput.{u})
    {n : ℕ} (f : Cochain M (n + 2)) (hf : ∀ x, differentialValue f x = 0) :
    ∃ g : Cochain M (n + 1), ∀ x, differentialValue g x = f x :=
…

Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differentialValue