[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
⊢ ∃ᶠ (m : ℕ) in atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
[PROOFSTEP]
by_contra H
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ¬∃ᶠ (m : ℕ) in atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
⊢ False
[PROOFSTEP]
simp only [not_frequently, eventually_atTop, Ne.def, Classical.not_not] at H 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ∃ a, ∀ (b : ℕ), b ≥ a → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
rcases H with ⟨N, hN⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
induction' N with N ihN
[GOAL]
case intro.zero
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
apply h0
[GOAL]
case intro.zero
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ ↑↑μ s = 0
[PROOFSTEP]
simpa using hN 0 le_rfl
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : (∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0) → False
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
rw [imp_false] at ihN 
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : ¬∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
push_neg at ihN 
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
ihN : ∃ b, b ≥ N ∧ ↑↑μ (s ∩ f^[b] ⁻¹' s) ≠ 0
⊢ False
[PROOFSTEP]
rcases ihN with ⟨n, hn, hμn⟩
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
⊢ False
[PROOFSTEP]
set T := s ∩ ⋃ n ≥ N + 1, f^[n] ⁻¹' s
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
⊢ False
[PROOFSTEP]
have hT : MeasurableSet T := hs.inter (MeasurableSet.biUnion (to_countable _) fun _ _ => hf.measurable.iterate _ hs)
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ False
[PROOFSTEP]
have hμT : μ T = 0 := by
  convert (measure_biUnion_null_iff <| to_countable _).2 hN
  rw [← inter_iUnion₂]
  rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ ↑↑μ T = 0
[PROOFSTEP]
convert (measure_biUnion_null_iff <| to_countable _).2 hN
[GOAL]
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), s ∩ f^[i] ⁻¹' s
[PROOFSTEP]
rw [← inter_iUnion₂]
[GOAL]
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = s ∩ ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), f^[i] ⁻¹' s
[PROOFSTEP]
rfl
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
⊢ False
[PROOFSTEP]
have : μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0 := by rwa [measure_diff_null hμT]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
⊢ ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
[PROOFSTEP]
rwa [measure_diff_null hμT]
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
⊢ False
[PROOFSTEP]
rcases hf.exists_mem_image_mem ((hs.inter (hf.measurable.iterate n hs)).diff hT) this with
  ⟨x, ⟨⟨hxs, _⟩, hxT⟩, m, hm0, ⟨_, hxm⟩, _⟩
[GOAL]
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬f^[m] x ∈ T
left✝ : f^[m] x ∈ s
hxm : f^[m] x ∈ f^[n] ⁻¹' s
⊢ False
[PROOFSTEP]
refine' hxT ⟨hxs, mem_iUnion₂.2 ⟨n + m, _, _⟩⟩
[GOAL]
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬f^[m] x ∈ T
left✝ : f^[m] x ∈ s
hxm : f^[m] x ∈ f^[n] ⁻¹' s
⊢ n + m ≥ N + 1
[PROOFSTEP]
exact add_le_add hn (Nat.one_le_of_lt <| pos_iff_ne_zero.2 hm0)
[GOAL]
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬f^[m] x ∈ T
left✝ : f^[m] x ∈ s
hxm : f^[m] x ∈ f^[n] ⁻¹' s
⊢ x ∈ f^[n + m] ⁻¹' s
[PROOFSTEP]
rwa [Set.mem_preimage, ← iterate_add_apply] at hxm 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
[PROOFSTEP]
by_contra H
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
⊢ False
[PROOFSTEP]
have : MeasurableSet (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s}) :=
  by
  simp only [setOf_forall, ← compl_setOf]
  exact hs.inter (MeasurableSet.biInter (to_countable _) fun m _ => hf.measurable.iterate m hs.compl)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
