WeakSelfMap.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Selfmaps with the topology of pointwise weak convergence

The domain remains the norm subtype. The codomain is the separate weak carrier, so the function space has exactly the product weak topology. Composition converts the inner value back to a domain point algebraically.

abbrev OAI.ReflexiveFixedPoints.WeakSelfMap line 26
Source documentation
Actual selfmaps of K, with pointwise weak topology on their values.
```
abbrev WeakSelfMap (K : Set X) := K → WeakCarrier K
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier
def OAI.ReflexiveFixedPoints.WeakSelfMap.ofNorm line 32
def OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm line 34
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm_ofNorm line 36
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.ofNorm_toNorm line 40
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm_injective line 44
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.ofNorm_injective line 48
def OAI.ReflexiveFixedPoints.WeakSelfMap.weakAmbient line 53
Source documentation
Pointwise weak values in their ambient vector space.
```
def weakAmbient (f : WeakSelfMap K) : K → WeakSpace ℝ X := fun a => f a
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap
def OAI.ReflexiveFixedPoints.WeakSelfMap.normAmbient line 56
Source documentation
The same actual values in the original normed space.
```
def normAmbient (f : WeakSelfMap K) : K → X := fun a => (toNorm f a : X)
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.weakAmbient_injective line 58
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.continuous_weakAmbient line 63
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.continuous_normToWeak line 66
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.continuous_ofNorm line 70
Source documentation
Norm-pointwise convergence implies weak-pointwise convergence.
```
theorem continuous_ofNorm : Continuous (ofNorm (K := K)) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap.ofNorm
def OAI.ReflexiveFixedPoints.WeakSelfMap.comp line 74
Source documentation
Composition is actual composition of the underlying norm selfmaps.
```
def comp (f g : WeakSelfMap K) : WeakSelfMap K := fun a => f (toNorm g a)
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.toNorm_comp line 76
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.ofNorm_comp line 79
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.comp_assoc line 84
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.continuous_comp_right line 88
Source documentation
Only the right argument is fixed. The inner map need not be weakly continuous.
```
theorem continuous_comp_right (g : WeakSelfMap K) :
    Continuous (fun f : WeakSelfMap K => comp f g) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakSelfMap, OAI.ReflexiveFixedPoints.WeakSelfMap.comp
def OAI.ReflexiveFixedPoints.WeakSelfMap.weakify line 93
Source documentation
Coordinatewise algebraic change from norm values to weak values.
```
def weakify : (K → X) ≃ₗ[ℝ] (K → WeakSpace ℝ X) :=
…
```
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.weakify_apply line 96
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.weakAmbient_ofNorm line 99
theorem OAI.ReflexiveFixedPoints.WeakSelfMap.convex_weakAmbient_image_ofNorm line 102