Anchor.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual anchor of the resolvent tail families

The tail-limit set is an intersection of closures in the weak carrier. Its points are then viewed in the original normed space. The idempotent constructed from the actual resolvents fixes the selected anchor, and compactness plus separation gives the required norm-convex-hull property.

def OAI.ReflexiveFixedPoints.weakCarrierPoint line 30
Source documentation
Underlying original-norm point of a weak carrier element. No weak-to-norm continuity assertion is made.
```
def weakCarrierPoint (w : WeakCarrier K) : X := (toWeakSpace ℝ X).symm w
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier
def OAI.ReflexiveFixedPoints.anchorTailClosure line 33
Source documentation
The closure of the (n+1)st tail image, in the weak subtype topology.
```
def anchorTailClosure (H : ℕ → Set (K → K)) (x : K) (n : ℕ) :
    Set (WeakCarrier K) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier
def OAI.ReflexiveFixedPoints.anchorTailSet line 38
Source documentation
The literal tail-limit set, viewed in the original ambient space.
```
def anchorTailSet (H : ℕ → Set (K → K)) (x : K) : Set X :=
…
```
theorem OAI.ReflexiveFixedPoints.anchorTailSet_subset line 41
theorem OAI.ReflexiveFixedPoints.anchorTailSet_mem_tailClosure line 46
structure OAI.ReflexiveFixedPoints.AnchorPoint line 62
Source documentation
This record states actual output properties. Its tail-set equality retains the concrete intersection definition used to construct it.
```
structure AnchorPoint (H : ℕ → Set (K → K)) where
…
```
theorem OAI.ReflexiveFixedPoints.subtype_val_image_iInter line 74
theorem OAI.ReflexiveFixedPoints.norm_preimage_subtype_image line 88
theorem OAI.ReflexiveFixedPoints.evaluated_tail_hull_mem line 106
theorem OAI.ReflexiveFixedPoints.anchor_mem_closedConvexHull_each line 122
theorem OAI.ReflexiveFixedPoints.exists_anchorPoint line 146
Source documentation
Construct the actual anchor and its literal tail-limit set from the resolvents. No approximation, semigroup, or convex-hull law is assumed.
```
theorem exists_anchorPoint (hKnonempty : K.Nonempty)
    (hKweak : WeaklyCompact K) :
    Nonempty (AnchorPoint (tailFamily hKclosed hKconvex T hT)) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.AnchorPoint, OAI.ReflexiveFixedPoints.tailFamily