ControlledCommutator.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Free Haar representatives with the scalar commutator bound

The finite-matrix representatives constructed by the two independence applications retain the dimension-free 2δ commutator estimate in the original normal representation.

theorem OAI.KadisonKastler.finiteMatrixEmbedding_operator line 35
theorem OAI.KadisonKastler.finiteMatrixEmbedding_commutator_le line 50
Source documentation
The estimate is in the operator norm on the actual amplified Hilbert space, not merely in the quotient.
```
theorem finiteMatrixEmbedding_commutator_le
    (E : Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
    (h : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hb : ∀ a ∈ M, ‖h * a - a * h‖ ≤ δ * ‖a‖)
    (v : unitary (FiniteMatrixModel n j)) :
    let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification
def OAI.KadisonKastler.finiteModelUnitaryLift line 73
Source documentation
The actual bounded sequence of finite-matrix representatives.
```
def finiteModelUnitaryLift
    (E : ∀ j, Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
    (v : unitary (VaryingBoundedSequence (FiniteMatrixModel n))) :
    unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))) :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.finiteModelUnitaryLift_commutator line 80
theorem OAI.KadisonKastler.exists_image_models line 92
theorem OAI.KadisonKastler.exists_freeHaar_commutator_lift_of_models line 102
Source documentation
The coordinate norm estimates can be attached to the free model before choosing a concrete representation for its quotient.
```
theorem exists_freeHaar_commutator_lift_of_models
    (τ : FaithfulTracialState (Algebra M))
    (R : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω)
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace

theorem OAI.KadisonKastler.exists_freeHaar_commutator_lift line 123

Source documentation

The free unitary and all its coordinate 2δ bounds, with exactly the three published structural hypotheses of the two-stage construction.

theorem exists_freeHaar_commutator_lift
    (hpub : PublishedTracialUltrapower.{u})
    (hmat : PublishedFiniteMatrixUltraproduct)
    (hind : PublishedPopaFiniteBaseIndependence.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ Filter.atTop)
    (h : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hb : ∀ a ∈ M, ‖h * a - a * h‖ ≤ δ * ‖a‖) :
    ∃ P : TracialUltrapower (matrixVonNeumannTrace (ι := Fin n) M (concreteFactorTrace hM)) ω,
…

Mentions: OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct, OAI.Generator.IsII1Factor, OAI.KadisonKastler.TracialUltrapower, OAI.KadisonKastler.matrixVonNeumannTrace, OAI.KadisonKastler.concreteFactorTrace