UnboundedReturnSection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive sections with unbounded return levels

Small positive holes, pulled back over increasingly long orbit segments, remove only a prescribed amount of mass but preclude bounded return time.

theorem OAI.DukePrimeDegree.exists_unbounded_return_section_of_holes line 17

theorem OAI.DukePrimeDegree.exists_unbounded_return_section line 63

Source documentation

Only arbitrarily small positive measurable sets are needed to create unbounded return levels inside every positive section.

theorem exists_unbounded_return_section
    {Y : Type*} [MeasurableSpace Y] (μ : Measure Y) [IsProbabilityMeasure μ]
    {T : Y → Y} (hT : Ergodic T μ) (hE : MeasurableEmbedding T)
    (hsmall : ∀ ε : ℝ≥0∞, 0 < ε → ε ≠ ∞ →
      ∃ E : Set Y, MeasurableSet E ∧ μ E ≠ 0 ∧ μ E ≤ ε)
    {A : Set Y} (hA : MeasurableSet A) (hAp : μ A ≠ 0) :
    ∃ S : Set Y, MeasurableSet S ∧ S ⊆ A ∧ μ S ≠ 0 ∧
      ∀ N : ℕ, ∃ n : ℕ, N ≤ n ∧ μ (firstReturnLevel T S n) ≠ 0 := by
…

Mentions: OAI.DukePrimeDegree.firstReturnLevel