OAI/Analysis/BoundedHochschild/RightAveragingOrbit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The compact invariant family of elementary right averages. This is the compactness portion of the module projection construction; it does not yet assert that a member of the family is a right module map.

  1. def OAI.BoundedHochschild.KadisonRingrose.rightAverageOrbit line 19

    Source documentation

    All finite normalized elementary right averages of one map.

    def rightAverageOrbit (T : M →L[ℂ] M) : Set (M →L[ℂ] M) :=
…
  2. lemma OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_mem_orbit line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.self_mem_rightAverageOrbit line 31
  4. lemma OAI.BoundedHochschild.KadisonRingrose.rightAverageOrbit_invariant line 38
  5. lemma OAI.BoundedHochschild.KadisonRingrose.rightAverageOrbit_convex line 45
  6. lemma OAI.BoundedHochschild.KadisonRingrose.rightAverageOrbit_norm_le line 54
  7. def OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit line 69

    Source documentation

    Pointwise weak-star closure of the finite averaging orbit.

    def weakRightAverageOrbit (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] N) (T : N →L[ℂ] N) :
    Set (N → WeakDual ℂ X) := closure (weakOperatorImage e '' rightAverageOrbit T)
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage, OAI.BoundedHochschild.KadisonRingrose.rightAverageOrbit

  8. lemma OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_nonempty line 73
  9. lemma OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_subset_ball line 77
  10. theorem OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_isCompact line 84
  11. lemma OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_invariant line 91
  12. lemma OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_convex line 103