⊢ MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
[PROOFSTEP]
simp only [setOf_forall, ← compl_setOf]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
⊢ MeasurableSet (s ∩ ⋂ (i : ℕ) (_ : i ≥ n), {a | f^[i] a ∈ s}ᶜ)
[PROOFSTEP]
exact hs.inter (MeasurableSet.biInter (to_countable _) fun m _ => hf.measurable.iterate m hs.compl)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
⊢ False
[PROOFSTEP]
rcases(hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})) ≠ 0
⊢ False
[PROOFSTEP]
rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})) ≠ 0
x : α
left✝ : x ∈ s
hxn : x ∈ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s}
hxm : f^[m] x ∈ s
⊢ False
[PROOFSTEP]
exact hxn m hmn.lt.le hxm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
simp only [frequently_atTop, @forall_swap (_ ∈ s), ae_all_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ i ∧ f^[b] a ∈ s
[PROOFSTEP]
intro n
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ n ∧ f^[b] a ∈ s
[PROOFSTEP]
filter_upwards [measure_zero_iff_ae_nmem.1 (hf.measure_mem_forall_ge_image_not_mem_eq_zero hs n)]
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] a ∈ s) → a ∈ s → ∃ b, b ≥ n ∧ f^[b] a ∈ s
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' ae_all_iff.2 fun k => _
[GOAL]
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' (hf.ae_mem_imp_frequently_image_mem (hf.measurable.iterate k hs)).mono fun x hx hk => _
[GOAL]
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
rw [← map_add_atTop_eq_nat k, frequently_map]
[GOAL]
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' (hx hk).mono fun n hn => _
[GOAL]
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
rwa [add_comm, iterate_add_apply]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
have : ∀ s ∈ countableBasis α, ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s := fun s hs =>
  h.ae_mem_imp_frequently_image_mem (isOpen_of_mem_countableBasis hs).measurableSet
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
refine' ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ (i : Set α), i ∈ countableBasis α → x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
rcases(isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ (i : Set α), i ∈ countableBasis α → x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
exact (hx o hoS hxo).mono fun n hn => hos hn
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[n] μ
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
⊢ Conservative f^[Nat.zero] μ
[PROOFSTEP]
exact Conservative.id μ
[GOAL]
case succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[Nat.succ n] μ
[PROOFSTEP]
refine' ⟨hf.1.iterate _, fun s hs hs0 => _⟩
[GOAL]
case succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
rcases(hf.frequently_ae_mem_and_frequently_image_mem hs hs0).exists with
  ⟨x, _, hx⟩
    /- We take a point `x ∈ s` such that `f^[k] x ∈ s` for infinitely many values of `k`,
        then we choose two of these values `k < l` such that `k ≡ l [MOD (n + 1)]`.
        Then `f^[k] x ∈ s` and `f^[n + 1]^[(l - k) / (n + 1)] (f^[k] x) = f^[l] x ∈ s`. -/
[GOAL]
case succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
rw [Nat.frequently_atTop_iff_infinite] at hx 
[GOAL]
case succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
rcases Nat.exists_lt_modEq_of_infinite hx n.succ_pos with ⟨k, hk, l, hl, hkl, hn⟩
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
set m := (l - k) / (n + 1)
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
have : (n + 1) * m = l - k := by
  apply Nat.mul_div_cancel'
  exact (Nat.modEq_iff_dvd' hkl.le).1 hn
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ (n + 1) * m = l - k
[PROOFSTEP]
apply Nat.mul_div_cancel'
[GOAL]
case H
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ n + 1 ∣ l - k
[PROOFSTEP]
exact (Nat.modEq_iff_dvd' hkl.le).1 hn
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
refine' ⟨f^[k] x, hk, m, _, _⟩
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ m ≠ 0
[PROOFSTEP]
intro hm
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
hm : m = 0
⊢ False
[PROOFSTEP]
rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this 
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : l ≤ k
hm : m = 0
⊢ False
[PROOFSTEP]
exact this.not_lt hkl
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ f^[Nat.succ n]^[m] (f^[k] x) ∈ s
[PROOFSTEP]
rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le]
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ k ≤ l
[PROOFSTEP]
exact hkl.le
