CompactMapSemigroup.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Compact semigroups of nonexpansive selfmaps

Convexity converts pointwise weak closure into finite simultaneous norm approximation. This justifies composition of limits without asserting weak continuity of an arbitrary nonlinear map. Fixed right translations are continuous and the compact semigroup theorem then gives an idempotent.

def OAI.ReflexiveFixedPoints.WeakSelfMap.ConvexFamily line 33
Source documentation
Convexity of an actual map family is measured in its ambient function vector space. The subtype of points of K need not be a vector space.
```
def ConvexFamily (B : Set (WeakSelfMap K)) : Prop :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.exists_finite_norm_approx line 37
Source documentation
One actual member approximates at all the chosen arguments.
```
theorem exists_finite_norm_approx {B : Set (WeakSelfMap K)}
    (hB : ConvexFamily B) {h : WeakSelfMap K} (hh : h ∈ closure B)
    {ι : Type v} [Fintype ι] (a : ι → K) {ε : ℝ} (hε : 0 < ε) :
    ∃ g ∈ B, ∀ i, dist (toNorm g (a i)) (toNorm h (a i)) < ε := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.ConvexFamily, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.exists_finset_norm_approx line 50
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.nonexpansive_of_mem_closure line 60
Source documentation
Nonexpansiveness passes to pointwise weak closure of a convex family.
```
theorem nonexpansive_of_mem_closure {B : Set (WeakSelfMap K)}
    (hB : ConvexFamily B)
    (hLip : ∀ g ∈ B, LipschitzWith 1 (toNorm g))
    {h : WeakSelfMap K} (hh : h ∈ closure B) :
    LipschitzWith 1 (toNorm h) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.ConvexFamily, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.mem_closure_of_finite_norm_approx line 86
Source documentation
Finite norm approximations suffice for membership in weak closure.
```
theorem mem_closure_of_finite_norm_approx {B : Set (WeakSelfMap K)}
    {h : WeakSelfMap K}
    (happrox : ∀ (s : Finset K) (ε : ℝ), 0 < ε →
      ∃ g ∈ B, ∀ a ∈ s, dist (toNorm g a) (toNorm h a) < ε) :
    h ∈ closure B := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.comp_mem_closure line 104
Source documentation
The closure is composition-closed using two finite simultaneous approximations, both evaluated at arguments fixed before approximation.
```
theorem comp_mem_closure {B : Set (WeakSelfMap K)}
    (hB : ConvexFamily B)
    (hLip : ∀ g ∈ B, LipschitzWith 1 (toNorm g))
    (hcomp : ∀ f ∈ B, ∀ g ∈ B, comp f g ∈ B)
    {h k : WeakSelfMap K} (hh : h ∈ closure B) (hk : k ∈ closure B) :
    comp h k ∈ closure B := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.ConvexFamily, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm, OAI.ReflexiveFixedPoints.WeakSelfMap.comp
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.exists_idempotent_in_iInter_closure line 132
Source documentation
A decreasing family of nonempty convex composition-closed families of nonexpansive maps has an idempotent in the intersection of its pointwise weak closures.
```
theorem exists_idempotent_in_iInter_closure
    [CompactSpace (WeakCarrier K)] [T2Space (WeakCarrier K)]
    (B : ℕ → Set (WeakSelfMap K))
    (hBn : ∀ n, (B n).Nonempty) (hBanti : Antitone B)
    (hBconv : ∀ n, ConvexFamily (B n))
    (hBLip : ∀ n g, g ∈ B n → LipschitzWith 1 (toNorm g))
    (hBcomp : ∀ n f, f ∈ B n → ∀ g, g ∈ B n → comp f g ∈ B n) :
    ∃ P ∈ ⋂ n, closure (B n), comp P P = P ∧ LipschitzWith 1 (toNorm P) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier, OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.ConvexFamily, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm, OAI.ReflexiveFixedPoints.WeakSelfMap.comp