FreeCornerEndgame.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite Fourier test completing the free-corner estimate

Given the actual finite word-level inclusion and its Fourier compression, the two propagation errors, narrow-arc norm bound, and Hankel test imply the paper's corner-independent constant. The free-product construction of those data is not assumed to be a published theorem.

theorem OAI.KadisonSimilarity.commutator_smul_right line 26
Source documentation
Scaling the test operator scales its commutator.
```
theorem commutator_smul_right (B S : H →L[ℂ] H) (c : ℂ) :
    commutator B (c • S) = c • commutator B S := by
…
```
Mentions: OAI.KadisonSimilarity.commutator
theorem OAI.KadisonSimilarity.norm_complex_smul_endomorphism line 32
Source documentation
Scalar multiplication of a bounded operator has the expected norm.
```
theorem norm_complex_smul_endomorphism (T : H →L[ℂ] H) (c : ℂ) :
    ‖c • T‖ = ‖c‖ * ‖T‖ := norm_smul c T
```

theorem OAI.KadisonSimilarity.free_corner_bound_of_fourier_compression line 38

Source documentation

A finite Fourier compression suffices to finish the corner estimate. All assumptions describe constructed operators and their checked identities; none assumes the free-corner conclusion.

theorem free_corner_bound_of_fourier_compression
    {N : ℕ} (hN : 0 < N) (G T : H →L[ℂ] H) (B S : K →L[ℂ] K)
    (ι : HilbertCopies K N →L[ℂ] H)
    (toeplitz : Matrix (Fin N) (Fin N) ℝ)
    {u ε c₀ : ℝ} (hu : 0 < u) (hε : 0 ≤ ε) (hc₀ : 0 ≤ c₀)
    (hι : ‖ι‖ ≤ 1) (hT : ‖T‖ ≤ 3 * u)
    (hG : ‖commutator G T‖ ≤ ε * ‖T‖)
    (hR : ‖G.comp ι - ι.comp (amplify B N)‖ ≤ 2 * c₀ * ε)
    (hR' : ‖G.adjoint.comp ι - ι.comp (amplify B N).adjoint‖ ≤ 2 * c₀ * ε)
    (hfourier : ι.adjoint.comp (T.comp ι) =
      (u : ℂ) • matrixOperator (fun i j =>
        (toeplitz i j : ℂ) • ContinuousLinearMap.id ℂ K +
…

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

theorem OAI.KadisonSimilarity.free_corner_bound_of_word_levels line 84

Source documentation

The word-level hypotheses of propagation imply the complete finite Fourier endgame, including both full-codomain errors.

theorem free_corner_bound_of_word_levels
    {N : ℕ} (hN : 0 < N) (G T : H →L[ℂ] H) (B S : K →L[ℂ] K)
    (U : Fin N → K →L[ℂ] H) (L : Fin N → Submodule ℂ H)
    (hUnorm : ∀ i, ‖U i‖ ≤ 1) (hUlevel : ∀ i x, U i x ∈ L i)
    (horth : ∀ i j, i ≠ j → ∀ x ∈ L i, ∀ y ∈ L j, inner ℂ x y = 0)
    (hGlevel : ∀ i x, x ∈ L i → G x ∈ L i)
    (hGstarlevel : ∀ i x, x ∈ L i → G.adjoint x ∈ L i)
    (toeplitz : Matrix (Fin N) (Fin N) ℝ)
    {u ε c₀ : ℝ} (hu : 0 < u) (hε : 0 ≤ ε) (hc₀ : 0 ≤ c₀)
    (hT : ‖T‖ ≤ 3 * u) (hG : ‖commutator G T‖ ≤ ε * ‖T‖)
    (herr : ∀ i, ‖G.comp (U i) - (U i).comp B‖ ≤ 2 * c₀ * ε)
    (herr' : ∀ i, ‖G.adjoint.comp (U i) - (U i).comp B.adjoint‖ ≤ 2 * c₀ * ε)
…

Mentions: OAI.KadisonSimilarity.commutator