CentralDecomposition.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Central decomposition and the uniform separable estimate

The direct-integral input records only representatives of decomposable operators, their almost-everywhere algebra operations, the scalar and matrix norm formulas, and countably many dense contraction sections. These are the specializations of Blackadar, III.1.6.1–4 and III.5.1.10–15 used here (with Kaplansky density, I.9.1.3, for the contraction tests). Representatives need satisfy algebraic identities only almost everywhere for each fixed pair.

The scalar fiber bounds, their common conull set, the factor estimates, and the final perturbation estimate are proved below.

theorem OAI.KadisonSimilarity.le_center_commutant line 29
Source documentation
Every element of the algebra commutes with its center.
```
theorem le_center_commutant (P : VonNeumannAlgebra H) :
    P.toStarSubalgebra ≤ (vonNeumannCenter P).commutant.toStarSubalgebra := by
…
```
Mentions: OAI.KadisonSimilarity.vonNeumannCenter
def OAI.KadisonSimilarity.centerCommutantInclusion line 37
Source documentation
The original algebra as a subalgebra of the decomposable operators.
```
def centerCommutantInclusion (P : VonNeumannAlgebra H) :
    P.toStarSubalgebra →⋆ₐ[ℂ] (vonNeumannCenter P).commutant.toStarSubalgebra :=
…
```
Mentions: OAI.KadisonSimilarity.vonNeumannCenter
structure OAI.KadisonSimilarity.CentralDecompositionData line 47
Source documentation
The exact direct-integral identities needed for one separable algebra. No commutator estimate is a field of this structure.
```
structure CentralDecompositionData (P : VonNeumannAlgebra H) where
…
```
theorem OAI.KadisonSimilarity.CentralDecompositionData.map_commutator line 71
Source documentation
Fiber representatives preserve each fixed commutator almost everywhere.
```
theorem CentralDecompositionData.map_commutator
    (D : CentralDecompositionData μ K P)
    (x y : (vonNeumannCenter P).commutant.toStarSubalgebra) :
    ∀ᵐ a ∂μ, D.fiber (commutator x y) a =
      commutator (D.fiber x a) (D.fiber y a) := by
…
```
Mentions: OAI.KadisonSimilarity.CentralDecompositionData, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.CentralDecompositionData.scalar_bound line 81

Source documentation

The countable sections give one conull set with the full scalar bound.

theorem CentralDecompositionData.scalar_bound
    (D : CentralDecompositionData μ K P)
    (Y : (vonNeumannCenter P).commutant.toStarSubalgebra)
    {c : ℝ} (hc : 0 ≤ c)
    (hbound : scalarCommutatorNorm P (Y : H →L[ℂ] H) ≤ c) :
    ∀ᵐ a ∂μ, scalarCommutatorNorm (D.algebra a) (D.fiber Y a) ≤ c := by
…

Mentions: OAI.KadisonSimilarity.CentralDecompositionData, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.scalarCommutatorNorm

theorem OAI.KadisonSimilarity.CentralDecompositionData.matrix_bound line 106
Source documentation
A decomposable operator on the separable direct-integral fibers inherits the uniform factor bound.
```
theorem CentralDecompositionData.matrix_bound
    (D : CentralDecompositionData μ K P)
    (cases : ∀ᵐ a ∂μ, PublishedFactorCasesInput (D.algebra a))
    (dickson : ∀ᵐ a ∂μ, DicksonTwoBound (A := D.algebra a) (RectangularSum (K a) (K a)))
…
```
Mentions: OAI.KadisonSimilarity.CentralDecompositionData, OAI.KadisonSimilarity.PublishedFactorCasesInput, OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum
theorem OAI.KadisonSimilarity.commutatorEstimate_of_centralDecomposition line 151
Source documentation
Central averaging followed by the factor estimates proves the manuscript's constant on this represented algebra.
```
theorem commutatorEstimate_of_centralDecomposition
    (D : CentralDecompositionData μ K P)
    (approximation : SpectralStepApproximation (vonNeumannCenter P))
    (cases : ∀ᵐ a ∂μ, PublishedFactorCasesInput (D.algebra a))
    (dickson : ∀ᵐ a ∂μ, DicksonTwoBound (A := D.algebra a) (RectangularSum (K a) (K a))) :
…
```
Mentions: OAI.KadisonSimilarity.CentralDecompositionData, OAI.KadisonSimilarity.SpectralStepApproximation, OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.PublishedFactorCasesInput, OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum