CompactDetector.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One functional detecting an entire norm-compact set

The diameter theorem first gives a uniform defect threshold at each fixed point. A finite net and its equal-weight barycenter then give a single norming functional which detects every point of a norm-compact set.

theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.uniform_diametral line 36
Source documentation
At a fixed point of the minimal set, sufficiently small fixed-point defect forces the distance to be arbitrarily close to the diameter.
```
theorem uniform_diametral (D : NormalizedMinimalData (X := X)) (a : D.K)
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData
theorem OAI.ReflexiveFixedPoints.NormalizedMinimalData.compact_detector line 61
Source documentation
Every sufficiently accurate approximate fixed point has one continuous linear functional detecting its distance from every point of a prescribed nonempty norm-compact subset of the minimal set.
```
theorem compact_detector (D : NormalizedMinimalData (X := X))
…
```
Mentions: OAI.ReflexiveFixedPoints.NormalizedMinimalData