RightTranslationLabel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Chamber relations pass to limiting horizontal directions

The compact carrier is constructed from the actual convergent multipliers. For right translations in a unimodular group, finite measurable labels then inherit every almost-everywhere relation satisfied before the limit.

def OAI.PolycyclicRecognition.rightTranslationMap line 25
theorem OAI.PolycyclicRecognition.continuous_rightTranslationMap line 27
theorem OAI.PolycyclicRecognition.finiteLabel_rightTranslations_relation line 34

theorem OAI.PolycyclicRecognition.finiteLabel_horizontalDirections_relation line 61

Source documentation

Applying the translation result to Exp (s • v) gives the exact fixed time flow comparison required when generic vectors approach an extremal ray.

theorem finiteLabel_horizontalDirections_relation
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (μ : Measure G) [μ.IsHaarMeasure] [μ.IsMulRightInvariant] [Measure.InnerRegular μ]
    (Exp : V → G) (hExp : Continuous Exp)
    (label : G → I) (hlabel : Measurable label)
    (v : ℕ → V) {v₀ : V} (hv : Tendsto v atTop (𝓝 v₀))
    (s t : ℝ) (K : Set G) (hK : IsCompact K) (R : I → I → Prop)
    (hR : ∀ᶠ n in atTop, ∀ᵐ x ∂μ.restrict K,
      R (label (x * Exp (s • v n))) (label (x * Exp (t • v n)))) :
    ∀ᵐ x ∂μ.restrict K,
      R (label (x * Exp (s • v₀))) (label (x * Exp (t • v₀))) := by
…