NilpotentBoundaryAveraging.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Boundary trace comparison on actual nilpotent groups

This proves the averaging step from the explicit published exponential inputs and the already chosen proper chain metric. No doubling premise is retained.

theorem OAI.PolycyclicRecognition.trace_bound_of_nilpotent_boundary_masses line 27

Source documentation

Uniform translated boundary masses determine their exponential volume characters, with a bound independent of the compact sets' diameters.

theorem trace_bound_of_nilpotent_boundary_masses
    (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) (ρ : P → Measure G) [μ.IsHaarMeasure] [∀ p, SFinite (ρ p)]
    (sets : J → Set G) (source : J → ℝ) (target : P → J → ℝ)
    (hsets : ∀ j, IsCompact (sets j)) {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
    (hvolume : ∀ j, μ (sets j) = ENNReal.ofReal (c * Real.exp (source j)))
    (hlower : ∀ p j z, ENNReal.ofReal (Real.exp (target p j)) ≤
      ENNReal.ofReal K * ρ p (leftTranslate (sets j) z))
…

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