CartanSheetAgreement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Supported Cartan sheets agree above an interior generator switch

theorem OAI.PolycyclicRecognition.rescaledMapProfile_suffix_dist_le line 17

Source documentation

At a fixed chart point, changing the suffix changes the profile by at most the normalized distance between the two right-positioned sheets.

theorem rescaledMapProfile_suffix_dist_le
    {G W V : Type*} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    [NormedAddCommGroup W] [NormedSpace ℝ W]
    {L : ℝ≥0} {J : G → W} (hJ : LipschitzWith L J)
    (x k l : G) (r : ℝ) (φ : V → G) (z : V) :
    dist (rescaledMapProfile J x k r φ z) (rescaledMapProfile J x l r φ z) ≤
      (L : ℝ) * (dist (k * φ z) (l * φ z) / Real.exp r) := by
…

Mentions: OAI.PolycyclicRecognition.rescaledMapProfile

theorem OAI.PolycyclicRecognition.CartanWordModel.supported_switch_profiles_agree line 48
Source documentation
Every supported joint limit of two actual sheets separated by a strictly interior root switch agrees at the given chart point.
```
theorem supported_switch_profiles_agree
    (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput