WeakBranchIntersection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One vector satisfying every branch halfspace

The finite-prefix witnesses lie in the same actual weakly compact set. Continuous linear evaluations define weakly closed halfspaces. Compactness then keeps one vector in all the constraints. In the final application the set is the whole unit ball of the closed difference span, viewed in X.

theorem OAI.ReflexiveFixedPoints.exists_weaklyCompact_all_halfspaces line 21

Source documentation

Finite-prefix feasibility in an actual weakly compact set gives one point in every halfspace. Only scalar linear evaluations use weak continuity.

theorem exists_weaklyCompact_all_halfspaces
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (B : Set X) (hB : WeaklyCompact B)
    (f : ℕ → X →L[ℝ] ℝ) (c : ℝ)
    (hPrefix : ∀ n : ℕ, ∃ x ∈ B, ∀ i < n, c ≤ f i x) :
    ∃ x ∈ B, ∀ i, c ≤ f i x := by
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact