OAI/GroupTheory/PolycyclicRecognition/Algebra/ModelDensityOccupation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.model_density_occupation_error_tendsto_zero line 19

   Source documentation

   For the independent chart law, every fixed move in the positively weighted second nilpotent factor has vanishing translated-observable error. All coordinate invariance and limiting assertions are derived from the actual exponential and the published Haar input.

   theorem model_density_occupation_error_tendsto_zero
       {E D L I A Y G ι : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       [FiniteDimensional ℝ E] [TopologicalSpace D] [ChartedSpace E D] [Group D]
       [LieGroup (𝓘(ℝ, E)) ⊤ D] [T2Space D] [SimplyConnectedSpace D]
       [MeasurableSpace D] [BorelSpace D] [LieRing L] [LieAlgebra ℝ L]
       [Fintype I] [DecidableEq I] [MeasurableSpace A]
       [TopologicalSpace Y] [CompactSpace Y] [MeasurableSpace Y] [BorelSpace Y]
       [SMul G Y] [ContinuousConstSMul G Y]
       (haar : NilpotentExponentialHaarInput E D)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) D → D) (hExp : IsGroupExponential Exp)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) D)
       (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) D))
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput