OAI/Analysis/BoundedHochschild/RightAveragingAlgebra.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Composition and convex combinations of elementary right averages

Normalized finite coefficient families are closed under concatenation and products. Thus the elementary averages form the convex semigroup used in the module-map projection argument.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_reindex line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.rightAverage_product_normalized line 26
  3. lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_comp line 38
  4. lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_sum line 46
  5. lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_real_smul line 52
  6. lemma OAI.BoundedHochschild.KadisonRingrose.rightAverage_real_smul_normalized line 60
  7. lemma OAI.BoundedHochschild.KadisonRingrose.rightAverage_convex_normalized line 68

    Source documentation

    Joining square-root-scaled coefficient families realizes a convex combination without changing normalization.

    lemma rightAverage_convex_normalized (m : I → M) (n : J → M)
    (hm : ∑ i, m i * star (m i) = 1) (hn : ∑ j, n j * star (n j) = 1)
    {r s : ℝ} (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) :
    ∑ p : I ⊕ J,
      (Sum.elim (fun i => Real.sqrt r • m i) (fun j => Real.sqrt s • n j) p) *
        star (Sum.elim (fun i => Real.sqrt r • m i) (fun j => Real.sqrt s • n j) p) = 1 := by
…
  8. lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_convex line 79