OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryPublishedMetricAveraging.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The published proper chain metric discharges the averaging metric

  1. theorem OAI.PolycyclicRecognition.boundary_averaged_trace_of_published_metric line 23

    Source documentation

    Only the existing proper chain metric input is needed on this connected nilpotent quotient; its topology is preserved before applying averaging.

    theorem boundary_averaged_trace_of_published_metric
    (metricInput : GeodesicMetricExistenceInput)
    (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.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput