TracialCompression.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Dense tracial vectors determine the word-level operator compression. In particular the matrix-entry identity is proved from the trace and the two-sided expectation identity, rather than supplied as an operator hypothesis.

theorem OAI.KadisonSimilarity.operator_eq_of_dense_coefficients line 20

Source documentation

Matrix coefficients on any dense family determine a bounded operator.

theorem operator_eq_of_dense_coefficients {ι : Type*} (v : ι → K)
    (hv : DenseRange v) (A B : K →L[ℂ] K)
    (h : ∀ i j, inner ℂ (v i) (A (v j)) = inner ℂ (v i) (B (v j))) : A = B := by
…

theorem OAI.KadisonSimilarity.star_unitary_zpow line 36
Source documentation
Star reverses the exponent of a unitary, in the units convention used in the dihedral word calculation.
```
theorem star_unitary_zpow (w : Rˣ) (hw : star w = w⁻¹) (j : ℤ) :
    star ((↑(w ^ j) : R)) = (↑(w ^ (-j)) : R) := by
…
```

theorem OAI.KadisonSimilarity.tracial_corner_word line 42

Source documentation

Removing the supporting corner in a tracial word leaves precisely the two Fourier powers around the test operator.

theorem tracial_corner_word (w : Rˣ) (hw : star w = w⁻¹)
    (e h a b : R) (he : star e = e) (heh : e * h = h) (hhe : h * e = h)
    (j k : ℤ) :
    star (e * (↑(w ^ (-j)) : R) * a) *
        (h * (e * (↑(w ^ (-k)) : R) * b)) =
      star a * ((↑(w ^ j) : R) * h * (↑(w ^ (-k)) : R)) * b := by
…

theorem OAI.KadisonSimilarity.tracial_expectation_test line 58

Source documentation

A trace-preserving bimodule projection preserves all matrix coefficients against its range algebra.

theorem tracial_expectation_test (A : StarSubalgebra ℂ R)
    (τ : R →ₗ[ℂ] ℂ) (E : R →ₗ[ℂ] R)
    (htrace : ∀ x, τ (E x) = τ x)
    (hbimod : ∀ (a b : A) x, E ((a : R) * x * (b : R)) =
      (a : R) * E x * (b : R)) (a b : A) (x : R) :
    τ (star (a : R) * x * (b : R)) = τ (star (a : R) * E x * (b : R)) := by
…

theorem OAI.KadisonSimilarity.tracial_word_compression_entry line 73

Source documentation

Word-level compression computed from dense tracial vectors. ρ is the compression of the left action to the base Hilbert space; it need only be linear on the full algebra.

theorem tracial_word_compression_entry
    (A : StarSubalgebra ℂ R) (τ : R →ₗ[ℂ] ℂ)
    (V : R →ₗ[ℂ] H) (L : R →ₗ[ℂ] (H →L[ℂ] H))
    (hinner : ∀ a b, inner ℂ (V a) (V b) = τ (star a * b))
    (hleft : ∀ a b, L a (V b) = V (a * b))
    (v : A → K) (hv : DenseRange v) (ρ : R →ₗ[ℂ] (K →L[ℂ] K))
    (hρ : ∀ (a b : A) x,
      inner ℂ (v a) (ρ x (v b)) = τ (star (a : R) * x * (b : R)))
    (E : R →ₗ[ℂ] R)
    (htrace : ∀ x, τ (E x) = τ x)
    (hbimod : ∀ (a b : A) x, E ((a : R) * x * (b : R)) =
      (a : R) * E x * (b : R))
…

theorem OAI.KadisonSimilarity.finite_dihedral_compression line 107

Source documentation

Once the algebraic entry calculation is known, linearity and the exact corner normalization give the whole finite Toeplitz-plus-Hankel matrix.

theorem finite_dihedral_compression
    {N : ℕ} (U : Fin N → K →L[ℂ] H) (T : H →L[ℂ] H)
    (ρ : R →ₗ[ℂ] (K →L[ℂ] K)) (hρone : ρ 1 = ContinuousLinearMap.id ℂ K)
    (s : R) (γ : ℤ → ℂ) (t : ℂ) (ht : t ≠ 0)
    (hentry : ∀ i j,
      (U i).adjoint.comp (T.comp (U j)) =
        t⁻¹ • ρ (((2 * t) ^ 2 / 2) •
          (γ ((i : ℕ) - (j : ℤ)) • (1 : R) +
            γ ((i : ℕ) + (j : ℤ) + 1) • s))) :
    (sumColumns U).adjoint.comp (T.comp (sumColumns U)) =
      (2 * t) • matrixOperator (fun i j =>
        γ ((i : ℕ) - (j : ℤ)) • ContinuousLinearMap.id ℂ K +
…

Mentions: OAI.KadisonSimilarity.sumColumns, OAI.KadisonSimilarity.matrixOperator