MinimalIsometricOrbit.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Minimal weakly compact isometric orbits are norm compact in a separable space.

def OAI.BoundedHochschild.KadisonRingrose.weakIsometry line 22
Source documentation
The weak action associated to a linear isometry.
```
def weakIsometry (T : E ≃ₗᵢ[ℂ] E) : WeakSpace ℂ E → WeakSpace ℂ E :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakIsometry_apply line 25

theorem OAI.BoundedHochschild.KadisonRingrose.minimal_isometric_orbit_finite_net line 29

Source documentation

Minimality and the Baire small-piece lemma give a finite norm net.

theorem minimal_isometric_orbit_finite_net (T : G → E ≃ₗᵢ[ℂ] E)
    (hone : ∀ x, T 1 x = x) (hmul : ∀ g h x, T (g * h) x = T g (T h x))
    (K : Set (WeakSpace ℂ E)) (hK : IsCompact K) (hne : K.Nonempty)
    (hsep : IsSeparable ((toWeakSpace ℂ E).symm '' K))
    (hinv : ∀ g, Set.MapsTo (weakIsometry (T g)) K K)
    (hmin : ∀ L : Set (WeakSpace ℂ E), L ⊆ K → L.Nonempty → IsClosed L →
      (∀ g, Set.MapsTo (weakIsometry (T g)) L L) → K ⊆ L)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ s : Finset E, (↑s : Set E) ⊆ (toWeakSpace ℂ E).symm '' K ∧
      ∀ x ∈ K, ∃ y ∈ s, ‖(toWeakSpace ℂ E).symm x - y‖ < ε := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.weakIsometry

theorem OAI.BoundedHochschild.KadisonRingrose.minimal_isometric_orbit_normCompact line 72

Source documentation

A minimal weakly compact orbit inside a norm-separable Banach space is compact for the norm topology as well.

theorem minimal_isometric_orbit_normCompact [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))
    (K : Set (WeakSpace ℂ E)) (hK : IsCompact K) (hne : K.Nonempty)
    (hsep : IsSeparable ((toWeakSpace ℂ E).symm '' K))
    (hinv : ∀ g, Set.MapsTo (weakIsometry (T g)) K K)
    (hmin : ∀ L : Set (WeakSpace ℂ E), L ⊆ K → L.Nonempty → IsClosed L →
      (∀ g, Set.MapsTo (weakIsometry (T g)) L L) → K ⊆ L) :
    IsCompact ((toWeakSpace ℂ E).symm '' K) := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.weakIsometry