RootFlow.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic distortion in Cartan root spaces

Generalized root spaces determine the nilpotent correction to the scalar weight action. A compatible group conjugation identity then gives logarithmic distortion.

def OAI.PolycyclicRecognition.rootCoordinates line 26
Source documentation
Fixed linear coordinates put a compatible norm on the root space.
```
def rootCoordinates : (rootSpace H χ) ≃ₗ[ℝ]
    (Fin (Module.finrank ℝ (rootSpace H χ)) → ℝ) :=
…
```
def OAI.PolycyclicRecognition.rootAction line 41
Source documentation
The actual adjoint action on a Cartan generalized root space.
```
def rootAction (h : H) : (rootSpace H χ) →L[ℝ] (rootSpace H χ) :=
…
```
theorem OAI.PolycyclicRecognition.rootAction_nilpotent_correction line 44
theorem OAI.PolycyclicRecognition.exists_contracting_root_direction line 54
Source documentation
Each nonzero real root has a direction where its value is -1.
```
theorem exists_contracting_root_direction (hχ : χ.IsNonZero) :
    ∃ h : H, χ h = -1 := by
…
```

theorem OAI.PolycyclicRecognition.root_logarithmic_distortion line 68

Source documentation

Logarithmic distortion follows for an integrated nonzero root chart. No semisimplicity or diagonal adjoint action is assumed.

theorem root_logarithmic_distortion
    {G : Type*} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    (Exp : (rootSpace H χ) → G) (hExp : Continuous Exp)
    (h : H) (hh : χ h = -1)
    (d : ℝ → G) (hd : Continuous d) (hd0 : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t)
    (hconj : ∀ v t, 0 ≤ t → Exp v =
      d t * Exp ((NormedSpace.exp (t • rootAction H χ h)) v) * (d t)⁻¹) :
    ∃ D : ℝ, 0 < D ∧ ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖) := by
…

Mentions: OAI.PolycyclicRecognition.rootAction