HaarBoxRadius.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact radius ratios for every normalization of nilpotent Haar measure

theorem OAI.PolycyclicRecognition.haar_exponential_box_radius line 23

Source documentation

Dilating a coordinate box by a scalar changes its Haar volume by the scalar to the dimension, independently of the exponential scaling basis.

theorem haar_exponential_box_radius
    (haarInput : NilpotentExponentialHaarInput E G)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G) (hnil : LieRing.IsNilpotent L)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    {n : ℕ} (b₀ b : Basis (Fin n) ℝ L) (μ : Measure G) [μ.IsHaarMeasure]
    {R : ℝ} (hR : 0 ≤ R) :
    μ (exponentialCoordinateBox (Exp ∘ e) b R) =
      ENNReal.ofReal R ^ n * μ (exponentialCoordinateBox (Exp ∘ e) b 1) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.haar_exponential_box_radius_real line 45