ConditionalBoundedHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounded height in a fixed metric and an arbitrary norm

The auxiliary Riemannian metric is used only to construct smoothing. The identity comparison transfers every uniformly controlled family from the specified proper chain metric. A bounded linear change of coordinates then returns the estimate to the specified norm on the canonical height space.

def OAI.PolycyclicRecognition.ModelIsUnimodular line 30
Source documentation
Unimodularity of the actual Lie model, using its canonical Borel Haar measure.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:192 (same declaration text).
```
def ModelIsUnimodular (R : SimplyConnectedSolvableLieModel) : Prop :=
…
```
Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel

theorem OAI.PolycyclicRecognition.uniform_bounded_height line 43

Source documentation

The standalone uniform bounded-height theorem. In particular the fixed metric can be any left-invariant proper Riemannian metric. The finite group is chosen before the quasi-isometry constants, and the bound is uniform over all self quasi-isometries with those constants.

theorem uniform_bounded_height
    (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier)
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier) a)
    (huni : ModelIsUnimodular R)
    {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    (Exp : GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier → R.carrier)
    (hExp : IsGroupExponential Exp) (π : R.carrier →* Multiplicative W)
    (hπExp : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :
    letI := d.compatibleMetric
…

Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric, OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.ModelIsUnimodular, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection

theorem OAI.PolycyclicRecognition.uniform_bounded_height_of_published_inputs line 150

Source documentation

Compatibility form of the height theorem; its published-input argument is no longer needed.

theorem uniform_bounded_height_of_published_inputs
    (_inputs : PublishedRecognitionInputs)
    (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier)
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier) a)
    (huni : ModelIsUnimodular R)
    {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    (Exp : GroupLieAlgebra (𝓘(ℝ, R.modelSpace)) R.carrier → R.carrier)
    (hExp : IsGroupExponential Exp) (π : R.carrier →* Multiplicative W)
    (hπExp : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :
    letI := d.compatibleMetric
…

Mentions: OAI.PolycyclicRecognition.PublishedRecognitionInputs, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric, OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.ModelIsUnimodular, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection