CompleteAmplification.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The uniform completely bounded derivation estimate for II₁ factors

theorem OAI.KadisonKastler.hilbertMatrix_map_innerDerivation line 27

Source documentation

The entrywise derivation acts as commutation with the diagonal operator.

theorem hilbertMatrix_map_innerDerivation {ι : Type*} [Fintype ι] [DecidableEq ι]
    (h : H →L[ℂ] H) (X : CStarMatrix ι ι (Algebra M)) :
    hilbertMatrix (CStarMatrix.mapₗ
      ((innerDerivation h).comp M.toStarSubalgebra.subtype.toLinearMap) X) =
      hilbertMatrix (diagonalAmplification h) * matrixOperatorHom M X -
        matrixOperatorHom M X * hilbertMatrix (diagonalAmplification h) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.innerDerivation, OAI.KadisonKastler.diagonalAmplification, OAI.KadisonKastler.matrixOperatorHom

def OAI.KadisonKastler.concreteDerivation line 54
Source documentation
The bounded derivation on the original represented algebra.
```
def concreteDerivation (M : VonNeumannAlgebra H) (h : H →L[ℂ] H) :
    Algebra M →L[ℂ] (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.concreteDerivation_apply line 65
theorem OAI.KadisonKastler.matrix_derivation_bound_of_represented_bound line 70
Source documentation
Transfer a bound on the represented matrix algebra to the abstract entrywise matrix derivation.
```
theorem matrix_derivation_bound_of_represented_bound {n : ℕ}
    (h : H →L[ℂ] H) {c : ℝ}
    (hbound : ∀ a : Algebra (matrixVonNeumann (ι := Fin n) M),
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.finiteFactor_completelyBounded_derivation line 92
Source documentation
The manuscript's uniform amplification theorem, with constant 600. The only assumptions beyond the represented factor are the cited published cyclic similarity, Fock representation, ultrapower, and independence inputs.
```
theorem finiteFactor_completelyBounded_derivation
    (hpub : PublishedTracialUltrapower.{u})
    (hmat : PublishedFiniteMatrixUltraproduct)
    (hind : PublishedPopaFiniteBaseIndependence.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hCyclic : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct, OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.finiteFactor_uniform_amplification line 112
Source documentation
Uniform amplification in terms of the ordinary operator norm of the restricted derivation, as in Theorem 3.1 of the manuscript.
```
theorem finiteFactor_uniform_amplification
    (hpub : PublishedTracialUltrapower.{u})
    (hmat : PublishedFiniteMatrixUltraproduct)
    (hind : PublishedPopaFiniteBaseIndependence.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hCyclic : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct, OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra