HankelCommutator.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

A finite Hankel matrix detects the base commutator

The constant-coordinate compression gives the tensor-product norm lower bound needed by the paper without introducing any infinite matrix norm assumption.

def OAI.KadisonSimilarity.constantCopies line 21
Source documentation
The unnormalized constant-coordinate inclusion.
```
def constantCopies (N : ℕ) : H →L[ℂ] HilbertCopies H N :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.constantCopies_apply line 26
theorem OAI.KadisonSimilarity.constantCopies_adjoint_apply line 29
theorem OAI.KadisonSimilarity.norm_constantCopies_le line 36

theorem OAI.KadisonSimilarity.constantCopies_compression line 46

Source documentation

Compressing a scalar operator matrix to constant coordinates sums all its coefficients.

theorem constantCopies_compression (N : ℕ) (M : Matrix (Fin N) (Fin N) ℝ)
    (T : H →L[ℂ] H) :
    (constantCopies N).adjoint.comp
      ((matrixOperator (fun i j => (M i j : ℂ) • T)).comp (constantCopies N)) =
      ((∑ i : Fin N, ∑ j : Fin N, M i j : ℝ) : ℂ) • T := by
…

Mentions: OAI.KadisonSimilarity.constantCopies, OAI.KadisonSimilarity.matrixOperator

theorem OAI.KadisonSimilarity.norm_constantCopies_compression_le line 55

theorem OAI.KadisonSimilarity.norm_scalar_operator_matrix_lower line 74

Source documentation

A matrix with coefficients bounded below by c ≥ 0 detects a factor N * c of the norm of its common operator entry.

theorem norm_scalar_operator_matrix_lower {N : ℕ} (hN : 0 < N)
    (M : Matrix (Fin N) (Fin N) ℝ) (T : H →L[ℂ] H) {c : ℝ}
    (hc : 0 ≤ c) (hM : ∀ i j, c ≤ M i j) :
    N * c * ‖T‖ ≤ ‖matrixOperator (fun i j => (M i j : ℂ) • T)‖ := by
…

Mentions: OAI.KadisonSimilarity.matrixOperator

theorem OAI.KadisonSimilarity.norm_arc_operator_matrix_lower line 94
Source documentation
The actual narrow-arc matrix detects a uniform fraction of the base norm.
```
theorem norm_arc_operator_matrix_lower {N : ℕ} (hN : 0 < N) (T : H →L[ℂ] H) :
    (1 / Real.pi ^ 2) * ‖T‖ ≤
      ‖matrixOperator (fun i j => (arcHankelMatrix N i j : ℂ) • T)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.arcHankelMatrix
theorem OAI.KadisonSimilarity.commutator_scalar_id_add line 106
Source documentation
Scalar diagonal terms vanish from the commutator.
```
theorem commutator_scalar_id_add (B S : H →L[ℂ] H) (a b : ℂ) :
    commutator B (a • ContinuousLinearMap.id ℂ H + b • S) = b • commutator B S := by
…
```
Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_commutator_fourier_matrix_lower line 115

Source documentation

The Toeplitz part of the finite Fourier compression contributes no commutator; the Hankel part detects the base operator.

theorem norm_commutator_fourier_matrix_lower {N : ℕ} (hN : 0 < N)
    (B S : H →L[ℂ] H) (toeplitz : Matrix (Fin N) (Fin N) ℝ) :
    (1 / Real.pi ^ 2) * ‖commutator B S‖ ≤
      ‖commutator (amplify B N)
        (matrixOperator (fun i j => (toeplitz i j : ℂ) • ContinuousLinearMap.id ℂ H +
          (arcHankelMatrix N i j : ℂ) • S))‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.arcHankelMatrix