CartanHeightRays.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual Cartan representatives of height rays

The height is exactly linear along these rays. Continuity on one compact ball and the one-parameter group identity give their linear metric growth.

def OAI.PolycyclicRecognition.CartanFactorModel.heightRay line 32
Source documentation
The Cartan one-parameter ray representing the height t • w.
```
def heightRay (w : W) (t : ℝ) : F.D.carrier :=
…
```
theorem OAI.PolycyclicRecognition.CartanFactorModel.heightRay_zero line 36

theorem OAI.PolycyclicRecognition.CartanFactorModel.heightRay_height line 41

Source documentation

These are actual ambient height rays, with no coordinate approximation.

theorem heightRay_height (height : G →* Multiplicative W)
    (hheight : ∀ x, (height (ExpG x)).toAdd = eW (heightProjection T.character x))
    (w : W) (t : ℝ) :
    (height (F.inclusionD (F.heightRay T eW w t))).toAdd = t • w := by
…

Mentions: OAI.PolycyclicRecognition.heightProjection

theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_heightRay_metric_bound line 52

Source documentation

One metric coefficient works for all directions. The cost of direction w is its norm in the chosen finite-dimensional height space.

theorem exists_heightRay_metric_bound [IsIsometricSMul G G]
    (chartD : GroupLieAlgebra (𝓘(ℝ, F.D.modelSpace)) F.D.carrier ≃ₜ F.D.carrier)
    (hchartD : ∀ x, chartD x = F.ExpD x) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (w : W) (t : ℝ),
      dist 1 (F.inclusionD (F.heightRay T eW w t)) ≤ C * (1 + |t| * ‖w‖) := by
…

theorem OAI.PolycyclicRecognition.CartanFactorModel.sublinear_error_on_heightRays line 78

Source documentation

A sublinear height error restricts to the actual Cartan exponential rays. The resulting threshold may depend on the direction and the map.

theorem sublinear_error_on_heightRays [IsIsometricSMul G G]
    (chartD : GroupLieAlgebra (𝓘(ℝ, F.D.modelSpace)) F.D.carrier ≃ₜ F.D.carrier)
    (hchartD : ∀ x, chartD x = F.ExpD x)
    (height : G →* Multiplicative W)
    (hheight : ∀ x, (height (ExpG x)).toAdd = eW (heightProjection T.character x))
    {P : Type*} (η : P → G → W) (A : P → W →ₗ[ℝ] W)
    (hsub : ∀ p ε, 0 < ε → ∃ B : ℝ, ∀ g,
      ‖η p g - η p 1 - A p (height g).toAdd‖ ≤ ε * dist 1 g + B) :
    ∀ p w ε, 0 < ε → ∃ R : ℝ, ∀ t, R ≤ t → 0 ≤ t →
      ‖(η p (F.inclusionD (F.heightRay T eW w t)) - η p 1) - t • A p w‖ ≤ ε * t := by
…

Mentions: OAI.PolycyclicRecognition.heightProjection