SquareArrayPadding.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Zero padding of Hilbert arrays

The coordinate inclusion along an arbitrary finite injection is isometric. Extension of an operator by zero consequently preserves scalar commutator norms and the norms of their matrix amplifications. No dimension factor occurs.

def OAI.KadisonSimilarity.copyEmbeddingMap line 22
Source documentation
The actual zero extension along an injection of finite coordinate sets.
```
def copyEmbeddingMap (e : Fin r ↪ Fin m) :
    HilbertCopies H r →L[ℂ] HilbertCopies H m :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.copyEmbeddingMap_apply_image line 26
theorem OAI.KadisonSimilarity.copyEmbeddingMap_apply_of_not_mem line 30
theorem OAI.KadisonSimilarity.norm_copyEmbeddingMap line 38
def OAI.KadisonSimilarity.copyEmbedding line 58
Source documentation
Zero extension, now bundled as a linear isometry.
```
def copyEmbedding (e : Fin r ↪ Fin m) :
    HilbertCopies H r →ₗᵢ[ℂ] HilbertCopies H m where
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.copyEmbedding_toContinuousLinearMap line 63
theorem OAI.KadisonSimilarity.norm_copyEmbeddingMap_le line 66
def OAI.KadisonSimilarity.copyRestriction line 73
Source documentation
Restriction to the coordinates in the image of the injection.
```
def copyRestriction (e : Fin r ↪ Fin m) :
    HilbertCopies H m →L[ℂ] HilbertCopies H r :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.copyRestriction_apply line 78
theorem OAI.KadisonSimilarity.norm_copyRestriction_le line 82
theorem OAI.KadisonSimilarity.copyRestriction_copyEmbedding line 98
theorem OAI.KadisonSimilarity.copyEmbeddingMap_amplify line 104
theorem OAI.KadisonSimilarity.copyRestriction_amplify line 113

theorem OAI.KadisonSimilarity.norm_split_extension line 129

Source documentation

Extension by zero along an isometric, contractively split inclusion has exactly the original operator norm.

theorem norm_split_extension (J : E →L[ℂ] F) (R : F →L[ℂ] E)
    (hJ : ‖J‖ ≤ 1) (hR : ‖R‖ ≤ 1)
    (hRJ : R.comp J = ContinuousLinearMap.id ℂ E) (T : E →L[ℂ] E) :
    ‖J.comp (T.comp R)‖ = ‖T‖ := by
…

theorem OAI.KadisonSimilarity.commutator_split_extension line 154
def OAI.KadisonSimilarity.padArrayOperator line 173
Source documentation
An operator on the smaller array, extended by zero on all new coordinates.
```
def padArrayOperator (e : Fin r ↪ Fin m)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r) :
    HilbertCopies H m →L[ℂ] HilbertCopies H m :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.norm_padArrayOperator line 178
theorem OAI.KadisonSimilarity.commutator_padArrayOperator line 189
Source documentation
Common left multiplication commutes with extending the multiplicity space.
```
theorem commutator_padArrayOperator (e : Fin r ↪ Fin m)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r) (T : H →L[ℂ] H) :
    commutator (padArrayOperator e Y) (amplify T m) =
      padArrayOperator e (commutator Y (amplify T r)) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.amplify
theorem OAI.KadisonSimilarity.norm_commutator_padArrayOperator line 197
Source documentation
Every scalar commutator norm is unchanged by multiplicity padding.
```
theorem norm_commutator_padArrayOperator (e : Fin r ↪ Fin m)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r) (T : H →L[ℂ] H) :
    ‖commutator (padArrayOperator e Y) (amplify T m)‖ =
      ‖commutator Y (amplify T r)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.scalar_bound_padArrayOperator_iff line 205

Source documentation

In particular, each prescribed homogeneous scalar bound transfers with the same constant, in both directions.

theorem scalar_bound_padArrayOperator_iff {A : Type*} [Norm A]
    (σ : A → (H →L[ℂ] H)) (e : Fin r ↪ Fin m)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r) (ε : ℝ) :
    (∀ a, ‖commutator (padArrayOperator e Y) (amplify (σ a) m)‖ ≤ ε * ‖a‖) ↔
      (∀ a, ‖commutator Y (amplify (σ a) r)‖ ≤ ε * ‖a‖) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.amplify

