WeakNestedConvexHull.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Closed convex hulls of decreasing weakly compact sets

All closures of convex hulls below are taken in the original norm topology. The compact sets themselves live in the distinct weak copy. A continuous linear functional attains a maximum on each compact set. Nested compact half-space cuts then supply a point of the intersection with at least the value of the proposed anchor. Hahn--Banach separation proves membership in the norm-closed convex hull of that intersection.

theorem OAI.ReflexiveFixedPoints.weakCopy_t2Space line 26
Source documentation
The scalar evaluations separate points of the actual weak copy.
```
private theorem weakCopy_t2Space : T2Space (WeakSpace ℝ X) := by
…
```
theorem OAI.ReflexiveFixedPoints.weaklyCompact_iInter_nonempty_compact line 40
Source documentation
A decreasing sequence of nonempty weakly compact sets has nonempty compact intersection. No completeness assumption on the normed space is needed.
```
theorem weaklyCompact_iInter_nonempty_compact
    (B : ℕ → Set (WeakSpace ℝ X))
    (hBc : ∀ n, IsCompact (B n)) (hBn : ∀ n, (B n).Nonempty)
    (hBanti : Antitone B) :
    (⋂ n, B n).Nonempty ∧ IsCompact (⋂ n, B n) := by
…
```

theorem OAI.ReflexiveFixedPoints.exists_dual_ge_of_mem_closure_convexHull_weaklyCompact line 54

Source documentation

A functional's maximum over a nonempty weakly compact set bounds its value on the norm-closed convex hull.

theorem exists_dual_ge_of_mem_closure_convexHull_weaklyCompact
    (B : Set (WeakSpace ℝ X)) (hBc : IsCompact B) (hBn : B.Nonempty)
    {x : X} (hx : x ∈ closure (convexHull ℝ ((toWeakSpace ℝ X) ⁻¹' B)))
    (f : X →L[ℝ] ℝ) :
    ∃ z ∈ B, f x ≤ f ((toWeakSpace ℝ X).symm z) := by
…

theorem OAI.ReflexiveFixedPoints.mem_closure_convexHull_iInter_weaklyCompact line 80
Source documentation
A point in the norm-closed convex hull of every decreasing nonempty weakly compact set belongs to the norm-closed convex hull of their intersection. Compactness, rather than a general interchange law for convex hulls and intersections, supplies the crucial step.
```
theorem mem_closure_convexHull_iInter_weaklyCompact
    (B : ℕ → Set (WeakSpace ℝ X))
    (hBc : ∀ n, IsCompact (B n)) (hBn : ∀ n, (B n).Nonempty)
    (hBanti : Antitone B) {x : X}
    (hx : ∀ n, x ∈ closure (convexHull ℝ ((toWeakSpace ℝ X) ⁻¹' B n))) :
    x ∈ closure (convexHull ℝ ((toWeakSpace ℝ X) ⁻¹' (⋂ n, B n))) := by
…
```