NilpotentChainPacking.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial packing of nilpotent chains

The logarithmic endpoint estimate and exponential-coordinate Haar formula supply actual finite polynomial bounds on separated chains. Only the precise published nilpotent exponential inputs are used.

theorem OAI.PolycyclicRecognition.exists_card_coefficient_of_haar_volume line 27

Source documentation

A fixed positive ball mass converts a real volume coefficient into a natural cardinal coefficient, uniformly in the scale.

theorem exists_card_coefficient_of_haar_volume
    (μ : Measure G) [μ.IsHaarMeasure] {r F : ℝ} (hr : 0 < r)
    (b : ℕ) (region : ℕ → Set G)
    (hvol : ∀ n, μ (region n) ≤ ENNReal.ofReal F * (1 + (n : ℝ≥0∞)) ^ b) :
    ∃ C : ℕ, ∀ (n : ℕ) (s : Finset G),
      (∀ x ∈ s, ∀ y ∈ s, x ≠ y → r + r ≤ dist x y) →
      (∀ x ∈ s, ball x r ⊆ region n) → s.card ≤ C * (1 + n) ^ b := by
…

theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_nilpotent_exponential line 58
Source documentation
Nilpotent chains satisfy the required finite polynomial packing property. This applies to any height map, since the estimate uses just the steps.
```
theorem polynomialBoundedChainPacking_of_nilpotent_exponential
    (dynkin : NilpotentDynkinExpansionInput E G)
    (haarInput : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {W : Type*} [NormedAddCommGroup W] (π : G → W) :
    PolynomialBoundedChainPacking π := by
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking