CompactPairs.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Compact sections of Lipschitz quasi-inverse pairs

The space consists of actual continuous maps, with the compact-open topology. Uniform Lipschitz bounds and a bound at one point give compactness in a proper target. The quasi-inverse conditions are closed, including their compositions.

theorem OAI.PolycyclicRecognition.isCompact_lipschitz_family line 25
Source documentation
The compact family of maps with a common Lipschitz constant and a common bound at one point.
```
theorem isCompact_lipschitz_family (K : ℝ≥0) (a : X) (b : Y) (R : ℝ) :
    IsCompact {f : C(X, Y) | LipschitzWith K f ∧ dist (f a) b ≤ R} := by
…
```
def OAI.PolycyclicRecognition.LipschitzPairBounds line 55
Source documentation
Uniform Lipschitz, lower-distance, and two-sided quasi-inverse bounds. The source manuscript uses the same constant in these four bounds.
```
def LipschitzPairBounds (Λ : ℝ≥0) (p : C(G, G) × C(G, G)) : Prop :=
…
```
def OAI.PolycyclicRecognition.normalizedPairs line 63
Source documentation
The first normalized section: the forward map sends the identity to itself.
```
def normalizedPairs (Λ : ℝ≥0) : Set (C(G, G) × C(G, G)) :=
…
```
theorem OAI.PolycyclicRecognition.isClosed_lipschitzPairBounds line 67
theorem OAI.PolycyclicRecognition.isClosed_normalizedPairs line 90
theorem OAI.PolycyclicRecognition.isCompact_normalizedPairs line 96
Source documentation
Both maps are anchored on the normalized section: the inverse anchor bound follows from its quasi-inverse bound and the forward normalization.
```
theorem isCompact_normalizedPairs (Λ : ℝ≥0) : IsCompact (normalizedPairs G Λ) := by
…
```
Mentions: OAI.PolycyclicRecognition.normalizedPairs
abbrev OAI.PolycyclicRecognition.NormalizedPair line 106
Source documentation
Actual normalized pairs, carrying their compact-open topology.
```
abbrev NormalizedPair (Λ : ℝ≥0) := normalizedPairs G Λ
```
Mentions: OAI.PolycyclicRecognition.normalizedPairs
instance OAI.PolycyclicRecognition.(instance at line 108) line 108