TracialFreeCornerTheorem.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The tracial free-corner argument assembled from the actual word model, matrix symmetrization, and spectral test. All propagation, Fourier-matrix, operator-norm, and averaging conclusions are derived from the local inputs. Only the underlying local model and the specified published inputs remain.

theorem OAI.KadisonSimilarity.exists_arcWidth_le line 19
Source documentation
An arbitrarily small positive spectral arc is available by choosing the finite compression size.
```
theorem exists_arcWidth_le {t : ℝ} (ht : 0 < t) :
    ∃ N : ℕ, 0 < N ∧ 4 * arcWidth N ≤ 2 * t := by
…
```
Mentions: OAI.KadisonSimilarity.arcWidth

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_corner_from_local_models line 110

Source documentation

For an operator with the finite matrix symmetries, the actual spectral test and the proved propagation give the uniform free-corner bound.

theorem free_corner_from_local_models (Y : H →L[ℂ] H)
    (hYD : ∀ x : D, Y.comp (G.left (x : P)) = (G.left (x : P)).comp Y)
    (hYU : ∀ j w, Y.comp
      (G.tracialMatrixUnitaryRepresentation A D M hgen hfaithful hext j w : H →L[ℂ] H) =
      (G.tracialMatrixUnitaryRepresentation A D M hgen hfaithful hext j w : H →L[ℂ] H).comp Y)
    {ε : ℝ} (hε : 0 ≤ ε) (hcorner : G.TraceCornerBound D Y t ε) :
    ‖commutator (G.baseOperator A Y) (G.baseRepresentation A s)‖ ≤
      6 * Real.pi ^ 2 * (1 + 4 * cyclicConstant) * ε := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.cyclicConstant

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_corner_original_operator line 148
Source documentation
The original operator satisfies the free-corner estimate. The extra matrix symmetries are constructed by actual normalized Haar averaging, and its exact base compression is restored at the end.
```
theorem free_corner_original_operator (T : H →L[ℂ] H)
    (hTD : ∀ x : D, T.comp (G.left (x : P)) = (G.left (x : P)).comp T)
    {ε : ℝ} (hε : 0 ≤ ε) (hcorner : G.TraceCornerBound D T t ε) :
    ‖G.baseOperator A (commutator T (G.left (s : P)))‖ ≤
      6 * Real.pi ^ 2 * (1 + 4 * cyclicConstant) * ε := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.cyclicConstant