OAI/Analysis/FactorGeneration/ProductWords.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Exact signed-word expansion for a product of two unitaries. A unit gap is allowed only between equal signs; opposite signs retain a centered gap.

  1. def OAI.Generator.Tracial.productLeft line 15
  2. def OAI.Generator.Tracial.productRight line 16
  3. theorem OAI.Generator.Tracial.signed_product_split line 18
  4. def OAI.Generator.Tracial.betweenWord line 22
  5. def OAI.Generator.Tracial.productGapList line 26
  6. def OAI.Generator.Tracial.finalWordSign line 30
  7. theorem OAI.Generator.Tracial.betweenWord_product line 34
  8. theorem OAI.Generator.Tracial.exactOrderedMoments_values line 51
  9. def OAI.Generator.Tracial.ProductGaps line 71

    Source documentation

    Centered coefficients may separate arbitrary signs; unit coefficients may only separate equal signs. This excludes cancellation through an internal unit.

    def ProductGaps (x : ℕ → Q τ ω) (s : Bool) : List (Q τ ω × Bool) → Prop
  | [] => True
  | (d,t)::xs => ((∃ i,x i=d) ∨ (d=1 ∧ s=t)) ∧ ProductGaps x t xs

    Mentions: OAI.Generator.Tracial.Q

  10. def OAI.Generator.Tracial.ReducedOrderedMoments line 75
  11. abbrev OAI.Generator.Tracial.ProductFamilyIndex line 88
  12. def OAI.Generator.Tracial.productFamilyValue line 90
  13. def OAI.Generator.Tracial.productCenteredFamily line 95
  14. theorem OAI.Generator.Tracial.productCenteredFamily_encode line 100
  15. theorem OAI.Generator.Tracial.productCenteredFamily_centered line 104
  16. theorem OAI.Generator.Tracial.productFamily_original line 129
  17. theorem OAI.Generator.Tracial.productFamily_right line 133
  18. theorem OAI.Generator.Tracial.productFamily_left line 138
  19. theorem OAI.Generator.Tracial.productFamily_conjugate line 143
  20. theorem OAI.Generator.Tracial.productFamily_optional line 148
  21. theorem OAI.Generator.Tracial.productFamily_first line 156
  22. theorem OAI.Generator.Tracial.productFamily_last line 164
  23. theorem OAI.Generator.Tracial.productFamily_gap line 172
  24. theorem OAI.Generator.Tracial.productGapList_members line 185
  25. theorem OAI.Generator.Tracial.product_reduced_moment line 197

    Source documentation

    The product has every reduced signed moment, including same-sign unit gaps.

    theorem product_reduced_moment (u v : Q τ ω) (x : ℕ → Q τ ω)
    (hm : ExactOrderedMoments τ ω v (productCenteredFamily τ ω u x))
    (a b : Option ℕ) (s : Bool) (xs : List (Q τ ω × Bool))
    (hx : ProductGaps τ ω x s xs) :
    quotientTrace τ ω (optionalCoefficient x a*betweenWord (u*v) s xs
      (optionalCoefficient x b))=0 := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.ExactOrderedMoments, OAI.Generator.Tracial.productCenteredFamily, OAI.Generator.Tracial.ProductGaps, OAI.Generator.Tracial.optionalCoefficient, OAI.Generator.Tracial.betweenWord

  26. def OAI.Generator.Tracial.powerBlockGaps line 217
  27. def OAI.Generator.Tracial.powerBlockWord line 221
  28. theorem OAI.Generator.Tracial.betweenWord_repeat_prefix line 225
  29. theorem OAI.Generator.Tracial.powerBlockWord_expand line 232
  30. def OAI.Generator.Tracial.integerPowerBlock line 245

    Source documentation

    Magnitude is encoded as predecessor, so every resulting block has positive length.

    def integerPowerBlock : ℤ → Bool × ℕ
  | .ofNat n => (false,n-1)
  | .negSucc n => (true,n)
  31. theorem OAI.Generator.Tracial.integerPowerBlock_eval line 249
  32. def OAI.Generator.Tracial.integerWord line 265
  33. theorem OAI.Generator.Tracial.integerWord_blocks line 269
  34. theorem OAI.Generator.Tracial.productGaps_repeat_prefix line 285
  35. theorem OAI.Generator.Tracial.productGaps_powerBlocks line 294
  36. theorem OAI.Generator.Tracial.reducedOrderedMoments_integerWord line 304
  37. theorem OAI.Generator.Tracial.reducedOrderedMoments_haar line 316