IsometricFixedPoint.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Common fixed points for weakly compact linear isometric actions

A countable orbit generates a norm-separable closed convex hull. Applying the separable argument to free groups on finitely many prescribed elements, then using compactness, removes the separability restriction.

theorem OAI.BoundedHochschild.KadisonRingrose.weakCompact_countable_isometric_fixedPoint line 28

Source documentation

A countable acting group can be restricted to the separable closed convex hull of one orbit.

theorem weakCompact_countable_isometric_fixedPoint [Countable G]
    (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) (hinv : ∀ g, Set.MapsTo (weakIsometry (T g)) C C) :
    ∃ x ∈ C, ∀ g, weakIsometry (T g) x = x := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.weakIsometry

theorem OAI.BoundedHochschild.KadisonRingrose.weakCompact_isometric_fixedPoint line 86

Source documentation

The linear-isometric case of the Ryll-Nardzewski fixed-point theorem, without separability assumptions.

theorem weakCompact_isometric_fixedPoint
    (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) (hinv : ∀ g, Set.MapsTo (weakIsometry (T g)) C C) :
    ∃ x ∈ C, ∀ g, weakIsometry (T g) x = x := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.weakIsometry