RelativeHaarExpectation.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Conjugating a free Haar model into relative free position

All expectation properties used here follow from its range and trace-pairing identities. The finite-base construction supplies those identities later.

def OAI.KadisonKastler.relativeHaarKernel line 19
Source documentation
The centered part of a containing algebra for the finite base projection.
```
def relativeHaarKernel (E : B →ₗ[ℂ] B) (T : StarSubalgebra ℂ B) : Submodule ℂ B :=
…
```
theorem OAI.KadisonKastler.mem_relativeHaarKernel line 23
structure OAI.KadisonKastler.TraceBaseProjection line 27
Source documentation
A trace projection is specified by precisely its range and pairing properties.
```
structure TraceBaseProjection (τ : FaithfulTracialState B) (D : StarSubalgebra ℂ B)
    (E : B →ₗ[ℂ] B) : Prop where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.TraceBaseProjection.trace line 39
theorem OAI.KadisonKastler.TraceBaseProjection.eq_of_pairings line 43
theorem OAI.KadisonKastler.TraceBaseProjection.fixed line 50
theorem OAI.KadisonKastler.TraceBaseProjection.left_mul line 53
theorem OAI.KadisonKastler.TraceBaseProjection.right_mul line 59
theorem OAI.KadisonKastler.TraceBaseProjection.kernel_trace line 71
theorem OAI.KadisonKastler.TraceBaseProjection.kernel_left_mul line 74
theorem OAI.KadisonKastler.TraceBaseProjection.kernel_right_mul line 77
theorem OAI.KadisonKastler.TraceBaseProjection.conjugate line 81
Source documentation
Conjugation by a unitary commuting with the base preserves its trace projection.
```
theorem conjugate (w : unitary B) (hw : ∀ d ∈ D, Commute (w : B) d) (x : B) :
    E ((w : B) * x * star (w : B)) = E x := by
…
```
theorem OAI.KadisonKastler.haarPower_unitary_conjugate line 101
Source documentation
Integer powers of a conjugated unitary telescope exactly.
```
theorem haarPower_unitary_conjugate (w s : unitary B) (k : ℤ) :
    haarPower (w * s * star w) k = (w : B) * haarPower s k * star (w : B) := by
…
```
Mentions: OAI.KadisonKastler.haarPower
theorem OAI.KadisonKastler.trace_unitary_conjugate line 108
Source documentation
Traces are invariant under the same conjugation.
```
theorem trace_unitary_conjugate (τ : FaithfulTracialState B) (w : unitary B) (x : B) :
    τ.toLinearMap ((w : B) * x * star (w : B)) = τ.toLinearMap x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState

theorem OAI.KadisonKastler.haar_moments_unitary_conjugate line 113

Source documentation

In particular, conjugation retains the Haar moments.

theorem haar_moments_unitary_conjugate (τ : FaithfulTracialState B)
    (w s : unitary B)
    (hs : ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower s k) = 0) :
    ∀ k : ℤ, k ≠ 0 → τ.toLinearMap (haarPower (w * s * star w) k) = 0 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.haarPower