OAI/Analysis/BoundedHochschild/WeakIsometricFixedPoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The separable isometric fixed-point argument

This is the specialization of the Ryll-Nardzewski argument needed for the normal-state orbit: a linear isometric group acting on a weakly compact, norm-separable convex set has a common fixed point.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.minimal_weak_convex_invariant line 27
  2. theorem OAI.BoundedHochschild.KadisonRingrose.weakCompact_separable_isometric_fixedPoint line 63

    Source documentation

    Common fixed point for the norm-separable weakly compact case.

    theorem weakCompact_separable_isometric_fixedPoint [CompleteSpace E]
    (T : G → E ≃ₗᵢ[ℂ] E)
    (hone : ∀ x, T 1 x = x) (hmul : ∀ g h x, T (g * h) x = T g (T h x))
    (C : Set (WeakSpace ℂ E)) (hC : IsCompact C) (hne : C.Nonempty)
    (hconv : Convex ℝ C) (hsep : IsSeparable ((toWeakSpace ℂ E).symm '' C))
    (hinv : ∀ g, Set.MapsTo (weakIsometry (T g)) C C) :
    ∃ x ∈ C, ∀ g, weakIsometry (T g) x = x := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.weakIsometry