ScalarNormalization.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Scalar normalization in the original norm

We move the actual invariant set by a positive scalar and conjugate its map. No norm instance is replaced. Minimality and absence of fixed points are transported by the explicit inverse scalar multiplication.

def OAI.ReflexiveFixedPoints.scaledSubtypeEquiv line 26
Source documentation
The actual homothety between a set and its nonzero scalar image.
```
def scaledSubtypeEquiv (K : Set X) (c : ℝ) (hc : c ≠ 0) : K ≃ (c • K : Set X) where
…
```
theorem OAI.ReflexiveFixedPoints.scaledSubtypeEquiv_apply line 35
theorem OAI.ReflexiveFixedPoints.scaledSubtypeEquiv_symm_apply line 38

def OAI.ReflexiveFixedPoints.scaledMap line 43

Source documentation

Conjugate an actual selfmap by the scalar bijection.

def scaledMap (K : Set X) (T : K → K) (c : ℝ) (hc : c ≠ 0) :
    (c • K : Set X) → (c • K : Set X) :=
…

theorem OAI.ReflexiveFixedPoints.scaledMap_fixed_iff line 48
Source documentation
Fixed points pull back through the actual scalar change of variables.
```
theorem scaledMap_fixed_iff (K : Set X) (T : K → K) (c : ℝ) (hc : c ≠ 0)
    (y : (c • K : Set X)) :
    scaledMap K T c hc y = y ↔
      T ((scaledSubtypeEquiv K c hc).symm y) = (scaledSubtypeEquiv K c hc).symm y := by
…
```
Mentions: OAI.ReflexiveFixedPoints.scaledMap, OAI.ReflexiveFixedPoints.scaledSubtypeEquiv
theorem OAI.ReflexiveFixedPoints.scaledMap_nonexpansive line 61
Source documentation
Conjugation by a positive homothety preserves nonexpansiveness.
```
theorem scaledMap_nonexpansive (K : Set X) (T : K → K)
    (hT : LipschitzWith 1 T) (c : ℝ) (hc : 0 < c) :
    LipschitzWith 1 (scaledMap K T c hc.ne') := by
…
```
Mentions: OAI.ReflexiveFixedPoints.scaledMap
theorem OAI.ReflexiveFixedPoints.scaledMap_minimal line 85
Source documentation
The image under a positive homothety retains minimality.
```
theorem scaledMap_minimal (K : Set X) (T : K → K)
    (hT : MinimalInvariant K T) (c : ℝ) (hc : 0 < c) :
    MinimalInvariant (c • K) (scaledMap K T c hc.ne') := by
…
```
Mentions: OAI.ReflexiveFixedPoints.MinimalInvariant, OAI.ReflexiveFixedPoints.scaledMap
theorem OAI.ReflexiveFixedPoints.MinimalInvariantData.diam_pos line 117
Source documentation
A fixed-point-free invariant set cannot have zero diameter.
```
theorem diam_pos (D : MinimalInvariantData (X := X)) : 0 < Metric.diam D.K := by
…
```
Mentions: OAI.ReflexiveFixedPoints.MinimalInvariantData
def OAI.ReflexiveFixedPoints.MinimalInvariantData.scaled line 124
Source documentation
All structural properties survive the actual scalar homothety.
```
def scaled (D : MinimalInvariantData (X := X)) (hX : CanonicallyReflexive X)
…
```
Mentions: OAI.ReflexiveFixedPoints.MinimalInvariantData, OAI.ReflexiveFixedPoints.CanonicallyReflexive
theorem OAI.ReflexiveFixedPoints.MinimalInvariantData.scaled_inv_diam line 140
Source documentation
Diameter is exactly one after inverse-diameter scaling.
```
theorem scaled_inv_diam (D : MinimalInvariantData (X := X))
…
```
Mentions: OAI.ReflexiveFixedPoints.MinimalInvariantData