FreeHaarConjugation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Scalar freeness after the second finite-base independence step

Centered letters are split by the trace projection. Consecutive base letters and Haar powers are retained as explicit reduced blocks; the remaining letters are in the relative kernel and are killed by Popa's endpoint identity.

def OAI.KadisonKastler.haarConjugate line 19
theorem OAI.KadisonKastler.haarConjugate_mul line 22
theorem OAI.KadisonKastler.haarConjugate_fixed line 31
theorem OAI.KadisonKastler.haarConjugate_right_base line 35
theorem OAI.KadisonKastler.haarConjugate_left_base line 40
theorem OAI.KadisonKastler.haarConjugate_power line 45
theorem OAI.KadisonKastler.split_centered_letter line 59
theorem OAI.KadisonKastler.block_kernel line 68
theorem OAI.KadisonKastler.completed_trace line 73

theorem OAI.KadisonKastler.continuation_trace_zero line 84

Source documentation

The finite expansion induction, retaining each maximal base/Haar segment as a reduced block rather than assuming an amalgamated-freeness theorem.

private theorem continuation_trace_zero
    (l : List (B × ℤ))
    (hm : ∀ z ∈ l, z.1 ∈ A) (hz : ∀ z ∈ l, τ.toLinearMap z.1 = 0)
    (hk : l.IsChain (fun z _ => z.2 ≠ 0))
    (a : B) (ha : a ∈ relativeHaarKernel E T ∨ a = 1)
    (p : List (B × B))
    (hp : ∀ z ∈ p, z.1 ∈ relativeHaarKernel E T ∧ z.2 ∈ relativeHaarKernel E T)
    (r : RelativeHaarBlock τ D s) :
    τ.toLinearMap (conjugateBlockPrefix w a p * haarConjugate w r.value *
      centeredHaarWord (w * s * star w) l) = 0 := by
…

Mentions: OAI.KadisonKastler.relativeHaarKernel, OAI.KadisonKastler.RelativeHaarBlock, OAI.KadisonKastler.conjugateBlockPrefix, OAI.KadisonKastler.haarConjugate, OAI.KadisonKastler.centeredHaarWord

theorem OAI.KadisonKastler.second_stage_centered_word line 161
theorem OAI.KadisonKastler.freeHaarMoments_of_second_independence line 199
Source documentation
The second-stage finite-base independence produces scalar free Haar moments relative to the whole prescribed algebra.
```
theorem freeHaarMoments_of_second_independence :
    FreeHaarMoments τ A (w * s * star w) := by
…
```
Mentions: OAI.KadisonKastler.FreeHaarMoments