NilpotentBallVolume.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial volume upper bounds for nilpotent metric balls

Linear bounded-step chains, the finite Dynkin formula and exponential Haar coordinates give the only volume estimate used by boundary averaging.

theorem OAI.PolycyclicRecognition.boundedHeightChain_of_sequence line 22

Source documentation

A finite sequence with controlled vertices and steps gives the inductive chain used by the coordinate estimates.

theorem boundedHeightChain_of_sequence
    {X W : Type*} [MetricSpace X] [NormedAddCommGroup W]
    (π : X → W) (p : ℕ → X) {L M : ℝ} (n : ℕ)
    (hheight : ∀ i ≤ n, ‖π (p i)‖ ≤ M)
    (hstep : ∀ i < n, dist (p i) (p (i + 1)) ≤ L) :
    BoundedHeightChain π L M n (p 0) (p n) := by
…

Mentions: OAI.PolycyclicRecognition.BoundedHeightChain

theorem OAI.PolycyclicRecognition.exists_polynomial_ball_coordinate_bound line 43

Source documentation

Every large metric ball is contained in one polynomially growing exponential coordinate cube.

theorem exists_polynomial_ball_coordinate_bound
    (chains : LinearMetricChains G)
    (dynkin : NilpotentDynkinExpansionInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    {c : ℕ} (hzero : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)
      (GroupLieAlgebra (𝓘(ℝ, E)) G) c = ⊥)
    {J : Type*} [Fintype J] (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ R : ℝ, 1 ≤ R →
      ball (1 : G) R ⊆ exponentialCoordinateBox Exp b (D * R ^ c) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.exists_haar_polynomial_ball_volume line 79

Source documentation

The concrete exponential Haar measure has polynomial ball-volume upper growth. The exponent need not be the sharp homogeneous dimension.

theorem exists_haar_polynomial_ball_volume
    (chains : LinearMetricChains G)
    (dynkin : NilpotentDynkinExpansionInput E G)
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G)) :
    ∃ (μ : Measure G) (C : ℝ) (d : ℕ), μ.IsHaarMeasure ∧ 0 ≤ C ∧
      ∀ R : ℝ, 1 ≤ R → (μ (ball 1 R)).toReal ≤ C * R ^ d := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput

theorem OAI.PolycyclicRecognition.haar_polynomial_ball_volume line 108

Source documentation

Haar normalization only changes the polynomial coefficient.

theorem haar_polynomial_ball_volume
    [SecondCountableTopology G]
    (chains : LinearMetricChains G)
    (dynkin : NilpotentDynkinExpansionInput E G)
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    (μ : Measure G) [μ.IsHaarMeasure] :
    ∃ C : ℝ, 0 ≤ C ∧ ∃ d : ℕ,
      ∀ R : ℝ, 1 ≤ R → (μ (ball 1 R)).toReal ≤ C * R ^ d := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput