OAI/Analysis/FactorGeneration/FreeGroupMoments.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Every nonempty reduced word in successive Haar variables has zero trace. The induction eliminates the largest label, retaining centered lower-label gaps.

  1. def OAI.Generator.Tracial.unitaryWord line 16
  2. theorem OAI.Generator.Tracial.unitaryWord_nil line 19
  3. theorem OAI.Generator.Tracial.unitaryWord_cons line 22
  4. theorem OAI.Generator.Tracial.unitaryWord_append line 26
  5. theorem OAI.Generator.Tracial.unitaryWord_mem line 30
  6. theorem OAI.Generator.Tracial.maximal_word_gaps line 45

    Source documentation

    Scan the tail after a maximal label. Empty gaps can only join equal signs.

    theorem maximal_word_gaps (v : ℕ → unitary (Q τ ω))
    (D : StarSubalgebra ℂ (Q τ ω)) (n : ℕ)
    (hv : ∀ i < n,(v i : Q τ ω) ∈ D)
    (hzero : ∀ a : List (ℕ × Bool),FreeGroup.IsReduced a → a ≠ [] →
      (∀ x ∈ a,x.1 < n) → quotientTrace τ ω (unitaryWord τ ω v a)=0)
    (w : List (ℕ × Bool)) (s : Bool)
    (hr : FreeGroup.IsReduced ((n,s)::w)) (hn : ∀ x ∈ w,x.1 ≤ n) :
    ∃ xs b,b ∈ D ∧ SignedReducedGaps τ ω D.toSubalgebra (!s) xs ∧
      unitaryWord τ ω v ((n,s)::w)=betweenWord (v n : Q τ ω) (!s) xs b := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.unitaryWord, OAI.Generator.Tracial.SignedReducedGaps, OAI.Generator.Tracial.betweenWord

  7. theorem OAI.Generator.Tracial.successive_reduced_word_zero line 90
  8. def OAI.Generator.Tracial.unitaryRepresentation line 134
  9. theorem OAI.Generator.Tracial.unitaryRepresentation_mk line 137
  10. theorem OAI.Generator.Tracial.successive_freeGroup_trace line 147
  11. theorem OAI.Generator.Tracial.unitaryRepresentation_injective line 162

    Source documentation

    Zero nonidentity moments imply faithfulness, since the unit has trace one.

    theorem unitaryRepresentation_injective {A : Type*} (v : A → unitary (Q τ ω))
    (hzero : ∀ g : FreeGroup A,g ≠ 1 →
      quotientTrace τ ω (unitaryRepresentation τ ω v g : Q τ ω)=0) :
    Function.Injective (unitaryRepresentation τ ω v) := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.unitaryRepresentation

  12. theorem OAI.Generator.Tracial.unitaryRepresentation_gram line 174
  13. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.freeGroup_trace line 198
  14. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.freeGroup_injective line 207
  15. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.freeGroup_gram line 213
  16. def OAI.Generator.Tracial.conjugateVariables line 232
  17. def OAI.Generator.Tracial.conjugateGaps line 235
  18. def OAI.Generator.Tracial.conjugateEnd line 240
  19. theorem OAI.Generator.Tracial.signed_conjugate line 244
  20. theorem OAI.Generator.Tracial.conjugateWord_formula line 254
  21. theorem OAI.Generator.Tracial.conjugateEnd_mem line 271
  22. theorem OAI.Generator.Tracial.conjugateGaps_reduced line 278
  23. theorem OAI.Generator.Tracial.conjugate_reduced_word_zero line 293
  24. theorem OAI.Generator.Tracial.conjugate_freeGroup_trace line 306
  25. theorem OAI.Generator.Tracial.HaarEndpoints.base_correlation line 324
  26. theorem OAI.Generator.Tracial.HaarEndpoints.positive_conjugate_correlation line 330
  27. theorem OAI.Generator.Tracial.HaarEndpoints.negative_conjugate_correlation line 345