PairLabelFunctions.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous uniformly bounded label-distance observables

theorem OAI.PolycyclicRecognition.continuous_pair_label_distance line 21
Source documentation
For each fixed scale the observable is continuous on the compact pair section.
```
theorem continuous_pair_label_distance
    (π : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (g : G) (r : ℝ) (S : Set W) :
    Continuous (fun p : NormalizedPair G Λ => infDist (r⁻¹ • pairHeight π g p) S) :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight

theorem OAI.PolycyclicRecognition.pair_label_distance_le line 30

Source documentation

Linear growth of the sampled group element gives a common bound at all scales at least one, using any fixed member of the comparison set.

theorem pair_label_distance_le
    (π : G →* Multiplicative W)
    (hπ : LipschitzWith K (fun g => (π g).toAdd))
    {g : G} {r R : ℝ} (hr : 1 ≤ r) (_hR : 0 ≤ R) (hg : dist 1 g ≤ R * r)
    {S : Set W} {w : W} (hw : w ∈ S) (p : NormalizedPair G Λ) :
    infDist (r⁻¹ • pairHeight π g p) S ≤ (K : ℝ) * Λ * R + ‖w‖ := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight