HaarProjectionApproximation.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Laurent approximation of tracial limits

A diagonal selection retains Laurent approximation after taking a tracial two-norm limit. Applied to continuous circle cutoffs, this passes the finite Laurent moment calculations to the resulting arc projection.

theorem OAI.KadisonKastler.exists_haarLaurent_approx_of_traceTwoNorm_limit line 26

Source documentation

Choose one Laurent approximant at each stage of a convergent sequence, with error less than 1 / (n + 1).

theorem exists_haarLaurent_approx_of_traceTwoNorm_limit
    (τ : FaithfulTracialState B) (v : unitary B) (x : ℕ → B) (e : B)
    (happrox : ∀ n, ∃ c : ℕ → B, (∀ k, c k ∈ haarLaurentSpan v) ∧
      Tendsto (fun k => traceTwoNorm τ (c k - x n)) atTop (𝓝 0))
    (hlim : Tendsto (fun n => traceTwoNorm τ (x n - e)) atTop (𝓝 0)) :
    ∃ c : ℕ → B, (∀ n, c n ∈ haarLaurentSpan v) ∧
      Tendsto (fun n => traceTwoNorm τ (c n - e)) atTop (𝓝 0) := by
…

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

theorem OAI.KadisonKastler.exists_haarLaurent_approx_of_functional_limit line 54

Source documentation

Every tracial limit of continuous functions of the Haar unitary has actual Laurent-polynomial approximants.

theorem exists_haarLaurent_approx_of_functional_limit
    (τ : FaithfulTracialState B) (v : unitary B)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n)
    (g : ℕ → C(HaarCircle, ℂ)) (e : B)
    (hlim : Tendsto (fun n => traceTwoNorm τ (Φ (g n) - e)) atTop (𝓝 0)) :
    ∃ c : ℕ → B, (∀ n, c n ∈ haarLaurentSpan v) ∧
      Tendsto (fun n => traceTwoNorm τ (c n - e)) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.haarLaurentSpan

theorem OAI.KadisonKastler.haarLaurentSpan_mul_mem line 65
theorem OAI.KadisonKastler.haarLaurentSpan_star_mem line 83
def OAI.KadisonKastler.HaarLaurentApproximable line 95
Source documentation
Approximation in the tracial two-norm by finite Laurent polynomials.
```
def HaarLaurentApproximable (τ : FaithfulTracialState B) (v : unitary B) (x : B) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.haarLaurentApproximable_of_mem line 99
theorem OAI.KadisonKastler.HaarLaurentApproximable.add line 104
theorem OAI.KadisonKastler.HaarLaurentApproximable.star_closed line 115
theorem OAI.KadisonKastler.HaarLaurentApproximable.mul line 123
Source documentation
Product approximation is diagonal: the second error is chosen after the norm of the first approximant is known. Uniform bounds are unnecessary.
```
theorem HaarLaurentApproximable.mul {τ : FaithfulTracialState B} {v : unitary B}
    {x y : B} (hx : HaarLaurentApproximable τ v x) (hy : HaarLaurentApproximable τ v y) :
    HaarLaurentApproximable τ v (x * y) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.HaarLaurentApproximable
def OAI.KadisonKastler.haarLaurentTraceClosure line 160
Source documentation
The tracial closure of Laurent polynomials, restricted to bounded elements of the ambient C*-algebra, is an actual star subalgebra.
```
def haarLaurentTraceClosure (τ : FaithfulTracialState B) (v : unitary B) :
    StarSubalgebra ℂ B where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.mem_haarLaurentTraceClosure line 175
theorem OAI.KadisonKastler.unitary_mem_haarLaurentTraceClosure line 178
theorem OAI.KadisonKastler.mem_haarLaurentTraceClosure_of_functional_limit line 182
theorem OAI.KadisonKastler.FreeHaarMoments.projectionTraceIndependent_haarLaurentTraceClosure line 197
Source documentation
Every base-algebra element is trace independent of the entire bounded tracial Laurent closure.
```
theorem projectionTraceIndependent_haarLaurentTraceClosure (h : FreeHaarMoments τ A v)
    {p : B} (hp : p ∈ A) : ProjectionTraceIndependent τ p (haarLaurentTraceClosure τ v) := by
…
```
Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.ProjectionTraceIndependent, OAI.KadisonKastler.haarLaurentTraceClosure

theorem OAI.KadisonKastler.FreeHaarMoments.trace_mul_eq_mul_trace_of_functional_limit line 204

Source documentation

The degree-two factorization passes through the continuous cutoff limit.

theorem trace_mul_eq_mul_trace_of_functional_limit (h : FreeHaarMoments τ A v)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n)
    (g : ℕ → C(HaarCircle, ℂ)) {p e : B} (hp : p ∈ A)
    (hlim : Tendsto (fun n => traceTwoNorm τ (Φ (g n) - e)) atTop (𝓝 0)) :
    τ.toLinearMap (p * e) = τ.toLinearMap p * τ.toLinearMap e := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.traceTwoNorm

theorem OAI.KadisonKastler.FreeHaarMoments.centeredProjectionMoments_of_functional_limit line 215

Source documentation

In particular the two precise centered projection moments hold for the arc projection constructed as a tracial limit of continuous cutoffs.

theorem centeredProjectionMoments_of_functional_limit (h : FreeHaarMoments τ A v)
    (Φ : C(HaarCircle, ℂ) →⋆ₐ[ℂ] B)
    (hΦ : ∀ n : ℤ, Φ (fourier n) = haarPower v n)
    (g : ℕ → C(HaarCircle, ℂ)) {p e : B} {t η : ℝ}
    (hp : p ∈ A) (hpτ : τ.toLinearMap p = (t : ℂ))
    (heτ : τ.toLinearMap e = (η : ℂ))
    (hlim : Tendsto (fun n => traceTwoNorm τ (Φ (g n) - e)) atTop (𝓝 0)) :
    CenteredProjectionMoments τ p e t η := by
…

Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.HaarCircle, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.CenteredProjectionMoments