RootRepresentation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Root distortion in a faithful integrated representation

The conjugation identity is proved from a Lie homomorphism into a normed algebra and the ordinary exponential matching identities. It is not an additional geometric hypothesis.

def OAI.PolycyclicRecognition.representedRootVector line 27
theorem OAI.PolycyclicRecognition.representedRootVector_intertwines line 33
theorem OAI.PolycyclicRecognition.represented_root_flow line 42
Source documentation
The restricted root action exponentiates to actual matrix conjugation.
```
theorem represented_root_flow (h : H) (t : ℝ) (v : rootSpace H χ) :
    representedRootVector H χ j ((NormedSpace.exp (t • rootAction H χ h)) v) =
      NormedSpace.exp (t • j h) * j v * NormedSpace.exp (-(t • j h)) := by
…
```
Mentions: OAI.PolycyclicRecognition.representedRootVector, OAI.PolycyclicRecognition.rootAction
theorem OAI.PolycyclicRecognition.represented_root_exp_conjugation line 52
theorem OAI.PolycyclicRecognition.represented_root_exp_inverse_conjugation line 60

theorem OAI.PolycyclicRecognition.represented_root_logarithmic_distortion line 70

Source documentation

In an integrated faithful representation, logarithmic root distortion requires only the exponential matching data.

theorem represented_root_logarithmic_distortion
    {G : Type*} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (Exp : (rootSpace H χ) → G) (hExp : Continuous Exp)
    (h : H) (hh : χ h = -1) (d : ℝ → G) (hd : Continuous d)
    (hExpρ : ∀ v, ρ (Exp v) = algebraExpUnit (j v))
    (hdρ : ∀ t, ρ (d t) = algebraExpUnit (-(t • j h))) :
    ∃ D : ℝ, 0 < D ∧ ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖) := by
…

Mentions: OAI.PolycyclicRecognition.algebraExpUnit

theorem OAI.PolycyclicRecognition.embedded_root_logarithmic_distortion line 98

Source documentation

Compatibility of the representation with the group topology supplies the chart continuity as well as the conjugation and one-parameter laws.

theorem embedded_root_logarithmic_distortion
    {G : Type*} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    (ρ : G →* Aˣ) (hρ : Topology.IsEmbedding ρ)
    (Exp : (rootSpace H χ) → G) (h : H) (hh : χ h = -1) (d : ℝ → G)
    (hExpρ : ∀ v, ρ (Exp v) = algebraExpUnit (j v))
    (hdρ : ∀ t, ρ (d t) = algebraExpUnit (-(t • j h))) :
    ∃ D : ℝ, 0 < D ∧ ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖) := by
…

Mentions: OAI.PolycyclicRecognition.algebraExpUnit