def OAI.KadisonSimilarity.initialCopyEmbedding line 214
Source documentation
The natural initial-coordinate inclusion is a special case of arbitrary coordinate padding.
```
def initialCopyEmbedding (hrm : r ≤ m) :
    HilbertCopies H r →ₗᵢ[ℂ] HilbertCopies H m :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.mapCopies_comp_eq line 225
theorem OAI.KadisonSimilarity.mapCopies_id_eq line 234
theorem OAI.KadisonSimilarity.amplify_padArrayOperator line 240

theorem OAI.KadisonSimilarity.norm_matrix_commutator_padArrayOperator line 249

Source documentation

Multiplicity padding preserves the norm of every matrix commutator.

theorem norm_matrix_commutator_padArrayOperator (e : Fin r ↪ Fin m)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r) {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    ‖commutator (amplify (padArrayOperator e Y) n)
      (matrixOperator (fun i j => amplify (X i j) m))‖ =
    ‖commutator (amplify Y n)
      (matrixOperator (fun i j => amplify (X i j) r))‖ := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.matrixOperator

def OAI.KadisonSimilarity.padOperatorMatrix line 284

Source documentation

Entrywise zero extension of a square operator matrix.

def padOperatorMatrix (e : Fin r ↪ Fin m)
    (X : Matrix (Fin r) (Fin r) (H →L[ℂ] H)) :
    Matrix (Fin m) (Fin m) (H →L[ℂ] H) :=
…

theorem OAI.KadisonSimilarity.padOperatorMatrix_apply_image line 290
theorem OAI.KadisonSimilarity.padOperatorMatrix_apply_of_not_mem_left line 295
theorem OAI.KadisonSimilarity.padOperatorMatrix_apply_of_not_mem_right line 301
theorem OAI.KadisonSimilarity.sum_eq_sum_embedding line 307
theorem OAI.KadisonSimilarity.matrixOperator_padOperatorMatrix line 322
Source documentation
Entrywise matrix padding realizes precisely extension by zero.
```
theorem matrixOperator_padOperatorMatrix (e : Fin r ↪ Fin m)
    (X : Matrix (Fin r) (Fin r) (H →L[ℂ] H)) :
    matrixOperator (padOperatorMatrix e X) = padArrayOperator e (matrixOperator X) := by
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.padOperatorMatrix, OAI.KadisonSimilarity.padArrayOperator
theorem OAI.KadisonSimilarity.norm_matrixOperator_padOperatorMatrix line 341
Source documentation
Square-matrix padding preserves the concrete operator norm.
```
theorem norm_matrixOperator_padOperatorMatrix (e : Fin r ↪ Fin m)
    (X : Matrix (Fin r) (Fin r) (H →L[ℂ] H)) :
    ‖matrixOperator (padOperatorMatrix e X)‖ = ‖matrixOperator X‖ := by
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.padOperatorMatrix
theorem OAI.KadisonSimilarity.norm_commutator_padOperatorMatrix line 347
Source documentation
Enlarging the matrix size introduces no loss in a commutator norm.
```
theorem norm_commutator_padOperatorMatrix (e : Fin r ↪ Fin m)
    (Y : H →L[ℂ] H) (X : Matrix (Fin r) (Fin r) (H →L[ℂ] H)) :
    ‖commutator (amplify Y m) (matrixOperator (padOperatorMatrix e X))‖ =
      ‖commutator (amplify Y r) (matrixOperator X)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.padOperatorMatrix

theorem OAI.KadisonSimilarity.norm_commutator_pad_both line 364

Source documentation

Padding the multiplicity and the testing matrix can be performed independently, preserving the complete commutator test exactly.

theorem norm_commutator_pad_both {s t : ℕ}
    (e : Fin r ↪ Fin m) (f : Fin s ↪ Fin t)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r)
    (X : Matrix (Fin s) (Fin s) (H →L[ℂ] H)) :
    ‖commutator (amplify (padArrayOperator e Y) t)
      (matrixOperator (padOperatorMatrix f (fun i j => amplify (X i j) m)))‖ =
    ‖commutator (amplify Y s)
      (matrixOperator (fun i j => amplify (X i j) r))‖ := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.padOperatorMatrix

theorem OAI.KadisonSimilarity.norm_commutator_le_square_padding line 378

Source documentation

The inequality used to fit an arbitrary finite test into a common square array, including the case of zero-size original arrays.

theorem norm_commutator_le_square_padding {s t : ℕ}
    (hrm : r ≤ m) (hst : s ≤ t)
    (Y : HilbertCopies H r →L[ℂ] HilbertCopies H r)
    (X : Matrix (Fin s) (Fin s) (H →L[ℂ] H)) :
    ‖commutator (amplify Y s)
      (matrixOperator (fun i j => amplify (X i j) r))‖ ≤
    ‖commutator (amplify (padArrayOperator (Fin.castLEEmb hrm) Y) t)
      (matrixOperator (padOperatorMatrix (Fin.castLEEmb hst)
        (fun i j => amplify (X i j) m)))‖ :=
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.padArrayOperator, OAI.KadisonSimilarity.padOperatorMatrix