FreeHaarClosure.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

The two free-projection moments under tracial approximation

Finite Laurent-polynomial moments follow from the alternating Haar moments. Cauchy--Schwarz then extends the required degree-two and degree-four identities under trace-two-norm approximation. In these degrees no uniform operator bound on the approximants is needed.

def OAI.KadisonKastler.haarLaurentSpan line 28
Source documentation
Finite Laurent polynomials in a unitary.
```
def haarLaurentSpan (v : unitary B) : Submodule ℂ B :=
…
```
def OAI.KadisonKastler.centeredHaarLaurentSpan line 32
Source documentation
Laurent polynomials with no constant Fourier term.
```
def centeredHaarLaurentSpan (v : unitary B) : Submodule ℂ B :=
…
```
theorem OAI.KadisonKastler.haarPower_mem_haarLaurentSpan line 35
theorem OAI.KadisonKastler.haarPower_mem_centeredHaarLaurentSpan line 38
theorem OAI.KadisonKastler.unitaryHaarPolynomial_mem line 42
Source documentation
The recovery polynomial stays in every star subalgebra containing its unitary.
```
theorem unitaryHaarPolynomial_mem {S : StarSubalgebra ℂ B} {v : unitary B}
    (hv : (v : B) ∈ S) (N : ℕ) : unitaryHaarPolynomial N v ∈ S := by
…
```
Mentions: OAI.KadisonKastler.unitaryHaarPolynomial
theorem OAI.KadisonKastler.isStarNormal_unitaryHaarPolynomial line 50
Source documentation
A Laurent polynomial in a unitary is normal; here only positive powers occur.
```
theorem isStarNormal_unitaryHaarPolynomial (N : ℕ) (v : unitary B) :
    IsStarNormal (unitaryHaarPolynomial N v) := by
…
```
Mentions: OAI.KadisonKastler.unitaryHaarPolynomial
def OAI.KadisonKastler.traceCenter line 64
Source documentation
Subtraction of the scalar trace is a complex-linear operation.
```
def traceCenter (τ : FaithfulTracialState B) : B →ₗ[ℂ] B :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.traceCenter_apply line 68
theorem OAI.KadisonKastler.trace_traceCenter line 72
theorem OAI.KadisonKastler.centeredHaarLaurentSpan_le line 76
theorem OAI.KadisonKastler.traceCenter_mem_centeredHaarLaurentSpan line 82
theorem OAI.KadisonKastler.FreeHaarMoments.trace_mul_haarPower line 103
theorem OAI.KadisonKastler.FreeHaarMoments.trace_four_haarPowers line 110
theorem OAI.KadisonKastler.FreeHaarMoments.trace_mul_laurent line 125
Source documentation
A centered base-algebra element is orthogonal to every Laurent polynomial.
```
theorem trace_mul_laurent (h : FreeHaarMoments τ A v) {a x : B}
    (ha : a ∈ A) (haτ : τ.toLinearMap a = 0) (hx : x ∈ haarLaurentSpan v) :
    τ.toLinearMap (a * x) = 0 := by
…
```
Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarLaurentSpan

theorem OAI.KadisonKastler.FreeHaarMoments.trace_four_laurent line 137

Source documentation

Alternating degree four, first Haar letter centered.

theorem trace_four_laurent (h : FreeHaarMoments τ A v) {a b x y : B}
    (ha : a ∈ A) (hb : b ∈ A) (haτ : τ.toLinearMap a = 0)
    (hbτ : τ.toLinearMap b = 0) (hx : x ∈ centeredHaarLaurentSpan v)
    (hy : y ∈ haarLaurentSpan v) :
    τ.toLinearMap (a * x * b * y) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.centeredHaarLaurentSpan, OAI.KadisonKastler.haarLaurentSpan

theorem OAI.KadisonKastler.traceTwoNorm_neg line 159
theorem OAI.KadisonKastler.traceTwoNorm_sub_comm line 163
theorem OAI.KadisonKastler.norm_trace_mul_le line 168
Source documentation
Cauchy--Schwarz in its product form.
```
theorem norm_trace_mul_le (τ : FaithfulTracialState B) (x y : B) :
    ‖τ.toLinearMap (x * y)‖ ≤ traceTwoNorm τ x * traceTwoNorm τ y := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.norm_trace_four_le line 172
theorem OAI.KadisonKastler.traceTwoNorm_traceCenter_le line 186
Source documentation
Centering preserves convergence in the tracial two-norm.
```
theorem traceTwoNorm_traceCenter_le (τ : FaithfulTracialState B) (x : B) :
    traceTwoNorm τ (traceCenter τ x) ≤ (1 + ‖(1 : B)‖) * traceTwoNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.traceCenter
theorem OAI.KadisonKastler.tendsto_traceCenter_in_traceTwoNorm line 200

theorem OAI.KadisonKastler.FreeHaarMoments.trace_mul_of_laurent_approx line 217

Source documentation

Degree-two moments pass to tracial two-norm limits of Laurent polynomials.

theorem trace_mul_of_laurent_approx (h : FreeHaarMoments τ A v) {a x : B}
    (ha : a ∈ A) (haτ : τ.toLinearMap a = 0) (c : ℕ → B)
    (hc : ∀ n, c n ∈ haarLaurentSpan v)
    (hlim : Tendsto (fun n => traceTwoNorm τ (c n - x)) atTop (𝓝 0)) :
    τ.toLinearMap (a * x) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarLaurentSpan, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.FreeHaarMoments.trace_mul_eq_mul_trace_of_laurent_approx line 235

Source documentation

The ordinary degree-two trace factorization for a Haar-algebra limit.

theorem trace_mul_eq_mul_trace_of_laurent_approx (h : FreeHaarMoments τ A v)
    {p x : B} (hp : p ∈ A) (c : ℕ → B) (hc : ∀ n, c n ∈ haarLaurentSpan v)
    (hlim : Tendsto (fun n => traceTwoNorm τ (c n - x)) atTop (𝓝 0)) :
    τ.toLinearMap (p * x) = τ.toLinearMap p * τ.toLinearMap x := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarLaurentSpan, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.FreeHaarMoments.trace_four_of_centered_laurent_approx line 246

Source documentation

Degree-four moments pass to tracial two-norm limits.

theorem trace_four_of_centered_laurent_approx (h : FreeHaarMoments τ A v)
    {a b x : B} (ha : a ∈ A) (hb : b ∈ A) (haτ : τ.toLinearMap a = 0)
    (hbτ : τ.toLinearMap b = 0) (c : ℕ → B)
    (hc : ∀ n, c n ∈ centeredHaarLaurentSpan v)
    (hlim : Tendsto (fun n => traceTwoNorm τ (c n - x)) atTop (𝓝 0)) :
    τ.toLinearMap (a * x * b * x) = 0 := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.centeredHaarLaurentSpan, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.FreeHaarMoments.centeredProjectionMoments_of_laurent_approx line 295
Source documentation
The precise two centered projection moments, obtained from Laurent approximation to the spectral projection. No freeness conclusion is an assumption of this theorem.
```
theorem centeredProjectionMoments_of_laurent_approx (h : FreeHaarMoments τ A v)
    {p e : B} {t η : ℝ} (hp : p ∈ A) (hpτ : τ.toLinearMap p = (t : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ)) (c : ℕ → B)
    (hc : ∀ n, c n ∈ haarLaurentSpan v)
    (hlim : Tendsto (fun n => traceTwoNorm τ (c n - e)) atTop (𝓝 0)) :
    CenteredProjectionMoments τ p e t η := by
…
```
Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarLaurentSpan, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.CenteredProjectionMoments