OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryAveragedTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The transversal trace bound from actual boundary maps and leaf bounds

  1. theorem OAI.PolycyclicRecognition.boundary_averaged_transversal_trace line 24

    Source documentation

    Boundary image masses and the leaf-height estimate imply a uniform transversal trace comparison. The actual homeomorphisms supply the measures; the nilpotent exponential inputs discharge all metric-volume obligations.

    theorem boundary_averaged_transversal_trace
    (chains : LinearMetricChains S)
    (dynkin : NilpotentDynkinExpansionInput ES S)
    (haar : NilpotentExponentialHaarInput ES S)
    (Exp : GroupLieAlgebra (𝓘(ℝ, ES)) S → S) (hExp : IsGroupExponential Exp)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, ES)) S))
    (ΞS : Measure S) [ΞS.IsHaarMeasure] (ΞT : Measure T) [SFinite ΞT]
    (act : G →* Equiv.Perm S) (hcont : ∀ x, Continuous (act x))
    (Îđ : N →* G) (π : N →* S) (hπ : Function.Surjective π)
    (hact : ∀ n x, act (Îđ n) x = π n * x)
    (B : P → S ≃ₜ T) (f : P → G → G) (height : G → ℝ)
    (d : D → G) (source : D → ℝ) (U : Set S) (hU : IsCompact U)
â€Ķ

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