RayGroupContraction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic contraction of the actual quotient-group action

The Lie-coordinate estimate is transported through the actual bijective exponential. Compact subsets have bounded logarithmic coordinates. The action is the exponential conjugate already identified with the descended Cartan action in ConeQuotientHaarAction.

def OAI.PolycyclicRecognition.exponentialLog line 32
Source documentation
The logarithm in a specified Lie-algebra realization of a bijective group exponential.
```
def exponentialLog : G → V :=
…
```
theorem OAI.PolycyclicRecognition.exponentialLog_exp line 35
theorem OAI.PolycyclicRecognition.exp_exponentialLog line 39
theorem OAI.PolycyclicRecognition.exponentialLog_conjugate line 45
Source documentation
Conjugation through the exponential acts on its logarithm by the specified Lie automorphism, exactly.
```
theorem exponentialLog_conjugate (F : V ≃ₗ⁅ℝ⁆ V) (g : G) :
    exponentialLog e Exp hbij (exponentialConjugate e Exp hbij F g) =
      F (exponentialLog e Exp hbij g) := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialLog, OAI.PolycyclicRecognition.exponentialConjugate

theorem OAI.PolycyclicRecognition.exists_bound_exponentialLog line 53

Source documentation

Compact sets in the group have uniformly bounded logarithms in each finite coordinate basis, using the actual exponential homeomorphism.

theorem exists_bound_exponentialLog
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ v, chart v = Exp v)
    {J : Type*} [Fintype J] (b : Basis J ℝ V)
    {K : Set G} (hK : IsCompact K) :
    ∃ R : ℝ, 0 ≤ R ∧ ∀ g ∈ K, ‖b.equivFun (exponentialLog e Exp hbij g)‖ ≤ R := by
…

Mentions: OAI.PolycyclicRecognition.exponentialLog

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ray_group_compact_contraction line 80

Source documentation

Every fixed compact set of the actual ray quotient contracts at the polynomial-exponential rate in logarithmic coordinates.

theorem exists_ray_group_compact_contraction
    (α : H →ₗ[ℝ] ℝ)
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α)))
    (Exp : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
    (hbij : Function.Bijective Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier ≃ₜ Q.carrier)
    (hchart : ∀ v, chart v = Exp v) :
    ∃ (b : Basis
        (Fin (finrank ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α))))
        ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α)))
      (p : ℕ) (c : ℝ), 0 < c ∧
      ∀ K : Set Q.carrier, IsCompact K → ∃ A : ℝ, 0 ≤ A ∧
…

Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.positiveWeightRay