CartanLogRegionVolume.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Cartan log restriction has subexponential Haar volume

theorem OAI.PolycyclicRecognition.cartan_log_regions_volume line 24

Source documentation

The coordinate restriction produced by the actual path lifts is an exponential box. Its volume is finite and subexponential in any Haar normalization, with no separate volume hypothesis.

theorem cartan_log_regions_volume
    (haar : NilpotentExponentialHaarInput E D)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) D → D) (hExp : IsGroupExponential Exp)
    (e : H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) D) (hbij : Function.Bijective Exp)
    (μ : Measure D) [μ.IsHaarMeasure]
    (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R) :
    let B := fun n => {d : D | ‖(finBasis ℝ H).equivFun (cartanLog H e Exp hbij d)‖ ≤ R n}
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq, OAI.PolycyclicRecognition.cartanLog