OAI/Analysis/BoundedHochschild/WeakCompactFragment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A small weakly open piece of a norm-separable compact set

The Baire-category step of the isometric fixed-point argument. It is used only on the compact orbit hull of a countably generated unitary subgroup.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.weak_closedBall line 27
  2. theorem OAI.BoundedHochschild.KadisonRingrose.weakCompact_small_open_piece line 34

    Source documentation

    A nonempty weakly compact, norm-separable set has a nonempty relatively weakly open subset of arbitrarily small norm diameter.

    theorem weakCompact_small_open_piece (K : Set (WeakSpace ℂ E))
    (hK : IsCompact K) (hne : K.Nonempty)
    (hsep : IsSeparable ((toWeakSpace ℂ E).symm '' K))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ U : Set (WeakSpace ℂ E), IsOpen U ∧ (K ∩ U).Nonempty ∧
      ∀ x ∈ K ∩ U, ∀ y ∈ K ∩ U,
        ‖(toWeakSpace ℂ E).symm x - (toWeakSpace ℂ E).symm y‖ < ε := by
…