CompletelyBounded.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Concrete matrix norms and complete boundedness

The matrix norm used here is CStarMatrix's C-star norm. The representation on finite Hilbert sums is shown to preserve that norm, connecting the concrete commutator estimate with the usual notion of complete boundedness.

def OAI.KadisonSimilarity.operatorMatrixRepresentation line 22
Source documentation
The algebraic operator-matrix action, before changing the matrix norm.
```
def operatorMatrixRepresentation (n : ℕ) :
    Matrix (Fin n) (Fin n) (H →L[ℂ] H) →⋆ₐ[ℂ]
      (HilbertCopies H n →L[ℂ] HilbertCopies H n) where
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
def OAI.KadisonSimilarity.matrixRepresentation line 60
Source documentation
Operator matrices act as a star algebra homomorphism on the Hilbert sum.
```
def matrixRepresentation (n : ℕ) :
    CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H) →⋆ₐ[ℂ]
      (HilbertCopies H n →L[ℂ] HilbertCopies H n) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.operatorMatrixRepresentation_injective line 69
Source documentation
Every entry can be recovered by evaluating on a vector in one coordinate.
```
theorem operatorMatrixRepresentation_injective (n : ℕ) :
    Function.Injective (operatorMatrixRepresentation (H := H) n) := by
…
```
Mentions: OAI.KadisonSimilarity.operatorMatrixRepresentation
theorem OAI.KadisonSimilarity.matrixRepresentation_injective line 80
Source documentation
The normed matrix action remains injective after the type synonym is changed.
```
theorem matrixRepresentation_injective (n : ℕ) :
    Function.Injective (matrixRepresentation (H := H) n) :=
…
```
Mentions: OAI.KadisonSimilarity.matrixRepresentation
theorem OAI.KadisonSimilarity.norm_matrixOperator_eq line 85
Source documentation
The abstract C-star matrix norm equals the concrete Hilbert-space operator norm.
```
theorem norm_matrixOperator_eq (n : ℕ)
    (X : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    ‖matrixOperator (CStarMatrix.ofMatrix.symm X)‖ = ‖X‖ :=
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator
def OAI.KadisonSimilarity.CompleteBound line 97
Source documentation
A uniform bound on all square matrix amplifications, with the C-star matrix norm on the domain and the Hilbert operator norm on the codomain.
```
def CompleteBound (f : A → (H →L[ℂ] H)) (C : ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.IsCompletelyBounded line 102
Source documentation
Complete boundedness in terms of the concrete matrix norm.
```
def IsCompletelyBounded (f : A → (H →L[ℂ] H)) : Prop :=
…
```
theorem OAI.KadisonSimilarity.completeBound_starHom line 106
Source documentation
A star representation is completely contractive.
```
theorem completeBound_starHom (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) : CompleteBound σ 1 := by
…
```
Mentions: OAI.KadisonSimilarity.CompleteBound
theorem OAI.KadisonSimilarity.completeBound_inner line 118
Source documentation
Every inner derivation associated to a star representation is completely bounded, by twice the norm of its implementer.
```
theorem completeBound_inner (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (V : H →L[ℂ] H) :
    CompleteBound (fun a => commutator V (σ a)) (2 * ‖V‖) := by
…
```
Mentions: OAI.KadisonSimilarity.CompleteBound, OAI.KadisonSimilarity.commutator
theorem OAI.KadisonSimilarity.completeBound_commutator_of_estimate line 140
Source documentation
The manuscript's concrete uniform estimate bounds the complete norm of an inner derivation after any star representation into the tested algebra.
```
theorem completeBound_commutator_of_estimate (P : VonNeumannAlgebra H)
    {C : ℝ} (hC : 0 ≤ C) (estimate : CommutatorEstimate P C)
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hσ : ∀ a, σ a ∈ P) (Y : H →L[ℂ] H) :
    CompleteBound (fun a => commutator Y (σ a)) (C * scalarCommutatorNorm P Y) := by
…
```
Mentions: OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.CompleteBound, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.scalarCommutatorNorm
def OAI.KadisonSimilarity.PaulsenSimilarityInput line 162
Source documentation
The quantitative published Paulsen input, specialized to a single bounded unital homomorphism. Paulsen, Completely bounded homomorphisms of operator algebras (1984), p. 226. It is an explicit hypothesis interface.
```
def PaulsenSimilarityInput (π : BoundedUnitalHom A H) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom