OAI/NumberTheory/DukePrimeDegree/Dynamics/SmallOrbitSection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.measurePreserving_homeomorph_pow line 21
2. lemma OAI.DukePrimeDegree.separated_section_mass_bound line 34
3. theorem OAI.DukePrimeDegree.exists_small_complete_orbit_section line 76

   Source documentation

   Inside an aperiodic measurable set, complete sections can have arbitrarily small measure. Completeness refers to the represented orbits, so no ergodicity of e is needed.

   theorem exists_small_complete_orbit_section
       (μ : Measure Y) [IsProbabilityMeasure μ]
       (e : Y ≃ₜ Y) (he : MeasurePreserving e μ μ)
       {A : Set Y} (hA : MeasurableSet A)
       (hfree : ∀ x ∈ A, ∀ n : ℕ, 0 < n → (e^n) x ≠ x)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ S : Set Y, MeasurableSet S ∧ S ⊆ A ∧ μ.real S < ε ∧
         ∀ x ∈ A, ∃ y ∈ S, (homeomorphOrbitSetoid e).r x y := by
   …

   Mentions: OAI.DukePrimeDegree.homeomorphOrbitSetoid