RescaledProfiles.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Equicontinuity of actual rescaled map profiles

def OAI.PolycyclicRecognition.rescaledMapProfile line 19
Source documentation
The map profile on an exponential chart, centered at x with suffix k.
```
def rescaledMapProfile (J : G → W) (x k : G) (r : ℝ) (φ : Z → G) (z : Z) : W :=
…
```
theorem OAI.PolycyclicRecognition.rescaledMapProfile_dist_le line 22

theorem OAI.PolycyclicRecognition.continuous_rescaledMapProfile line 42

Source documentation

Continuity at each fixed scale is inherited from the actual chart.

theorem continuous_rescaledMapProfile {J : G → W} (hJ : Continuous J)
    (x k : G) (r : ℝ) {φ : Z → G} (hφ : Continuous φ)
    [IsTopologicalGroup G] : Continuous (rescaledMapProfile J x k r φ) := by
…

Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

theorem OAI.PolycyclicRecognition.equicontinuous_rescaled_profiles line 53

Source documentation

Uniformly Lipschitz maps, arbitrary centers, and arbitrary suffixes have equicontinuous rescaled profiles once their normalized group charts have the proved sublinear-distance property. No bound on the centers is required.

theorem equicontinuous_rescaled_profiles
    (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
    (hweight : ∀ i j k, b.repr ⁅b i, b j⁆ k ≠ 0 → cost i + cost j ≤ cost k)
    (Exp : L → G) (hinj : Function.Injective Exp) (hzero : Exp 0 = 1)
    (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    {C : ℝ} (hC : 0 ≤ C)
    (hmetric : ∀ r : ℝ, 0 ≤ r → ∀ v : L,
      ‖(exponentialRescaleBasis b cost r).equivFun v‖ ≤ 1 →
        dist 1 (Exp v) ≤ C * Real.exp r)
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.exponentialRescaleBasis