OAI/GroupTheory/PolycyclicRecognition/Algebra/JointDirectionLabels.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint transport of direction labels in both flow times

Keeping both times as coordinates turns the horizontal flows into measure-preserving skew products. This supplies local convergence in measure on triples directly, including compact sets that are not product sets.

  1. def OAI.PolycyclicRecognition.pairTimeMeasure line 24
  2. instance OAI.PolycyclicRecognition.(instance at line 26) line 26
  3. instance OAI.PolycyclicRecognition.(instance at line 28) line 28
  4. def OAI.PolycyclicRecognition.timedRightTranslation line 33
  5. theorem OAI.PolycyclicRecognition.continuous_timedRightTranslation line 38
  6. theorem OAI.PolycyclicRecognition.measurePreserving_timedRightTranslation line 50
  7. theorem OAI.PolycyclicRecognition.finiteLabel_jointDirections_relation line 63

    Source documentation

    A finite relation true locally on triples for nearby directions remains true at the limiting direction. Compact carriers are built from the actual convergent sequence and the two continuous skew products.

    theorem finiteLabel_jointDirections_relation
    {L : Type*} [Fintype L] [MeasurableSpace L] [MeasurableSingletonClass L]
    (μ : Measure G) [μ.IsHaarMeasure] [μ.IsMulRightInvariant]
    (Exp : V → G) (hExp : Continuous Exp) (label : G → L) (hlabel : Measurable label)
    (v : ℕ → V) {v₀ : V} (hv : Tendsto v atTop (𝓝 v₀))
    (K : Set ((ℝ × ℝ) × G)) (hK : IsCompact K) (R : L → L → Prop)
    (hR : ∀ᶠ n in atTop, ∀ᵐ z ∂(pairTimeMeasure.prod μ).restrict K,
      R (label (z.2 * Exp (z.1.1 • v n))) (label (z.2 * Exp (z.1.2 • v n)))) :
    ∀ᵐ z ∂(pairTimeMeasure.prod μ).restrict K,
      R (label (z.2 * Exp (z.1.1 • v₀))) (label (z.2 * Exp (z.1.2 • v₀))) := by
…