Basic.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Actual norm and weak carriers for the fixed point argument

The public reflexivity predicate uses the continuous bidual. All maps on convex sets use their norm subtypes. Weak convergence takes place on a separate subtype of WeakSpace, so it cannot alter the given norm. The data structures record conclusions of the reduction from actual fixed-point-free counterexamples.

abbrev OAI.ReflexiveFixedPoints.WeakCarrier line 29
Source documentation
The weak carrier is distinct from the norm subtype K.
```
abbrev WeakCarrier (K : Set X) :=
…
```
def OAI.ReflexiveFixedPoints.normToWeak line 33
Source documentation
Change only the carrier; both representatives denote the same point.
```
def normToWeak (K : Set X) : K ≃ WeakCarrier K where
…
```
Mentions: OAI.ReflexiveFixedPoints.WeakCarrier
theorem OAI.ReflexiveFixedPoints.normToWeak_val line 39
theorem OAI.ReflexiveFixedPoints.normToWeak_symm_val line 42
def OAI.ReflexiveFixedPoints.WeaklyCompact line 46
Source documentation
Actual weak compactness in the ambient weak topology.
```
def WeaklyCompact (K : Set X) : Prop :=
…
```
def OAI.ReflexiveFixedPoints.WeaklyClosed line 50
Source documentation
Actual weak closedness in the ambient weak topology.
```
def WeaklyClosed (K : Set X) : Prop :=
…
```
def OAI.ReflexiveFixedPoints.differenceSpan line 54
Source documentation
The norm-closed linear span of the actual differences.
```
def differenceSpan (K : Set X) : Submodule ℝ X :=
…
```
def OAI.ReflexiveFixedPoints.differenceBall line 58
Source documentation
The entire closed unit ball of the difference span, viewed in X.
```
def differenceBall (K : Set X) : Set X :=
…
```
def OAI.ReflexiveFixedPoints.InvariantSubset line 62
Source documentation
Invariance for an ambient subset under a map of the norm subtype.
```
def InvariantSubset (K : Set X) (T : K → K) (s : Set X) : Prop :=
…
```
def OAI.ReflexiveFixedPoints.MinimalInvariant line 66
Source documentation
Minimality concerns genuine norm-closed convex invariant subsets.
```
def MinimalInvariant (K : Set X) (T : K → K) : Prop :=
…
```
structure OAI.ReflexiveFixedPoints.MinimalInvariantData line 71
Source documentation
Structural conclusions obtained from a genuine fixed-point-free map.
```
structure MinimalInvariantData where
…
```
structure OAI.ReflexiveFixedPoints.NormalizedMinimalData line 86
Source documentation
The normalized reduction data, still in the original ambient norm. The normalization producer uses an actual scalar homothety of the set.
```
structure NormalizedMinimalData extends MinimalInvariantData (X := X) where
…
```
Mentions: OAI.ReflexiveFixedPoints.MinimalInvariantData
instance OAI.ReflexiveFixedPoints.MinimalInvariantData.(instance at line 95) line 95
instance OAI.ReflexiveFixedPoints.MinimalInvariantData.(instance at line 97) line 97
instance OAI.ReflexiveFixedPoints.NormalizedMinimalData.(instance at line 104) line 104
instance OAI.ReflexiveFixedPoints.NormalizedMinimalData.(instance at line 106) line 106
theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.norm_sub_le_one line 110
Source documentation
Every pair of points is at distance at most the normalized diameter.
```
theorem norm_sub_le_one (D : NormalizedMinimalData (X := X)) (x y : D.K) :
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData