frequently_ae_mem_and_frequently_image_mem

English

There exists a frequently returning point in s with its returns also frequently in s under iterates of f.

Русский

Существует x ∈ s, для которого возвраты в s происходят часто и сами возвраты происходят часто под итерациями f.

LaTeX

$$$\mathrm{Frequently}\bigl(\lambda x,\, x\in s \wedge \exists^{\mathrm{F}} n, f^{n}x\in s\bigr)$ in measure μ. (formal equivalence with a.e. membership).$$

Lean4

/-- If `f` is a conservative self-map and `s` is a measurable set of positive measure, then
`ae μ`-frequently we have `x ∈ s` and `s` returns to `s` under infinitely many iterations of `f`. -/
theorem frequently_ae_mem_and_frequently_image_mem (hf : Conservative f μ) (hs : NullMeasurableSet s μ) (h0 : μ s ≠ 0) :
    ∃ᵐ x ∂μ, x ∈ s ∧ ∃ᶠ n in atTop, f^[n] x ∈ s :=
  ((frequently_ae_mem_iff.2 h0).and_eventually (hf.ae_mem_imp_frequently_image_mem hs)).mono fun _ hx =>
    ⟨hx.1, hx.2 hx.1⟩

Похожие утверждения