Revision #1175 → #1815 · back to history
modifiedPoincaré recurrence theoreme676d1ac9f2e
| Field | From #1175 | To #1815 |
|---|
| mathlib.decl | Conservative.measure_mem_forall_ge_image_count_eq | MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero |
| note | Mathlib's `Mathlib.Dynamics.Ergodic.Conservative` contains both the measure-theoretic and topological versions of Poincaré recurrence. | Mathlib's `Mathlib.Dynamics.Ergodic.Conservative` proves the measure-theoretic Poincaré recurrence theorem along with a topological version. |
addedLyapunov stability4c504691df39
addedStructural stabilityf5278e4bf759
addedSmale horseshoe46c1b499cfca
modifiedPoincaré recurrence theorem (ergodic statement)a72ddb7e4c49
| Field | From #1175 | To #1815 |
|---|
| mathlib.decl | Conservative.measure_mem_forall_ge_image_count_eq | MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero |
addedPicard–Lindelöf theorem9f40e31ddb69