IndependenceMoments.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar free moments from finite-base independence

The endpoint form of Popa's independence identity gives exactly the alternating moments used by the free diagonal construction. The final Haar exponent may vanish; in that case its coefficient is an endpoint.

theorem OAI.KadisonKastler.property_before_last line 20
theorem OAI.KadisonKastler.HaarEndpointIndependence.word_with_endpoint line 43
theorem OAI.KadisonKastler.HaarEndpointIndependence.centered_word line 58
Source documentation
The endpoint identity also permits a zero final exponent, by absorbing the final centered coefficient into the endpoint.
```
theorem centered_word (h : HaarEndpointIndependence τ D X w)
    (htrace : ∀ x ∈ X, τ.toLinearMap x = 0)
    (l : List (B × ℤ)) (hl : l ≠ [])
    (hmem : ∀ z ∈ l, z.1 ∈ X)
    (hexp : l.IsChain (fun x _ => x.2 ≠ 0)) :
    τ.toLinearMap (centeredHaarWord w l) = 0 := by
…
```
Mentions: OAI.KadisonKastler.HaarEndpointIndependence, OAI.KadisonKastler.centeredHaarWord
theorem OAI.KadisonKastler.HaarEndpointIndependence.freeHaarMoments line 88
Source documentation
The scalar freeness hypothesis needed downstream follows from the published endpoint identity whenever the centered base lies in X.
```
theorem freeHaarMoments (h : HaarEndpointIndependence τ D X w)
    (hhaar : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower w k) = 0)
    (htrace : ∀ x ∈ X, τ.toLinearMap x = 0)
    (A : StarSubalgebra ℂ B)
    (hAX : ∀ a ∈ A, τ.toLinearMap a = 0 → a ∈ X) :
    FreeHaarMoments τ A w := by
…
```
Mentions: OAI.KadisonKastler.HaarEndpointIndependence, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.FreeHaarMoments