OAI/Analysis/KadisonSimilarity/Tracial/IntegerMomentScaling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar homogeneity of each finite integer-power mixed word.

  1. def OAI.KadisonSimilarity.intWordCoeffNumber line 13
  2. theorem OAI.KadisonSimilarity.integerEval_smul line 16
  3. def OAI.KadisonSimilarity.wordScalar line 34
  4. lemma OAI.KadisonSimilarity.wordCoeff_smul_family line 38
  5. theorem OAI.KadisonSimilarity.integerEval_smul_family line 44

    Source documentation

    Each coefficient can be rescaled separately, including coefficients that occur repeatedly in the word.

    theorem integerEval_smul_family (F : I → B) (c : I → ℂ) (u : unitary B)
    (a : Option I) (l : List (IntAtom I)) :
    integerEval (fun i => c i • F i) u a l =
      (wordScalar c a * (l.map (fun b => wordScalar c b.2)).prod) • integerEval F u a l := by
…

    Mentions: OAI.KadisonSimilarity.wordScalar