OAI/GroupTheory/PolycyclicRecognition/Algebra/RecognitionFromPairRepresentatives.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_pair_representatives line 16

   Source documentation

   This bridge applies the proved normalized height estimate to actual transferred maps once their uniformly close Lipschitz representatives are constructed. Representative existence remains a separate obligation.

   theorem recognition_and_lattice_of_pair_representatives
       (dekimpe : DekimpeLatticeRealizationInput)
       (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
       (liPD : LiDualityInput) (bieri : BieriDualityInput)
       {P J : Type} [Group P] [Group J] [MetricSpace P] [MetricSpace J]
       [IsIsometricSMul P P] [IsIsometricSMul J J] [Group.FG P] [Group.FG J]
       [DiscreteTopology J] [ProperSpace J]
       [MeasurableSpace J] [BorelSpace J] [MeasurableMul J]
       (e : MetricQuasiEquivalence P J) (hP : IsVirtuallyPolycyclic P)
       (hPfinite : ∀ R : ℝ, (Metric.closedBall (1 : P) R).Finite)
       {E G : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
       [MetricSpace G] [ChartedSpace E G] [Group G] [LieGroup (𝓘(ℝ, E)) ⊤ G]
   …

   Mentions: OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput, OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.MetricQuasiEquivalence