TailMaps.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Resolvent tail families

The outer resolvent in every tail map gives a uniform approximate fixed point bound. Convex hulls are taken in the ambient vector space of maps. Precomposition is linear on that vector space; only this linear operation is distributed over convex combinations.

def OAI.ReflexiveFixedPoints.tailFamily line 28
Source documentation
Tail maps retain their actual outer resolvent and generated inner map.
```
def tailFamily (m : ℕ) : Set (K → K) :=
…
```
theorem OAI.ReflexiveFixedPoints.tailFamily_nonempty line 33
theorem OAI.ReflexiveFixedPoints.tailFamily_generated line 38
theorem OAI.ReflexiveFixedPoints.tailFamily_antitone line 44
theorem OAI.ReflexiveFixedPoints.tailFamily_nonexpansive line 49
theorem OAI.ReflexiveFixedPoints.tailFamily_defect_le line 55
theorem OAI.ReflexiveFixedPoints.tailFamily_precomp line 68
Source documentation
Appending any generated map on the input side retains the same tail.
```
theorem tailFamily_precomp {m : ℕ} {h g : K → K}
    (hh : h ∈ tailFamily hKclosed hKconvex T hT m)
    (hg : Generated hKclosed hKconvex T hT g) :
    h ∘ g ∈ tailFamily hKclosed hKconvex T hT m := by
…
```
Mentions: OAI.ReflexiveFixedPoints.tailFamily, OAI.ReflexiveFixedPoints.Generated
def OAI.ReflexiveFixedPoints.ambientTailFamily line 76
Source documentation
Tail maps represented in the actual vector space of ambient-valued maps.
```
def ambientTailFamily (m : ℕ) : Set (K → X) :=
…
```
def OAI.ReflexiveFixedPoints.ambientTailConvexHull line 80
Source documentation
The algebraic convex hull, before pointwise weak closure is taken.
```
def ambientTailConvexHull (m : ℕ) : Set (K → X) :=
…
```
theorem OAI.ReflexiveFixedPoints.ambientTailFamily_nonempty line 83
theorem OAI.ReflexiveFixedPoints.ambientTailFamily_antitone line 87
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_nonempty line 92
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_antitone line 96
theorem OAI.ReflexiveFixedPoints.convex_ambientTailConvexHull line 101
theorem OAI.ReflexiveFixedPoints.ambientTailFamily_subset_generated line 105
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_subset_generated line 111
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_representative line 118
Source documentation
Every element of the ambient convex hull is a genuine generated selfmap.
```
theorem ambientTailConvexHull_representative {m : ℕ} {f : K → X}
    (hf : f ∈ ambientTailConvexHull hKclosed hKconvex T hT m) :
    ∃ g : K → K, Generated hKclosed hKconvex T hT g ∧ ambientMap g = f :=
…
```
Mentions: OAI.ReflexiveFixedPoints.ambientTailConvexHull, OAI.ReflexiveFixedPoints.Generated, OAI.ReflexiveFixedPoints.ambientMap
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_mapsTo line 123
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_nonexpansive line 130
def OAI.ReflexiveFixedPoints.precompLinear line 140
Source documentation
Precomposition by a fixed selfmap is a linear map on ambient-valued maps.
```
def precompLinear (g : K → K) : (K → X) →ₗ[ℝ] (K → X) where
…
```
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_precomp line 145
theorem OAI.ReflexiveFixedPoints.ambientTailConvexHull_comp line 160
Source documentation
Composition closure follows from linear precomposition, without a continuity or affinity assumption on the nonlinear maps.
```
theorem ambientTailConvexHull_comp {m : ℕ} {f g : K → K}
    (hf : ambientMap f ∈ ambientTailConvexHull hKclosed hKconvex T hT m)
    (hg : ambientMap g ∈ ambientTailConvexHull hKclosed hKconvex T hT m) :
    ambientMap (f ∘ g) ∈ ambientTailConvexHull hKclosed hKconvex T hT m := by
…
```
Mentions: OAI.ReflexiveFixedPoints.ambientMap, OAI.ReflexiveFixedPoints.ambientTailConvexHull