CompactHilbertCenter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Unique centers of compact convex Hilbert images

Only compactness for the lower semicontinuous squared distances is used. This form applies directly to weak operator compact sets of implementers.

theorem OAI.KadisonKastler.exists_unique_compact_hilbert_center line 21

Source documentation

A compact family whose Hilbert image is bounded and midpoint convex has a unique image minimizing its squared covering radius.

theorem exists_unique_compact_hilbert_center
    (K : Set X) (hK : IsCompact K) (hne : K.Nonempty) (v : X → E)
    (hdist : ∀ y, LowerSemicontinuous (fun x => ‖v x - y‖ ^ 2))
    (hmid : ∀ x ∈ K, ∀ y ∈ K,
      ∃ z ∈ K, v z = (1 / 2 : ℝ) • (v x + v y))
    (C : ℝ) (hC : ∀ x ∈ K, ‖v x‖ ≤ C) :
    ∃ x ∈ K, ∀ y ∈ K,
      (∀ z ∈ K, ‖v y - v z‖ ^ 2 ≤ ⨆ w : K, ‖v x - v w‖ ^ 2) → v y = v x := by
…