HankelOperator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The narrow-arc Hankel test on an arbitrary complex Hilbert space.

theorem OAI.KadisonSimilarity.norm_lower_of_orthonormal_coefficients line 17
Source documentation
A finite orthonormal compression with entries bounded below forces an operator-norm lower bound. The ambient Hilbert space may be infinite-dimensional.
```
theorem norm_lower_of_orthonormal_coefficients {N : ℕ} (hN : 0 < N)
    (T : H →L[ℂ] H) (e : Fin N → H) (he : Orthonormal ℂ e) {c : ℝ}
    (hcoeff : ∀ j k, c ≤ (inner ℂ (e j) (T (e k))).re) :
    N * c ≤ ‖T‖ := by
…
```
theorem OAI.KadisonSimilarity.norm_lower_of_arcHankelCompression line 49
Source documentation
A compression with the actual narrow-arc Fourier coefficients has a uniform lower bound, independently of the ambient space and N.
```
theorem norm_lower_of_arcHankelCompression {N : ℕ} (hN : 0 < N)
    (T : H →L[ℂ] H) (e : Fin N → H) (he : Orthonormal ℂ e)
    (hcoeff : ∀ j k, (inner ℂ (e j) (T (e k))).re = arcHankelMatrix N j k) :
    1 / Real.pi ^ 2 ≤ ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.arcHankelMatrix