OAI/Analysis/KadisonKastler/FreeHaarTwist.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Finite word reductions for unitary twists of a free Haar unitary

The reduction splits an uncentered separator into its centered and scalar parts. A scalar separator is removed only between powers of the same sign, so their merged exponent is nonzero. These are algebraic trace arguments, with no additional free-probability input.

  1. def OAI.KadisonKastler.leftHaarWord line 25
  2. def OAI.KadisonKastler.rightHaarWord line 28
  3. def OAI.KadisonKastler.shiftedPowers line 31
  4. theorem OAI.KadisonKastler.shiftedPowers_fst line 37
  5. theorem OAI.KadisonKastler.shiftedPowers_property line 47
  6. theorem OAI.KadisonKastler.shiftedPowers_nonzero line 58
  7. theorem OAI.KadisonKastler.shiftedPowers_word line 75
  8. theorem OAI.KadisonKastler.FreeHaarMoments.trace_rightWord_centered line 91
  9. theorem OAI.KadisonKastler.FreeHaarMoments.trace_leftWord_centered line 105
  10. def OAI.KadisonKastler.FreeHaarMoments.SameSignSeparated line 129
  11. theorem OAI.KadisonKastler.FreeHaarMoments.sameSign_merge line 134
  12. theorem OAI.KadisonKastler.FreeHaarMoments.separated_merge line 150
  13. theorem OAI.KadisonKastler.FreeHaarMoments.trace_signSeparated line 160

    Source documentation

    Finite sign reduction: only an uncentered separator between powers of the same sign is removed in the scalar branch.

    private theorem trace_signSeparated (h : FreeHaarMoments τ A s)
    (tail : List (B × ℤ)) (pref : List (B × ℤ)) (q : ℤ)
    (hp_mem : ∀ x ∈ pref, x.1 ∈ A)
    (hp_z : ∀ x ∈ pref, τ.toLinearMap x.1 = 0)
    (hp_k : ∀ x ∈ pref.tail, x.2 ≠ 0)
    (hq : q ≠ 0 ∨ pref = [])
    (ht_mem : ∀ x ∈ tail, x.1 ∈ A)
    (ht : SameSignSeparated (τ := τ) q tail)
…

    Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.FreeHaarMoments.SameSignSeparated

  14. def OAI.KadisonKastler.FreeHaarMoments.signPower line 231
  15. def OAI.KadisonKastler.FreeHaarMoments.twistCarry line 233
  16. def OAI.KadisonKastler.FreeHaarMoments.twistFront line 237
  17. theorem OAI.KadisonKastler.FreeHaarMoments.twistPower_sign line 239
  18. def OAI.KadisonKastler.FreeHaarMoments.expandedAtoms line 245
  19. def OAI.KadisonKastler.FreeHaarMoments.terminalCarry line 251
  20. theorem OAI.KadisonKastler.FreeHaarMoments.expandedAtoms_word line 255
  21. theorem OAI.KadisonKastler.FreeHaarMoments.twistCarry_mem line 270
  22. theorem OAI.KadisonKastler.FreeHaarMoments.twistFront_mem line 276
  23. theorem OAI.KadisonKastler.FreeHaarMoments.expandedAtoms_mem line 282
  24. theorem OAI.KadisonKastler.FreeHaarMoments.terminalCarry_mem line 294
  25. def OAI.KadisonKastler.FreeHaarMoments.previousPower line 300
  26. theorem OAI.KadisonKastler.FreeHaarMoments.twist_separator_centered line 304
  27. theorem OAI.KadisonKastler.FreeHaarMoments.expandedAtoms_separated line 317
  28. theorem OAI.KadisonKastler.FreeHaarMoments.trace_signed_atoms line 340

    Source documentation

    A signed expansion with centered sign-change separators has zero trace even after multiplication by its final coefficient in the base algebra.

    private theorem trace_signed_atoms (h : FreeHaarMoments τ A s)
    (U : unitary B) (hU : (U : B) ∈ A) (l : List (B × Bool)) (hl : l ≠ [])
    (hmem : ∀ x ∈ l, x.1 ∈ A)
    (hchain : l.IsChain (fun x y => x.2 ≠ y.2 → τ.toLinearMap y.1 = 0))
    (b : B) (hb : b ∈ A) :
    τ.toLinearMap (b * (l.map (fun x => x.1 *
      haarPower (s * U) (signPower x.2))).prod) = 0 := by
…

    Mentions: OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.haarPower, OAI.KadisonKastler.FreeHaarMoments.signPower

  29. def OAI.KadisonKastler.FreeHaarMoments.powerAtoms line 371
  30. theorem OAI.KadisonKastler.FreeHaarMoments.powerAtoms_ne_nil line 376
  31. theorem OAI.KadisonKastler.FreeHaarMoments.powerAtoms_word line 381
  32. theorem OAI.KadisonKastler.FreeHaarMoments.powerAtoms_mem line 403
  33. theorem OAI.KadisonKastler.FreeHaarMoments.powerAtoms_head line 409
  34. theorem OAI.KadisonKastler.FreeHaarMoments.powerAtoms_chain line 415
  35. def OAI.KadisonKastler.FreeHaarMoments.allPowerAtoms line 432
  36. theorem OAI.KadisonKastler.FreeHaarMoments.allPowerAtoms_head line 435
  37. theorem OAI.KadisonKastler.FreeHaarMoments.allPowerAtoms_chain line 450
  38. theorem OAI.KadisonKastler.FreeHaarMoments.allPowerAtoms_word line 460
  39. theorem OAI.KadisonKastler.FreeHaarMoments.trace_nonzero_twisted_powers line 474
  40. theorem OAI.KadisonKastler.FreeHaarMoments.trace_twisted_power line 494
  41. theorem OAI.KadisonKastler.FreeHaarMoments.nonzero_before_last line 502
  42. theorem OAI.KadisonKastler.FreeHaarMoments.trace_alternating_twist_list line 516
  43. theorem OAI.KadisonKastler.FreeHaarMoments.mul_right line 546

    Source documentation

    Multiplying a free Haar unitary on the right by any unitary of the base algebra preserves its Haar and alternating centered moments.

    theorem mul_right (h : FreeHaarMoments τ A s) (U : unitary B) (hU : (U : B) ∈ A) :
    FreeHaarMoments τ A (s * U) where
…

    Mentions: OAI.KadisonKastler.FreeHaarMoments