OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryVolumeAveraging.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.BoundaryVolumeComparison.averaged_trace line 27

   Source documentation

   No metric or doubling condition on the boundary is assumed: the existing published metric input and nilpotent exponential inputs supply them.

   theorem BoundaryVolumeComparison.averaged_trace [SFinite C.targetMeasure]
       (metricInput : GeodesicMetricExistenceInput)
       (dynkin : NilpotentDynkinExpansionInput ES S)
       (haar : NilpotentExponentialHaarInput ES S)
       (Exp : GroupLieAlgebra (𝓘(ℝ, ES)) S → S) (hExp : IsGroupExponential Exp)
       (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, ES)) S))
       (hcont : ∀ x, Continuous (actS x))
       (ι : N →* G) (π : N →* S) (hπ : Function.Surjective π)
       (hact : ∀ n x, actS (ι n) x = π n * x)
       (d : D → G) {L : ℝ}
       (hleaf : ∀ p n j,
         |C.targetRate * αT (height (f p (ι n * d j))).toAdd -
   …

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