OAI/Analysis/KadisonKastler/DenseSupportSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Dense support tests for a bounded closed convex set

A dense family of Hilbert-space support tests suffices when the candidate set is uniformly bounded. This is used for self-adjoint operator balls.

  1. theorem OAI.KadisonKastler.mem_closed_convex_of_dense_support line 21

    Source documentation

    The uniform bound lets dense tests recover every separating functional.

    theorem mem_closed_convex_of_dense_support {C D : Set E} {y : E} {B : ℝ}
    (hC : IsClosed C) (hconv : Convex ℝ C) (hD : Dense D)
    (hB : ∀ x ∈ C, ‖x‖ ≤ B)
    (htest : ∀ h ∈ D, ∃ x ∈ C, inner ℝ h y ≤ inner ℝ h x) : y ∈ C := by
…