HankelBounds.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The finite Hankel test in the similarity manuscript

The coefficients here are the actual Fourier coefficients of the narrow-arc function in Section hankel: sin (l θ) / (π l), with θ = 1/(2N). The lower bound uses the constant vector in the first N coordinates. No assertion about the free-product construction is assumed here.

def OAI.KadisonSimilarity.arcWidth line 24
Source documentation
The angular half-width used in the manuscript.
```
def arcWidth (N : ℕ) : ℝ := 1 / (2 * N)
```
def OAI.KadisonSimilarity.arcCoefficient line 27
Source documentation
A positive Fourier coefficient of the centered narrow-arc indicator.
```
def arcCoefficient (N l : ℕ) : ℝ :=
…
```
theorem OAI.KadisonSimilarity.arcWidth_pos line 30
theorem OAI.KadisonSimilarity.arcCoefficient_lower line 34
def OAI.KadisonSimilarity.arcHankelMatrix line 58
Source documentation
The actual N × N Hankel block tested in the manuscript.
```
def arcHankelMatrix (N : ℕ) : Matrix (Fin N) (Fin N) ℝ :=
…
```
theorem OAI.KadisonSimilarity.arcHankelMatrix_entry_lower line 61

def OAI.KadisonSimilarity.realMatrixOperator line 70

Source documentation

A finite real matrix, acting with its Hilbert-space operator norm.

def realMatrixOperator {N : ℕ} (M : Matrix (Fin N) (Fin N) ℝ) :
    EuclideanSpace ℝ (Fin N) →L[ℝ] EuclideanSpace ℝ (Fin N) :=
…

theorem OAI.KadisonSimilarity.realMatrixOperator_norm_lower line 76
Source documentation
Testing on the constant vector turns a pointwise lower bound into an operator-norm lower bound. This avoids assuming the desired Hankel estimate.
```
theorem realMatrixOperator_norm_lower {N : ℕ} (hN : 0 < N)
    (M : Matrix (Fin N) (Fin N) ℝ) {c : ℝ} (hc : 0 ≤ c)
    (hM : ∀ j k, c ≤ M j k) :
    N * c ≤ ‖realMatrixOperator M‖ := by
…
```
Mentions: OAI.KadisonSimilarity.realMatrixOperator
theorem OAI.KadisonSimilarity.arcHankelMatrix_norm_lower line 111
Source documentation
The finite Hankel block has the stronger lower bound 1/π².
```
theorem arcHankelMatrix_norm_lower {N : ℕ} (hN : 0 < N) :
    1 / Real.pi ^ 2 ≤ ‖realMatrixOperator (arcHankelMatrix N)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.realMatrixOperator, OAI.KadisonSimilarity.arcHankelMatrix
theorem OAI.KadisonSimilarity.arcHankelMatrix_norm_lower_paper line 123
Source documentation
The weaker lower bound used for the published numerical constant.
```
theorem arcHankelMatrix_norm_lower_paper {N : ℕ} (hN : 0 < N) :
    1 / (2 * Real.pi ^ 2) ≤ ‖realMatrixOperator (arcHankelMatrix N)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.realMatrixOperator, OAI.KadisonSimilarity.arcHankelMatrix

theorem OAI.KadisonSimilarity.cancel_corner_trace line 133

Source documentation

Cancellation of the nonzero corner trace in the final Hankel estimate.

theorem cancel_corner_trace {u x c₀ ε : ℝ} (hu : 0 < u)
    (h : u / (2 * Real.pi ^ 2) * x ≤ 3 * u * (1 + 4 * c₀) * ε) :
    x ≤ 6 * Real.pi ^ 2 * (1 + 4 * c₀) * ε := by
…