RescaledDensityOccupation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Density sampling under fixed moves in actual rescaled nilpotent groups

theorem OAI.PolycyclicRecognition.model_rescaled_density_occupation_error_tendsto_zero line 22

Source documentation

A fixed right move has vanishing error in a density-weighted average, even when the bounded observable varies with scale. The coordinate laws, their inverses, Haar invariance and their small-move limit are all derived from the actual exponential and the positively weighted word basis.

theorem model_rescaled_density_occupation_error_tendsto_zero
    {E G L I ι : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [TopologicalSpace G] [ChartedSpace E G] [Group G]
    [LieGroup (𝓘(ℝ, E)) ⊤ G] [T2Space G] [SimplyConnectedSpace G]
    [MeasurableSpace G] [BorelSpace G] [LieRing L] [LieAlgebra ℝ L]
    [Fintype I] [DecidableEq I]
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (X : I → L) {k c : ℕ} (hk : lowerCentralSeries ℝ L L k = ⊥)
    (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.boundedBracketWords