The Poincaré recurrence theorem
ProvedFamousTheorems.ae_mem_imp_frequently_image_memThe Poincar\u00e9 recurrence theorem. For a measure-preserving transformation of a finite measure space, almost every point of a measurable set returns to that set infinitely often. Volume preservation plus finite total volume forces recurrence: the iterated images cannot all be disjoint, so points must come back. The conclusion is striking physically — a closed mechanical system returns arbitrarily close to its initial state, seemingly at odds with thermodynamic irreversibility, a tension resolved by the astronomical length of the recurrence times. The theorem is the starting point of ergodic theory. Formalization note. Conservative packages the measure-preserving and recurrence hypotheses, and frequently expresses return infinitely often. The result is Mathlib's MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem.
import Mathlib
namespace FamousTheorems
universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25
open Filter Set Topology DirectSum
theorem ae_mem_imp_frequently_image_mem :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α}
{s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ →
MeasureTheory.NullMeasurableSet s μ → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s := by sorry
end FamousTheorems