ContractingCutItineraries.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Neighborhoods inside cut-itinerary atoms

Summable boundary avoidance and uniform contraction leave an entire parameter neighborhood in the same infinite itinerary atom. The contraction estimate is explicit, so it can be supplied by root dynamics.

lemma OAI.DukePrimeDegree.cut_agrees_of_abs_sub_le line 17
theorem OAI.DukePrimeDegree.eventually_cut_itinerary_eq line 29
theorem OAI.DukePrimeDegree.ae_avoid_cut_boundary_at_all_times line 55

theorem OAI.DukePrimeDegree.exists_cut_with_contracting_itinerary_neighborhoods line 70

Source documentation

A cut can be chosen in every open interval so that its infinite itinerary is locally constant along every uniformly contracting continuous parameter family, at almost every base point.

theorem exists_cut_with_contracting_itinerary_neighborhoods
    {Y : Type*} [TopologicalSpace Y] [MeasurableSpace Y]
    [OpensMeasurableSpace Y] (μ : Measure Y) [IsProbabilityMeasure μ]
    {T : Y → Y} (hT : MeasurePreserving T μ μ) (hTc : Continuous T)
    {f : Y → ℝ} (hf : Continuous f)
    (ε : ℕ → ℝ) (hε : Summable ε) (hεpos : ∀ n, 0 ≤ ε n)
    {a b : ℝ} (hab : a < b) :
    ∃ r ∈ Ioo a b, ∀ᵐ x ∂μ,
      ∀ {V : Type} [TopologicalSpace V] (F : V → Y) (v₀ : V),
        F v₀=x → ContinuousAt F v₀ →
        ∀ U ∈ 𝓝 v₀,
          (∀ n : ℕ, ∀ v ∈ U, |f (T^[n] (F v))-f (T^[n] x)| ≤ ε n) →
…