EndpointBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The endpoint matrix-unit estimate from a supporting projection

For the coefficient tests it suffices to move a self-adjoint supporting projection across the inner product. This gives the required dimension factor without invoking the full tracial commutation theorem.

theorem OAI.KadisonSimilarity.norm_tensorWord line 25
Source documentation
The tensor norm on elementary words is exactly the product of letter norms.
```
theorem norm_tensorWord : ∀ (n : ℕ) (x : Fin n → E),
    ‖tensorWord x‖ = ∏ i, ‖x i‖ := by
…
```
Mentions: OAI.KadisonSimilarity.tensorWord
theorem OAI.KadisonSimilarity.norm_completedTensorWord line 40
Source documentation
Completion preserves the elementary tensor norm.
```
theorem norm_completedTensorWord {n : ℕ} (x : Fin n → E) :
    ‖completedTensorWord x‖ = ∏ i, ‖x i‖ := by
…
```
Mentions: OAI.KadisonSimilarity.completedTensorWord

theorem OAI.KadisonSimilarity.norm_completedTensorWord_le_matrix_units line 46

Source documentation

The normalized matrix-unit bound multiplies over all tensor letters.

theorem norm_completedTensorWord_le_matrix_units {n : ℕ} (x : Fin n → E)
    (m : ℝ) (hm : 0 < m) (hx : ∀ i, ‖x i‖ ≤ m ^ (-(1 : ℝ) / 2)) :
    ‖completedTensorWord x‖ ≤ m ^ (-(n : ℝ) / 2) := by
…

Mentions: OAI.KadisonSimilarity.completedTensorWord

theorem OAI.KadisonSimilarity.supported_coefficient_eq line 64

Source documentation

A supporting projection transfers to the source through an intertwiner.

theorem supported_coefficient_eq
    (Y : H →L[ℂ] K) (p : H →L[ℂ] H) (q : K →L[ℂ] K)
    (hq : q.adjoint = q) (hintertwine : q.comp Y = Y.comp p)
    (a : K) (ha : q a = a) (Ω : H) :
    inner ℂ a (Y Ω) = inner ℂ a (Y (p Ω)) := by
…

theorem OAI.KadisonSimilarity.norm_supported_coefficient_le line 81

Source documentation

The norm cost depends on the two supported vectors. In the matrix-unit application each endpoint vector has norm equal to the inverse square root of the matrix dimension.

theorem norm_supported_coefficient_le
    (Y : H →L[ℂ] K) (p : H →L[ℂ] H) (q : K →L[ℂ] K)
    (hq : q.adjoint = q) (hintertwine : q.comp Y = Y.comp p)
    (a : K) (ha : q a = a) (Ω : H) :
    ‖inner ℂ a (Y Ω)‖ ≤ ‖Y‖ * (‖a‖ * ‖p Ω‖) := by
…

theorem OAI.KadisonSimilarity.matrix_unit_endpoint_bound line 95

Source documentation

Combining the supporting projection with the matrix-unit vector norms produces exactly the exponent used to eliminate long cycles.

theorem matrix_unit_endpoint_bound
    (Y : H →L[ℂ] K) (p : H →L[ℂ] H) (q : K →L[ℂ] K)
    (hq : q.adjoint = q) (hintertwine : q.comp Y = Y.comp p)
    (a : K) (ha : q a = a) (Ω : H)
    (m : ℝ) (hm : 0 < m) (k l : ℕ)
    (htest : ‖a‖ ≤ m ^ (-((l : ℝ) + 1) / 2))
    (hsource : ‖p Ω‖ ≤ m ^ (-((k : ℝ) + 1) / 2)) :
    ‖inner ℂ a (Y Ω)‖ ≤ ‖Y‖ * m ^ (-1 - ((k : ℝ) + l) / 2) := by
…