MeasurePreservation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.TriangularBilliards.measure_image_countably_piecewise line 16

Source documentation

On a measurable set, an injective measurable map that locally agrees with one of countably many measure-preserving embeddings preserves the measure of that set. The pieces need not be open.

lemma measure_image_countably_piecewise
    {α : Type uAlpha} [MeasurableSpace α] [MeasurableEq α]
    (μ : Measure α) {f : α → α} (hf : Measurable f) {R : Set α}
    (hR : MeasurableSet R) (hi : InjOn f R) (F : ℕ → α → α)
    (hF : ∀ n, MeasurePreserving (F n) μ μ)
    (hE : ∀ n, MeasurableEmbedding (F n))
    (hcover : ∀ x ∈ R, ∃ n, f x = F n x) : μ (f '' R) = μ R := by
…

lemma OAI.TriangularBilliards.phaseWord_injective line 67
lemma OAI.TriangularBilliards.freeFlow_add line 74
lemma OAI.TriangularBilliards.freeFlow_zero line 80
lemma OAI.TriangularBilliards.freeFlow_injective line 82
lemma OAI.TriangularBilliards.measurableEmbedding_branch line 88
lemma OAI.TriangularBilliards.phaseMeasure_eq_regularAt line 93
lemma OAI.TriangularBilliards.measurePreserving_billiardFlow line 104
Source documentation
Exact Liouville-measure preservation of every actual billiard time map. The proof uses finite unfolding and injectivity, not an assumed dynamical invariance or a numerical/recurrence input.
```
lemma measurePreserving_billiardFlow (Q : Triangle) (t : ℝ) :
    MeasurePreserving (billiardFlow Q t) (phaseMeasure Q) (phaseMeasure Q) := by
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.billiardFlow, OAI.TriangularBilliards.phaseMeasure

theorem OAI.TriangularBilliards.geometric_obligations line 146

Source documentation

Geometric and nonvacuity conclusions for every nondegenerate triangle. Only ergodicity requires an irrational angle.

theorem geometric_obligations (Q : Triangle) :
    phaseMeasure Q univ = 1 ∧
    (∀ᵐ z ∂phaseMeasure Q, Nonempty (FlightChain Q z)) ∧
    (∀ (z : Phase) (c d : FlightChain Q z), c = d) ∧
    (∀ t : ℝ, MeasurePreserving (billiardFlow Q t) (phaseMeasure Q) (phaseMeasure Q)) ∧
    (∀ s t : ℝ, billiardFlow Q (s + t) =ᵐ[phaseMeasure Q]
      (billiardFlow Q s ∘ billiardFlow Q t)) :=
…

Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.phaseMeasure, OAI.TriangularBilliards.FlightChain, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.billiardFlow