ArcCompression.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite narrow-arc compression, assembled from the trace calculation, the dihedral expectation, and the actual Fourier integral.

theorem OAI.KadisonSimilarity.narrow_arc_tracial_compression line 18

Source documentation

The finite operator matrix identity used by the Hankel test. Every entry comes from tracial vectors and the two expectation identities.

theorem narrow_arc_tracial_compression
    {N : ℕ} (hN : 0 < N)
    (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)))
    (hρone : ρ 1 = ContinuousLinearMap.id ℂ K)
    (E₀ EC : R →ₗ[ℂ] R)
    (htrace : ∀ x, τ (E₀ x) = τ x)
…