CenterAveragingReduction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The precise remaining center-valued trace input

The construction of faithful normal scalar traces is reduced to the center-valued trace theorem for finite von Neumann algebras (Blackadar, III.2.5.7--8). Normal states and their central supports are constructed without this input. Only the positive normal central averaging map remains an explicit hypothesis; the global central partition is derived.

structure OAI.BoundedHochschild.KadisonRingrose.NormalCentralAverage line 29

Source documentation

The part of a center-valued trace used by the scalar trace construction.

structure NormalCentralAverage {N Y : Type u} [CStarAlgebra N]
    [PartialOrder N] [StarOrderedRing N] [NormedAddCommGroup Y]
    [NormedSpace ℂ Y] [CompleteSpace Y] (e : StrongDual ℂ Y ≃ₗᵢ⋆[ℂ] N) where
…

def OAI.BoundedHochschild.KadisonRingrose.FiniteCentralAveragingInput line 45
Source documentation
Center-valued trace existence, restricted to the finite type-II central corners needed for this application.
```
def FiniteCentralAveragingInput (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) : Prop :=
…
```
theorem OAI.BoundedHochschild.KadisonRingrose.localTracialCutInput_of_center_averaging line 52
Source documentation
A center-valued trace yields the exact local scalar-trace consequence needed by the already proved global decomposition.
```
theorem localTracialCutInput_of_center_averaging (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (haverage : FiniteCentralAveragingInput e) : LocalTracialCutInput M := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCentralAveragingInput, OAI.BoundedHochschild.KadisonRingrose.LocalTracialCutInput
theorem OAI.BoundedHochschild.KadisonRingrose.centralDecompositionInput_of_center_averaging line 72
Source documentation
All central partition and scalar-trace work is discharged; only the center-valued averaging existence input remains in the structural reduction.
```
theorem centralDecompositionInput_of_center_averaging (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (haverage : FiniteCentralAveragingInput e) : CentralDecompositionInput M :=
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCentralAveragingInput, OAI.BoundedHochschild.KadisonRingrose.CentralDecompositionInput
theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_center_averaging line 77