TailMapSemigroup.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The compact semigroup supplied by the actual resolvent tails

The ambient convex hull of each resolvent tail consists of genuine generated selfmaps. Changing their values to the weak carrier therefore gives a convex, composition-closed family of nonexpansive selfmaps. The decreasing sequence of their pointwise weak closures has an actual idempotent.

def OAI.ReflexiveFixedPoints.weakTailConvexFamily line 32
Source documentation
Actual selfmaps whose ambient representatives belong to the algebraic convex hull of the resolvent tail. The ambient function space is used for convexity, and the weak selfmap space is used for topology.
```
def weakTailConvexFamily (m : ℕ) : Set (WeakSelfMap K) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap
theorem OAI.ReflexiveFixedPoints.weakAmbient_image_weakTailConvexFamily line 38
Source documentation
Every point of the ambient convex hull has an actual selfmap representative, so passing to weak values loses no elements.
```
theorem weakAmbient_image_weakTailConvexFamily (m : ℕ) :
    WeakSelfMap.weakAmbient '' weakTailConvexFamily hKclosed hKconvex T hT m =
      WeakSelfMap.weakify '' ambientTailConvexHull hKclosed hKconvex T hT m := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap.weakAmbient, OAI.ReflexiveFixedPoints.weakTailConvexFamily, OAI.ReflexiveFixedPoints.WeakSelfMap.weakify, OAI.ReflexiveFixedPoints.ambientTailConvexHull
theorem OAI.ReflexiveFixedPoints.weakTailConvexFamily_nonempty line 60
theorem OAI.ReflexiveFixedPoints.weakTailConvexFamily_antitone line 71
theorem OAI.ReflexiveFixedPoints.convex_weakTailConvexFamily line 76
theorem OAI.ReflexiveFixedPoints.weakTailConvexFamily_generated line 86
Source documentation
A member is generated by the actual identity, resolvents, composition, and finite convex operations.
```
theorem weakTailConvexFamily_generated {m : ℕ} {f : WeakSelfMap K}
    (hf : f ∈ weakTailConvexFamily hKclosed hKconvex T hT m) :
    Generated hKclosed hKconvex T hT (WeakSelfMap.toNorm f) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.weakTailConvexFamily, OAI.ReflexiveFixedPoints.Generated, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm
theorem OAI.ReflexiveFixedPoints.weakTailConvexFamily_nonexpansive line 92
theorem OAI.ReflexiveFixedPoints.weakTailConvexFamily_comp line 99
Source documentation
Composition closure is inherited from actual tail maps. No nonlinear map is distributed over a convex combination in its input.
```
theorem weakTailConvexFamily_comp {m : ℕ} {f g : WeakSelfMap K}
    (hf : f ∈ weakTailConvexFamily hKclosed hKconvex T hT m)
    (hg : g ∈ weakTailConvexFamily hKclosed hKconvex T hT m) :
    WeakSelfMap.comp f g ∈ weakTailConvexFamily hKclosed hKconvex T hT m := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.weakTailConvexFamily, OAI.ReflexiveFixedPoints.WeakSelfMap.comp
theorem OAI.ReflexiveFixedPoints.exists_idempotent_in_tail_closures line 111
Source documentation
An idempotent in every positive tail closure. Compactness and Hausdorffness are properties of the actual weak carrier supplied by the weak-compactness foundations.
```
theorem exists_idempotent_in_tail_closures
    [CompactSpace (WeakCarrier K)] [T2Space (WeakCarrier K)] :
    ∃ P ∈ ⋂ n, closure (weakTailConvexFamily hKclosed hKconvex T hT (n + 1)),
      WeakSelfMap.comp P P = P ∧ LipschitzWith 1 (WeakSelfMap.toNorm P) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier, OAI.ReflexiveFixedPoints.weakTailConvexFamily, OAI.ReflexiveFixedPoints.WeakSelfMap.comp, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm