OAI/Analysis/BoundedHochschild/RightModuleFixedPoints.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The common fixed points of right averaging are exactly the left multiplication maps. This identifies the target of the projection without assuming that a common fixed point has already been constructed.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.right_module_of_unitary_averages line 15
  2. lemma OAI.BoundedHochschild.KadisonRingrose.right_module_eq_left_multiplication line 27
  3. theorem OAI.BoundedHochschild.KadisonRingrose.fixed_right_averages_iff line 33
  4. theorem OAI.BoundedHochschild.KadisonRingrose.weak_fixed_right_averages_realize line 51

    Source documentation

    A simultaneous weak-star fixed point, when constructed, is necessarily an actual bounded left multiplication map.

    theorem weak_fixed_right_averages_realize (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {F : M → WeakDual ℂ X} {C : ℝ} (hC : 0 ≤ C) (hF : F ∈ weakOperatorBall C)
    (hfix : ∀ (n : ℕ) (m : Fin n → M), (∑ i, m i * star (m i) = 1) →
      weakRightAverage e m F = F) :
    ∃ b : M, ‖ContinuousLinearMap.mul ℂ M b‖ ≤ C ∧
      weakOperatorImage e (ContinuousLinearMap.mul ℂ M b) = F := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.weakOperatorBall, OAI.BoundedHochschild.KadisonRingrose.weakRightAverage, OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage