exists_gt_measure_inter_ne_zero — Mathlib

English

For any N, there exists m > N with μ(s ∩ f^(-m)(s)) ≠ 0 for a conservative f and nonzero-measure s.

Русский

Для любого N найдётся m > N такое, что μ( s ∩ f^{-m}(s) ) ≠ 0.

LaTeX

$$$\forall N\in\mathbb{N},\ exists\ m>N: μ(s \cap f^{-[m]}(s)) \neq 0.$$$

Lean4

/-- If `f` is a conservative map and `s` is a measurable set of nonzero measure, then
for an arbitrarily large `m` a positive measure of points `x ∈ s` returns back to `s`
after `m` iterations of `f`. -/
theorem exists_gt_measure_inter_ne_zero (hf : Conservative f μ) (hs : NullMeasurableSet s μ) (h0 : μ s ≠ 0) (N : ℕ) :
    ∃ m > N, μ (s ∩ f^[m] ⁻¹' s) ≠ 0 :=
  let ⟨m, hm, hmN⟩ := ((hf.frequently_measure_inter_ne_zero hs h0).and_eventually (eventually_gt_atTop N)).exists
  ⟨m, hmN, hm⟩

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