GeneratedMaps.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

The finitely generated family of nonexpansive selfmaps

The family consists of actual maps of the norm subtype. Its constructors are identity, resolvents, composition, and binary convex combinations. Its image in the ambient module of maps to X is convex, and the finite convex-combination theorem below proves closure under every finite family. Thus the binary presentation also gives closure under finite convex combinations. All displacement constants are proved from the derivation.

def OAI.ReflexiveFixedPoints.ambientMap line 28
Source documentation
The ambient representative of an actual selfmap.
```
def ambientMap (g : K → K) : K → X := fun a => g a
```
theorem OAI.ReflexiveFixedPoints.ambientMap_apply line 30
theorem OAI.ReflexiveFixedPoints.ambientMap_injective line 34
def OAI.ReflexiveFixedPoints.convexMix line 42
Source documentation
A binary convex combination, with membership proved in the ambient space.
```
def convexMix (hKconvex : Convex ℝ K) (f g : K → K)
    (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : K → K :=
…
```
theorem OAI.ReflexiveFixedPoints.convexMix_val line 47
theorem OAI.ReflexiveFixedPoints.convexMix_nonexpansive line 52
theorem OAI.ReflexiveFixedPoints.convexMix_displacement line 83

theorem OAI.ReflexiveFixedPoints.convexMix_comp_right line 111

Source documentation

Right composition is precomposition of the pointwise combination.

theorem convexMix_comp_right (hKconvex : Convex ℝ K) (f g k : K → K)
    (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    convexMix hKconvex f g a b ha hb hab ∘ k =
      convexMix hKconvex (f ∘ k) (g ∘ k) a b ha hb hab := rfl

Mentions: OAI.ReflexiveFixedPoints.convexMix

def OAI.ReflexiveFixedPoints.convexCombination line 117

Source documentation

An actual finite pointwise convex combination, for arbitrary finite index universes.

def convexCombination (hKconvex : Convex ℝ K) {ι : Type v} [Fintype ι]
    (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (hsum : ∑ i, w i = 1)
    (g : ι → K → K) : K → K :=
…

theorem OAI.ReflexiveFixedPoints.convexCombination_val line 123
theorem OAI.ReflexiveFixedPoints.ambientMap_convexCombination line 129
theorem OAI.ReflexiveFixedPoints.convexCombination_comp_right line 137

inductive OAI.ReflexiveFixedPoints.Generated line 146

Source documentation

The actual family generated using finitely many constructors.

inductive Generated (hKclosed : IsClosed K) (hKconvex : Convex ℝ K)
    (T : K → K) (hT : LipschitzWith 1 T) : (K → K) → Prop where
…

theorem OAI.ReflexiveFixedPoints.generated_nonexpansive line 163

theorem OAI.ReflexiveFixedPoints.generated_displacement line 173

Source documentation

Every generated map has a finite nonnegative displacement constant.

theorem generated_displacement {g : K → K}
    (hg : Generated hKclosed hKconvex T hT g) :
    ∃ c : ℝ, 0 ≤ c ∧ ∀ a : K,
      ‖(g a : X) - (a : X)‖ ≤ c * ‖(T a : X) - (a : X)‖ := by
…

Mentions: OAI.ReflexiveFixedPoints.Generated

def OAI.ReflexiveFixedPoints.ambientGenerated line 208
Source documentation
The ambient function-space image of the generated actual selfmaps.
```
def ambientGenerated (hKclosed : IsClosed K) (hKconvex : Convex ℝ K)
    (T : K → K) (hT : LipschitzWith 1 T) : Set (K → X) :=
…
```
theorem OAI.ReflexiveFixedPoints.ambientMap_mem_ambientGenerated line 212
theorem OAI.ReflexiveFixedPoints.generated_of_ambient_mem line 216
theorem OAI.ReflexiveFixedPoints.ambientMap_mem_ambientGenerated_iff line 223
theorem OAI.ReflexiveFixedPoints.convex_ambientGenerated line 228
theorem OAI.ReflexiveFixedPoints.convexHull_subset_ambientGenerated line 235

theorem OAI.ReflexiveFixedPoints.generated_convexCombination line 241

Source documentation

Binary generation is closed under every finite pointwise convex combination.

theorem generated_convexCombination {ι : Type v} [Fintype ι]
    (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (hsum : ∑ i, w i = 1)
    (g : ι → K → K) (hg : ∀ i, Generated hKclosed hKconvex T hT (g i)) :
    Generated hKclosed hKconvex T hT (convexCombination hKconvex w hw hsum g) := by
…

Mentions: OAI.ReflexiveFixedPoints.Generated, OAI.ReflexiveFixedPoints.convexCombination