OAI/Analysis/Unitarizability/CompactMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Dixmier.amenable_of_approximate_means line 16

   Source documentation

   Approximate positive normalized means, with all finite translation tests, have a positive normalized invariant weak-star cluster point.

   theorem amenable_of_approximate_means
       (h : ∀ (S : Finset G) (ε : ℝ), 0 < ε →
         ∃ m : (G →ᵇ ℂ) →L[ℂ] ℂ,
           ‖m‖ ≤ 1 ∧ m (BoundedContinuousFunction.const G (1 : ℂ)) = 1 ∧
           (∀ b : G →ᵇ ℂ, (∀ x, 0 ≤ (b x).re ∧ (b x).im = 0) →
             0 ≤ (m b).re ∧ (m b).im = 0) ∧
           ∀ g ∈ S, ∀ b : G →ᵇ ℂ, ‖m (leftTranslate g b) - m b‖ ≤ ε * ‖b‖) :
       Amenable G := by
   …

   Mentions: OAI.Dixmier.leftTranslate, OAI.Dixmier.Amenable