# Weak mixing of triangular billiards with an irrational angle

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Ergodicity of triangular billiards with an irrational angle](../../preprints/Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026/Ergodicity-of-triangular-billiards-with-an-irrational-angle-September-25-2026.pdf)

## Scope

The formalization proves that the unit-speed billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to $\pi$ is ergodic for normalized area times uniform angular measure. It constructs the flow outside the null set of exceptional trajectories, proves uniqueness of the flight chain there, and establishes measure preservation and the flow law almost everywhere. No genericity or Diophantine condition on the irrational angle is assumed.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Ergodicity of triangular billiards with an irrational angle | [IrrationalTriangleBilliard.lean](../ComparatorChallenges/IrrationalTriangleBilliard.lean) |