SequenceQuotientVolume.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Quotient log boxes in the chosen Haar normalization

The quotient Jacobian and the packing argument use the same Haar measure. Uniqueness of Haar measure transfers the exponential cube formula to that normalization, including along an arbitrary sequence of profile scales.

theorem OAI.PolycyclicRecognition.haar_model_cube_volume line 26

Source documentation

The logarithmic cube formula for any actual Lie-algebra model and any Haar normalization. The constant is independent of the cube radius.

theorem haar_model_cube_volume
    (haar : NilpotentExponentialHaarInput E Q)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) Q) (hnil : LieRing.IsNilpotent L)
    {n : ℕ} (b : Basis (Fin n) ℝ L) (μ : Measure Q) [μ.IsHaarMeasure] :
    ∃ c : ℝ≥0, 0 < c ∧ ∀ R : ℝ, 0 ≤ R →
      μ (exponentialCoordinateBox (Exp ∘ e) b R) =
        (c : ℝ≥0∞) * ENNReal.ofReal (2 * R) ^ n := by
…

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

theorem OAI.PolycyclicRecognition.haar_model_sequence_boxes line 65

Source documentation

Subexponential radii have finite, subexponential Haar volume in the normalization already used for the quotient action.

theorem haar_model_sequence_boxes
    (haar : NilpotentExponentialHaarInput E Q)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) Q) (hnil : LieRing.IsNilpotent L)
    {n : ℕ} (b : Basis (Fin n) ℝ L) (μ : Measure Q) [μ.IsHaarMeasure]
    (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hR0 : ∀ j, 0 ≤ R j) (hR : HasSubexponentialUpperBoundSeq scale R) :
    (∀ j, μ (exponentialCoordinateBox (Exp ∘ e) b (R j)) ≠ ⊤) ∧
      HasSubexponentialUpperBoundSeq scale (fun j =>
        (μ (exponentialCoordinateBox (Exp ∘ e) b (R j))).toReal) := by
…

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