WeakCompactness.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Weak compactness from the actual canonical bidual map

The inverse of the surjective canonical inclusion is weak-star to weak continuous because its scalar evaluations are precisely the evaluations of the bidual. Banach–Alaoglu then gives weak compactness of norm balls. Closed convex subsets are weakly closed by Hahn–Banach separation.

theorem OAI.ReflexiveFixedPoints.weakSpaceT2Space line 28
Source documentation
Continuous linear functionals separate points of the actual weak space.
```
theorem weakSpaceT2Space : T2Space (WeakSpace ℝ X) := by
…
```
theorem OAI.ReflexiveFixedPoints.weakCarrierT2Space line 38
Source documentation
The separate weak carrier inherits Hausdorffness from the weak space.
```
theorem weakCarrierT2Space (K : Set X) : T2Space (WeakCarrier K) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier

theorem OAI.ReflexiveFixedPoints.isClosed_toWeakSpace_image_of_closed_convex line 43

Source documentation

Norm-closed convex sets are closed in the actual weak topology.

theorem isClosed_toWeakSpace_image_of_closed_convex {K : Set X}
    (hclosed : IsClosed K) (hconvex : Convex ℝ K) :
    IsClosed ((toWeakSpace ℝ X) '' K) := by
…

theorem OAI.ReflexiveFixedPoints.weaklyClosed_of_closed_convex line 49
theorem OAI.ReflexiveFixedPoints.weaklyClosed_closedBall line 54
Source documentation
Every norm closed ball is weakly closed, including an empty ball.
```
theorem weaklyClosed_closedBall (x : X) (r : ℝ) :
    WeaklyClosed (closedBall x r) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyClosed
def OAI.ReflexiveFixedPoints.bidualIsometryEquiv line 58
def OAI.ReflexiveFixedPoints.weakBidualInverse line 62
theorem OAI.ReflexiveFixedPoints.weakBidualInverse_eval line 66
theorem OAI.ReflexiveFixedPoints.continuous_weakBidualInverse line 73
theorem OAI.ReflexiveFixedPoints.weakBidualInverse_image_closedBall line 81
theorem OAI.ReflexiveFixedPoints.weaklyCompact_closedBall_zero line 106
Source documentation
Canonical bidual surjectivity implies weak compactness of every ball. No completeness or nontriviality assumption is needed for this implication.
```
theorem weaklyCompact_closedBall_zero (hX : CanonicallyReflexive X) (r : ℝ) :
    WeaklyCompact (closedBall (0 : X) r) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive, OAI.ReflexiveFixedPoints.WeaklyCompact
theorem OAI.ReflexiveFixedPoints.weaklyCompact_of_closed_bounded_convex line 116
Source documentation
Every norm-closed bounded convex set in a canonically reflexive space is weakly compact in the topology generated by its continuous dual.
```
theorem weaklyCompact_of_closed_bounded_convex (hX : CanonicallyReflexive X)
    {K : Set X} (hclosed : IsClosed K) (hbounded : Bornology.IsBounded K)
    (hconvex : Convex ℝ K) : WeaklyCompact K := by
…
```
Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive, OAI.ReflexiveFixedPoints.WeaklyCompact
theorem OAI.ReflexiveFixedPoints.weaklyCompact_closedBall line 123

theorem OAI.ReflexiveFixedPoints.weakCarrier_set_eq_image line 129

Source documentation

The weak carrier really is the subtype of the weak image.

theorem weakCarrier_set_eq_image (K : Set X) :
    {x : WeakSpace ℝ X | (toWeakSpace ℝ X).symm x ∈ K} =
      (toWeakSpace ℝ X) '' K := by
…

theorem OAI.ReflexiveFixedPoints.WeaklyCompact.compactSpace line 140
Source documentation
Transfer actual ambient weak compactness to the separate weak carrier.
```
theorem WeaklyCompact.compactSpace {K : Set X} (hK : WeaklyCompact K) :
    CompactSpace (WeakCarrier K) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.WeakCarrier
theorem OAI.ReflexiveFixedPoints.differenceBall_eq_inter line 147
theorem OAI.ReflexiveFixedPoints.isClosed_differenceBall line 153
theorem OAI.ReflexiveFixedPoints.isBounded_differenceBall line 157
theorem OAI.ReflexiveFixedPoints.convex_differenceBall line 161
theorem OAI.ReflexiveFixedPoints.weaklyCompact_differenceBall line 166
Source documentation
Weak compactness of the entire unit ball of the closed difference span.
```
theorem weaklyCompact_differenceBall (hX : CanonicallyReflexive X) (K : Set X) :
    WeaklyCompact (differenceBall K) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive, OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.differenceBall