Reduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Full reduction of an original-norm counterexample

Starting from the given map, this producer constructs the separable minimal invariant set, scales its points and conjugates its map in the same ambient space, and proves the weak compactness and metrizability conclusions. In particular the compact ball is the entire unit ball of the closed linear span of the differences; compactness of the minimal set alone would not supply that conclusion.

theorem OAI.ReflexiveFixedPoints.exists_normalizedMinimalData_of_counterexample line 29
Source documentation
A genuine original-norm fixed-point-free map produces all normalized minimal invariant data used by the anchor and switching constructions.
```
theorem exists_normalizedMinimalData_of_counterexample
    (hX : CanonicallyReflexive X) {C : Set X}
    (hne : C.Nonempty) (hclosed : IsClosed C)
    (hbounded : Bornology.IsBounded C) (hconvex : Convex ℝ C)
    (F : C → C) (hF : LipschitzWith 1 F) (hno : ∀ x : C, F x ≠ x) :
    Nonempty (NormalizedMinimalData (X := X)) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.CanonicallyReflexive, OAI.ReflexiveFixedPoints.NormalizedMinimalData