noncomputable def HomogeneousDynamics.SL3Z : Subgroup (Matrix.SpecialLinearGroup (Fin 3) ℝ)

The arithmetic lattice $SL(3, \mathbb{Z})$ viewed as a subgroup of $SL(3, \mathbb{R})$ via the canonical embedding.

noncomputable def HomogeneousDynamics.unipotentU (t : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The unipotent matrix $U(t) = \begin{pmatrix} 1 & t & t^2 \\ 0 & 1 & t \\ 0 & 0 & 1 \end{pmatrix}$ parameterizing the one-parameter unipotent subgroup of $SL(3, \mathbb{R})$ used in Lindenstrauss–Mohammadi–Wang–Yang.

theorem HomogeneousDynamics.unipotentU_det (t : ℝ) : (unipotentU t).det = 1

The unipotent matrix $U(t)$ has determinant $1$.

noncomputable def HomogeneousDynamics.unipotentElem (t : ℝ) : Matrix.SpecialLinearGroup (Fin 3) ℝ

The unipotent element $U(t)$ packaged as an element of $SL(3, \mathbb{R})$ using the determinant computation.

def HomogeneousDynamics.IsEpsDense {X : Type u_1} [PseudoMetricSpace X] (S : Set X) (ε : ℝ) : Prop

A subset S of a pseudometric space is ε-dense if every point lies within distance ε of some element of S.

noncomputable def HomogeneousDynamics.orbitSegment (x : Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z) (T : ℝ) : Set (Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z)

The orbit segment $\{U(t) \cdot x : t \in [0, T]\}$ of a point $x$ in the homogeneous space $SL(3,\mathbb{R}) / SL(3,\mathbb{Z})$ under the unipotent flow.

structure HomogeneousDynamics.ProperHomogeneousSubspace [TopologicalSpace (Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z)] : Type

A proper homogeneous subspace of $SL(3,\mathbb{R}) / SL(3,\mathbb{Z})$: a closed proper subset invariant under a nontrivial proper subgroup of $SL(3,\mathbb{R})$. These are the exceptional sets near which the unipotent orbit can fail to equidistribute.

• carrier : Set (Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z)
• isClosed : IsClosed self.carrier
• isProper : self.carrier ≠ Set.univ
• isSubgroupInvariant : ∃ (H : Subgroup (Matrix.SpecialLinearGroup (Fin 3) ℝ)), H ≠ ⊤ ∧ ∀ h ∈ H, ∀ y ∈ self.carrier, h • y ∈ self.carrier

def HomogeneousDynamics.IsOrbitFarFromProperHomogeneous [PseudoMetricSpace (Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z)] (x : Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z) (η : ℝ) : Prop

The unipotent orbit closure of x stays at distance at least η from every proper homogeneous subspace; the diophantine condition under which LMWY proves polynomial density of the orbit.

theorem HomogeneousDynamics.lmwy_quantitative_density [PseudoMetricSpace (Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z)] : ∃ c > 0, ∀ (x : Matrix.SpecialLinearGroup (Fin 3) ℝ ⧸ SL3Z), ∀ η > 0, IsOrbitFarFromProperHomogeneous x η → ∀ T > 0, IsEpsDense (orbitSegment x T) (T ^ (-c))

Lindenstrauss–Mohammadi–Wang–Yang quantitative density: there exists $c > 0$ such that for every $x \in SL(3,\mathbb{R}) / SL(3,\mathbb{Z})$ whose unipotent orbit is $\eta$-far from every proper homogeneous subspace, the orbit segment $\{U(t) \cdot x : t \in [0,T]\}$ is $T^{-c}$-dense for every $T > 0$.