TracialArcCompression.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite Fourier matrix with the actual base compression and actual trace-pairing expectations. Only scalar moments of the arc remain as data.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.arc_compression_of_scalar_moments line 22

Source documentation

Scalar Fourier moments and the expectation range on the tested word algebra determine the finite operator matrix on the actual tracial base.

theorem arc_compression_of_scalar_moments
    (E : TracialExpectation G.trace A) {C S : StarSubalgebra ℂ P}
    (EC : TracialExpectation G.trace C) (hCS : C ≤ S)
    (hf : Function.Injective G.vector) (hτ : G.trace 1 = 1)
    (w d : Pˣ) (hw : star w = w⁻¹) (hd : d * w = w⁻¹ * d)
    (hsA : (↑(w⁻¹ * d) : P) ∈ A) (hsC : (↑(w⁻¹ * d) : P) ∈ C)
    (hs0 : G.trace (↑(w⁻¹ * d) : P) = 0)
    (hs2 : (↑(w⁻¹ * d) : P) * (↑(w⁻¹ * d) : P) = 1)
    (hspan : ∀ x, x ∈ S → ∃ α β : ℂ,
      E.map x = α • (1 : P) + β • (↑(w⁻¹ * d) : P))
    (hpower : ∀ j : ℤ, (↑(w ^ j) : P) ∈ C)
    (e f h : P) (hestar : star e = e) (heh : e * h = h) (hhe : h * e = h)
…

Mentions: OAI.KadisonSimilarity.TracialExpectation