NormalizedExponentialLaws.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compact normalized exponential-coordinate groups

The defining equations retain both the exact group law and its adjoint conjugation formula. All of these equations hold in the actual rescalings and survive passage to a limit.

def OAI.PolycyclicRecognition.normalizedExponentialParameters line 21
theorem OAI.PolycyclicRecognition.isCompact_normalizedExponentialParameters line 27

theorem OAI.PolycyclicRecognition.exists_rescaledExponentialData_bound line 41

Source documentation

Actual rescalings satisfy all the closed equations used in the limiting endpoint-map argument. No limiting-group assertion is an external input.

theorem exists_rescaledExponentialData_bound (X : I → L) {k : ℕ}
    (hk : LieModule.lowerCentralSeries ℝ L L k = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    (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))
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (hmatch : ∀ x, ρ (Exp x) = algebraExpUnit (j x)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (s : I → ℝ)
…

Mentions: OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.algebraExpUnit