RescaledChartDistances.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Metric convergence for pairs of rescaled chart points

theorem OAI.PolycyclicRecognition.exp_chart_difference line 22
Source documentation
The coordinate of a quotient of exponential-chart points is the exact Dynkin product. This identity transfers polynomial convergence to distance.
```
theorem exp_chart_difference (b : Basis (Fin n) ℝ L)
    (Exp : L → G) (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (x y : Fin n → ℝ) :
    Exp (b.equivFun.symm (dynkinProduct a (basisBracket b) (-x) y)) =
      (Exp (b.equivFun.symm x))⁻¹ * Exp (b.equivFun.symm y) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket

theorem OAI.PolycyclicRecognition.rescaled_chart_distance_tendsto_zero line 35

Source documentation

If two normalized chart points approach the same point, their distance in the original group, divided by the dilation, tends to zero.

theorem rescaled_chart_distance_tendsto_zero
    (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