QuotientReturn.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integral matrices from recurrence on a subgroup orbit

A late return with close subgroup parameters in the arithmetic quotient produces a conjugate integral special-linear matrix. This is the orbit recurrence step in EKL Theorem 5.1.

theorem OAI.DukePrimeDegree.exists_integral_return_of_closed_orbit line 24

Source documentation

Recurrence on a closed subgroup orbit produces integral conjugates of late flow elements multiplied by arbitrarily small subgroup elements.

theorem exists_integral_return_of_closed_orbit {n : ℕ}
    (H : Subgroup (G n)) (hH : IsClosed (H : Set (G n)))
    (μ : Measure (X n)) [IsFiniteMeasure μ] [NeZero μ]
    (x : X n) (hfull : ∀ᵐ y ∂μ, ∃ h : H, rightAction x (h : G n) = y)
    (a : G n) (hinv : μ.map (fun y => rightAction y a) = μ)
    (U : Set H) (hU : U ∈ 𝓝 1) (N : ℕ) :
    ∃ m > N, ∃ h : H, h ∈ U ∧ ∃ q : G n,
      ∃ γ : Matrix.SpecialLinearGroup (Fin n) ℤ,
        q⁻¹ * (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) γ) * q =
          a ^ m * (h : G n) := by
…