ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, (f^[k]) a ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) a ∈ s
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), (f^[k]) x ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
refine' ae_all_iff.2 fun k => _
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ f^[k] ⁻¹' s
hk : (f^[k]) x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, (f^[k]) a ∈ s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) a ∈ s
refine' (hf.ae_mem_imp_frequently_image_mem (hf.measurable.iterate k hs)).mono fun x hx hk => _
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ f^[k] ⁻¹' s
hk : (f^[k]) x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, (f^[a + k]) x ∈ s
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ f^[k] ⁻¹' s
hk : (f^[k]) x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ s
rw [← map_add_atTop_eq_nat k, frequently_map]
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ f^[k] ⁻¹' s
hk : (f^[k]) x ∈ s
n : ℕ
hn : (f^[n]) x ∈ f^[k] ⁻¹' s
⊢ (f^[n + k]) x ∈ s
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ f^[k] ⁻¹' s
hk : (f^[k]) x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, (f^[a + k]) x ∈ s
refine' (hx hk).mono fun n hn => _
no goals
ι : Type ?u.75187
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, (f^[n]) x ∈ f^[k] ⁻¹' s
hk : (f^[k]) x ∈ s
n : ℕ
hn : (f^[n]) x ∈ f^[k] ⁻¹' s
⊢ (f^[n + k]) x ∈ s
rwa [add_comm, iterate_add_apply]