ExponentialProfileCells.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual Haar good sets from the independently sampled coordinate profiles

theorem OAI.PolycyclicRecognition.exists_exponential_good_profile_cells_sequence line 17

Source documentation

The slow diagonal is performed in the original coordinate probability space. Its image consists of measurable good sheets in the actual translated exponential cell, with the same subexponential relative mass.

theorem exists_exponential_good_profile_cells_sequence
    {L E N I V W : Type*} [LieRing L] [LieAlgebra ℝ L]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [TopologicalSpace N] [ChartedSpace E N] [Group N]
    [LieGroup (𝓘(ℝ, E)) ⊤ N] [T2Space N] [SimplyConnectedSpace N]
    [MeasurableSpace N] [BorelSpace N]
    [TopologicalSpace V] [NormedAddCommGroup W]
    (haar : NilpotentExponentialHaarInput E N)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) N) (hnil : LieRing.IsNilpotent L)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) N → N) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) N ≃ₜ N) (hchart : ∀ x, chart x = Exp x)
    (X : I → L) (words : Finset (FreeMagma I))
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput