FiniteCovolumeLattice.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-covolume lattice formulation

Mostow's uniformity theorem is used only for a lattice in the original connected solvable Lie group: Mostow (1962), Theorem 6.2, as stated in Geng, When are radicals of Lie groups lattice-hereditary?, NYJM 21 (2015), Theorem 2.9(i), p.325. No recognition conclusion is part of this input.

def OAI.PolycyclicRecognition.IsFiniteCovolumeLattice line 20
Source documentation
A discrete subgroup with finite covolume, expressed by the normalized invariant measure on the coset space.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:106 (same declaration text).
```
def IsFiniteCovolumeLattice {G : Type} [Group G] [TopologicalSpace G]
    (Λ : Subgroup G) : Prop :=
…
```
def OAI.PolycyclicRecognition.MostowSolvableLatticeUniformInput line 27
Source documentation
The connected-solvable specialization of Mostow's uniformity theorem.
```
def MostowSolvableLatticeUniformInput : Prop :=
…
```
theorem OAI.PolycyclicRecognition.lattice_recognition_of_published_inputs line 33
Source documentation
Corollary lattice-recognition, including finite-covolume lattices in the hypothesis and allowing the ambient Lie group to change.
```
theorem lattice_recognition_of_published_inputs
    (inputs : PublishedRecognitionInputs) (mostow : MostowSolvableLatticeUniformInput)
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsFiniteCovolumeLattice Λ)
    {J : Type} [Group J] [Group.FG J] (e : GroupCoarseEquivalence Λ J) :
    ∃ Γ : Subgroup J, Γ.FiniteIndex ∧
      ∃ (R : SimplyConnectedSolvableLieModel) (Δ : Subgroup R.carrier),
        IsUniformLattice Δ ∧ Nonempty (Γ ≃* Δ) :=
…
```
Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.MostowSolvableLatticeUniformInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsFiniteCovolumeLattice, OAI.PolycyclicRecognition.GroupCoarseEquivalence