PolynomialBallScales.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Good closed-ball scales for nilpotent Haar measure

Polynomial upper growth alone supplies a sequence of compact balls tending to infinity with bounded tripling ratio. No lower growth asymptotic is used.

theorem OAI.PolycyclicRecognition.closedBall_measureReal_pos line 24

theorem OAI.PolycyclicRecognition.closedBall_polynomial_bound line 33

Source documentation

Convert the open-ball polynomial estimate to closed balls.

theorem closedBall_polynomial_bound {C : ℝ} {d : ℕ}
    (h : ∀ r : ℝ, 1 ≤ r → μ.real (ball 1 r) ≤ C * r ^ d) :
    ∀ r : ℝ, 1 ≤ r → μ.real (closedBall 1 r) ≤ (C * 2 ^ d) * r ^ d := by
…

theorem OAI.PolycyclicRecognition.exists_closedBall_tripling_scales line 46

Source documentation

Choose good radii cofinally, retaining the exact closed-ball ratio.

theorem exists_closedBall_tripling_scales {C : ℝ} {d : ℕ}
    (h : ∀ r : ℝ, 1 ≤ r → μ.real (ball 1 r) ≤ C * r ^ d) :
    ∃ scale : ℕ → ℝ,
      (∀ n, 1 ≤ scale n) ∧ Tendsto scale atTop atTop ∧
      ∀ n, μ.real (closedBall 1 (3 * scale n)) ≤
        (2 * (3 : ℝ) ^ d) * μ.real (closedBall 1 (scale n)) := by
…

theorem OAI.PolycyclicRecognition.exists_closedBall_tripling_scales_above line 62

Source documentation

The good radii may all be chosen above any fixed lower threshold.

theorem exists_closedBall_tripling_scales_above {C : ℝ} {d : ℕ}
    (h : ∀ r : ℝ, 1 ≤ r → μ.real (ball 1 r) ≤ C * r ^ d) (R : ℝ) :
    ∃ scale : ℕ → ℝ,
      (∀ n, max R 1 ≤ scale n) ∧ Tendsto scale atTop atTop ∧
      ∀ n, μ.real (closedBall 1 (3 * scale n)) ≤
        (2 * (3 : ℝ) ^ d) * μ.real (closedBall 1 (scale n)) := by
…

theorem OAI.PolycyclicRecognition.nilpotent_closedBall_tripling_scales line 86

Source documentation

The nilpotent Dynkin and Haar constructions provide all growth inputs for the good scales used in the Cartan semidirect cover.

theorem nilpotent_closedBall_tripling_scales
    (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)) :
    ∃ (scale : ℕ → ℝ) (D : ℝ), (∀ n, 1 ≤ scale n) ∧
      Tendsto scale atTop atTop ∧ 0 ≤ D ∧
      ∀ n, μ.real (closedBall 1 (3 * scale n)) ≤ D * μ.real (closedBall 1 (scale n)) := by
…

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

theorem OAI.PolycyclicRecognition.nilpotent_closedBall_tripling_scales_above line 99