CartanRayFactorContraction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compact increments and contraction for the actual Cartan factors

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_compact_factor_quotient_orbit line 25

Source documentation

Compact ambient increments have compact quotient images. This uses compact lifts of the actual factors, so no continuity of an arbitrarily chosen factorization or permutation-valued action is assumed.

theorem exists_compact_factor_quotient_orbit
    {Q : Type*} [Group Q] [TopologicalSpace Q]
    (π : F.N.carrier →* Q) (hπ : Continuous π)
    (α : F.D.carrier →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ u d q, act (F.inclusionN u * F.inclusionD d) q = π u * α d q)
    {K : Set G} (hK : IsCompact K) :
    ∃ C : Set Q, IsCompact C ∧ ∀ g ∈ K, act g 1 ∈ C := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.factor_quotient_action_eq_exponential line 59
Source documentation
The quotient action of each actual Cartan factor is the exponential of its induced Lie action, with the actual Cartan logarithm.
```
theorem factor_quotient_action_eq_exponential (d : F.D.carrier) (q : Q.carrier) :
    α d q = exponentialConjugate Q.equiv ExpQ hbijQ
      (M.coneAdjointAutomorphism T (positiveWeightRay α₀) (positiveWeightRay_add α₀)
        (cartanLog H F.D.equiv F.ExpD hbijD d)) q := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialConjugate, OAI.PolycyclicRecognition.positiveWeightRay, OAI.PolycyclicRecognition.positiveWeightRay_add, OAI.PolycyclicRecognition.cartanLog

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ray_factor_compact_contraction line 93

Source documentation

The contraction estimate is expressed directly in a basis of the actual tangent algebra and in the actual Cartan factor coordinates.

theorem exists_ray_factor_compact_contraction :
    ∃ (b : Basis
        (Fin (finrank ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α₀))))
        ℝ (GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier)) (p : ℕ) (rate : ℝ),
      0 < rate ∧ ∀ K : Set Q.carrier, IsCompact K → ∃ A : ℝ, 0 ≤ A ∧
        ∀ d : F.D.carrier,
          α₀ (cartanLog H F.D.equiv F.ExpD hbijD d) ≤ 0 → ∀ q ∈ K,
          ‖b.equivFun (chartQ.symm (α d q))‖ ≤
            A * (1 + ‖(finBasis ℝ H).equivFun
              (cartanLog H F.D.equiv F.ExpD hbijD d)‖) ^ p *
              Real.exp (rate * α₀ (cartanLog H F.D.equiv F.ExpD hbijD d)) := by
…

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