CompletelyBoundedImplementation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Implementation of completely bounded rectangular derivations

def OAI.KadisonSimilarity.RectangularCompleteBound line 17
Source documentation
A uniform square-matrix bound for an operator-valued map between two spaces.
```
def RectangularCompleteBound (δ : A → (K →L[ℂ] F)) (D : ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.rectangularDiagonalStarHom line 22
Source documentation
The diagonal of the triangular representation is a star representation.
```
def rectangularDiagonalStarHom (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F))
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) : A →⋆ₐ[ℂ] (RectangularSum F K →L[ℂ] RectangularSum F K) :=
…
```
Mentions: OAI.KadisonSimilarity.RectangularSum
theorem OAI.KadisonSimilarity.rectangularDiagonalStarHom_apply line 41
theorem OAI.KadisonSimilarity.norm_rectangularInl_le_one line 46
theorem OAI.KadisonSimilarity.norm_rectangularSnd_le_one line 53
theorem OAI.KadisonSimilarity.matrixOperator_offDiagonal line 60
Source documentation
The off-diagonal square matrix is an isometric-coordinate compression.
```
theorem matrixOperator_offDiagonal {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (K →L[ℂ] F)) :
    matrixOperator (fun i j => (rectangularInl (F := F) (K := K)).comp ((X i j).comp (WithLp.sndL 2 ℂ F K))) =
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.rectangularInl
theorem OAI.KadisonSimilarity.norm_comp_contracts line 82
theorem OAI.KadisonSimilarity.norm_matrixOperator_offDiagonal_le line 100
Source documentation
The norm of the amplified off-diagonal block does not exceed that of the original rectangular matrix.
```
theorem norm_matrixOperator_offDiagonal_le {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (K →L[ℂ] F)) :
    ‖matrixOperator (fun i j => (rectangularInl (F := F) (K := K)).comp ((X i j).comp (WithLp.sndL 2 ℂ F K)))‖ ≤
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.rectangularInl

theorem OAI.KadisonSimilarity.completeBound_rectangularRepresentation line 116

Source documentation

A rectangular complete bound controls the complete norm of its triangular representation by one plus that bound.

theorem completeBound_rectangularRepresentation
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    {D : ℝ} (hD : RectangularCompleteBound δ D) :
    CompleteBound (rectangularRepresentation ρ σ δ hδ).1 (1 + D) := by
…

Mentions: OAI.KadisonSimilarity.RectangularCompleteBound, OAI.KadisonSimilarity.CompleteBound, OAI.KadisonSimilarity.rectangularRepresentation

theorem OAI.KadisonSimilarity.rectangularCompleteBound_normalized line 152
Source documentation
Rescaling a rectangular derivation rescales all of its matrix bounds.
```
theorem rectangularCompleteBound_normalized
    (δ : A →L[ℂ] (K →L[ℂ] F)) {D : ℝ} (hD : RectangularCompleteBound δ D) :
    RectangularCompleteBound (normalizedRectangularDerivation δ) (D * ‖δ‖⁻¹) := by
…
```
Mentions: OAI.KadisonSimilarity.RectangularCompleteBound, OAI.KadisonSimilarity.normalizedRectangularDerivation

theorem OAI.KadisonSimilarity.rectangular_inner_of_completeBound line 174

Source documentation

The manuscript's completely bounded implementation lemma, using only the explicit Paulsen input. The projection argument actually bounds the implementer by the first power of the condition number, hence implies the stated square.

theorem rectangular_inner_of_completeBound
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    {D : ℝ} (hD0 : 0 ≤ D) (hD : RectangularCompleteBound δ D)
    (paulsen : PaulsenSimilarityInput (normalizedRectangularRepresentation ρ σ δ hδ)) :
    ∃ V : K →L[ℂ] F, (∀ a, δ a = V.comp (σ a) - (ρ a).comp V) ∧
      ‖V‖ ≤ ‖δ‖ * (1 + D * ‖δ‖⁻¹) ^ 2 := by
…

Mentions: OAI.KadisonSimilarity.RectangularCompleteBound, OAI.KadisonSimilarity.PaulsenSimilarityInput, OAI.KadisonSimilarity.normalizedRectangularRepresentation

theorem OAI.KadisonSimilarity.cyclic_derivation_implementation line 223

Source documentation

The cyclic implementation constant, conditional on Dickson, Paulsen, and cyclic-column approximation.

theorem cyclic_derivation_implementation
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    (dickson : DicksonTwoBound (A := A) (RectangularSum F K))
…

Mentions: OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum