OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportedCellOccupation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.supported_model_cell_occupation_error_tendsto_zero line 16

   Source documentation

   The small first-factor move need only be uniform where the second coordinate is sampled. No estimate outside that full-measure set is used.

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

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput