CyclicDerivations.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The cyclic-domain completely bounded estimate

Approximate cyclic column factorization and the column Leibniz identity bound every finite matrix amplification of a derivation.

def OAI.KadisonSimilarity.columnAction line 24
Source documentation
Application of an operator-valued column to a single vector.
```
def columnAction {n : ℕ} (f : A → (K →L[ℂ] F))
    (W : Matrix (Fin n) (Fin 1) A) (ζ : K) : HilbertCopies F n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.columnAction_apply line 30

theorem OAI.KadisonSimilarity.norm_columnAction_le line 37

Source documentation

A column bound controls its value on a unit vector.

theorem norm_columnAction_le {n : ℕ} {f : A → (K →L[ℂ] F)} {c : ℝ}
    (hc : ColumnBound f c) (W : Matrix (Fin n) (Fin 1) A) (ζ : K)
    (hζ : ‖ζ‖ = 1) : ‖columnAction f W ζ‖ ≤ c * ‖CStarMatrix.ofMatrix W‖ := by
…

Mentions: OAI.KadisonSimilarity.ColumnBound, OAI.KadisonSimilarity.columnAction

theorem OAI.KadisonSimilarity.rectangularDerivation_mul_column line 50

Source documentation

The exact matrix-column Leibniz identity.

theorem rectangularDerivation_mul_column
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    {n : ℕ} (X : Matrix (Fin n) (Fin n) A)
    (W : Matrix (Fin n) (Fin 1) A) (ζ : K) :
    columnAction δ (X * W) ζ =
      matrixOperator (X.map ρ) (columnAction δ W ζ) +
        rectangularMatrixOperator (X.map δ) (columnAction σ W ζ) := by
…

Mentions: OAI.KadisonSimilarity.columnAction, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.rectangularMatrixOperator

theorem OAI.KadisonSimilarity.norm_cstarMatrix_mul_column_le line 68

Source documentation

Rectangular C-star matrix multiplication is submultiplicative in the square-times-column case used below.

theorem norm_cstarMatrix_mul_column_le {n : ℕ}
    (X : Matrix (Fin n) (Fin n) A) (W : Matrix (Fin n) (Fin 1) A) :
    ‖CStarMatrix.ofMatrix (X * W)‖ ≤
      ‖CStarMatrix.ofMatrix X‖ * ‖CStarMatrix.ofMatrix W‖ := by
…

def OAI.KadisonSimilarity.ApproximateCyclicColumns line 85
Source documentation
Every unit vector in a finite Hilbert sum is a limit of bounded cyclic columns applied to one unit vector.
```
def ApproximateCyclicColumns (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) : Prop :=
…
```

theorem OAI.KadisonSimilarity.norm_derivation_on_column_le line 93

Source documentation

The column Leibniz identity gives a bound before taking an approximation limit; only the column bound and the column norm enter.

theorem norm_derivation_on_column_le
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    {c : ℝ} (hc : 0 ≤ c) (hcol : ColumnBound δ c)
    {n : ℕ} (X : Matrix (Fin n) (Fin n) A)
    (W : Matrix (Fin n) (Fin 1) A) (hW : ‖CStarMatrix.ofMatrix W‖ ≤ 2)
    (ζ : K) (hζ : ‖ζ‖ = 1) :
    ‖rectangularMatrixOperator (X.map δ) (columnAction σ W ζ)‖ ≤
      (4 * c) * ‖CStarMatrix.ofMatrix X‖ := by
…

Mentions: OAI.KadisonSimilarity.ColumnBound, OAI.KadisonSimilarity.rectangularMatrixOperator, OAI.KadisonSimilarity.columnAction

theorem OAI.KadisonSimilarity.rectangularDerivation_bound_of_approximateCyclicColumns line 131

Source documentation

Approximate cyclic column factorization upgrades the column estimate to all square matrix amplifications.

theorem rectangularDerivation_bound_of_approximateCyclicColumns
    (ρ : A →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (K →L[ℂ] F))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    {c : ℝ} (hc : 0 ≤ c) (hcol : ColumnBound δ c)
    (hcyclic : ApproximateCyclicColumns σ)
    (n : ℕ) (X : Matrix (Fin n) (Fin n) A) :
    ‖rectangularMatrixOperator (X.map δ)‖ ≤ (4 * c) * ‖CStarMatrix.ofMatrix X‖ := by
…

Mentions: OAI.KadisonSimilarity.ColumnBound, OAI.KadisonSimilarity.ApproximateCyclicColumns, OAI.KadisonSimilarity.rectangularMatrixOperator

theorem OAI.KadisonSimilarity.cyclic_derivation_matrix_bound line 148

Source documentation

The row/column estimate and approximate cyclic column factorization give a uniform matrix bound for a derivation.

theorem cyclic_derivation_matrix_bound
    (ρ : 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

theorem OAI.KadisonSimilarity.cyclic_derivation_completeBound line 165
Source documentation
A derivation between representations on the same Hilbert space is completely bounded under approximate cyclic column factorization.
```
theorem cyclic_derivation_completeBound
    (ρ σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (δ : A →L[ℂ] (K →L[ℂ] K))
    (hδ : ∀ a b, δ (a * b) = (ρ a).comp (δ b) + (δ a).comp (σ b))
    (dickson : DicksonTwoBound (A := A) (RectangularSum K K))
…
```
Mentions: OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum