[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa✝ : Measure α
μb✝ : Measure β
μc : Measure γ
μd : Measure δ
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving ↑e
⊢ map (↑(MeasurableEquiv.symm e)) μb = μa
[PROOFSTEP]
rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
s : Set β
hs : MeasurableSet s
⊢ map f (Measure.restrict μa (f ⁻¹' s)) = Measure.restrict μb s
[PROOFSTEP]
rw [← hf.map_eq, restrict_map hf.measurable hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
h₂ : MeasurableEmbedding f
s : Set β
⊢ map f (Measure.restrict μa (f ⁻¹' s)) = Measure.restrict μb s
[PROOFSTEP]
rw [← hf.map_eq, h₂.restrict_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
h₂ : MeasurableEmbedding f
s : Set α
⊢ MeasurePreserving f
[PROOFSTEP]
simpa only [Set.preimage_image_eq _ h₂.injective] using hf.restrict_preimage_emb h₂ (f '' s)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEMeasurable (g ∘ f) ↔ AEMeasurable g
[PROOFSTEP]
rw [← hf.map_eq, h₂.aemeasurable_map_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : β → γ
f : α → β
hg : MeasurePreserving g
hf : MeasurePreserving f
⊢ map (g ∘ f) μa = μc
[PROOFSTEP]
rw [← map_map hg.1 hf.1, hf.2, hg.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving ↑e
⊢ MeasurePreserving (↑e ∘ g) ↔ MeasurePreserving g
[PROOFSTEP]
refine' ⟨fun hg => _, fun hg => h.comp hg⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving ↑e
hg : MeasurePreserving (↑e ∘ g)
⊢ MeasurePreserving g
[PROOFSTEP]
convert (MeasurePreserving.symm e h).comp hg
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving ↑e
hg : MeasurePreserving (↑e ∘ g)
⊢ g = ↑(MeasurableEquiv.symm e) ∘ ↑e ∘ g
[PROOFSTEP]
simp [← Function.comp.assoc e.symm e g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
⊢ MeasurePreserving (g ∘ ↑e) ↔ MeasurePreserving g
[PROOFSTEP]
refine' ⟨fun hg => _, fun hg => hg.comp h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
hg : MeasurePreserving (g ∘ ↑e)
⊢ MeasurePreserving g
[PROOFSTEP]
convert hg.comp (MeasurePreserving.symm e h)
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
hg : MeasurePreserving (g ∘ ↑e)
⊢ g = (g ∘ ↑e) ∘ ↑(MeasurableEquiv.symm e)
[PROOFSTEP]
simp [Function.comp.assoc g e e.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
inst✝ : SigmaFinite μb
⊢ SigmaFinite (map f μa)
[PROOFSTEP]
rwa [hf.map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
s : Set β
hs : MeasurableSet s
⊢ ↑↑μa (f ⁻¹' s) = ↑↑μb s
[PROOFSTEP]
rw [← hf.map_eq, map_apply hf.1 hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
hfe : MeasurableEmbedding f
s : Set β
⊢ ↑↑μa (f ⁻¹' s) = ↑↑μb s
[PROOFSTEP]
rw [← hf.map_eq, hfe.map_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
⊢ ↑↑μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • ↑↑μ (s ∆ (f ⁻¹' s))
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
⊢ ↑↑μ (s ∆ (f^[Nat.zero] ⁻¹' s)) ≤ Nat.zero • ↑↑μ (s ∆ (f ⁻¹' s))
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
ih : ↑↑μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • ↑↑μ (s ∆ (f ⁻¹' s))
⊢ ↑↑μ (s ∆ (f^[Nat.succ n] ⁻¹' s)) ≤ Nat.succ n • ↑↑μ (s ∆ (f ⁻¹' s))
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
ih : ↑↑μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • ↑↑μ (s ∆ (f ⁻¹' s))
⊢ ↑↑μ (s ∆ (f^[Nat.succ n] ⁻¹' s)) ≤ Nat.succ n • ↑↑μ (s ∆ (f ⁻¹' s))
[PROOFSTEP]
simp only [add_smul, one_smul, ← n.add_one]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
ih : ↑↑μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • ↑↑μ (s ∆ (f ⁻¹' s))
⊢ ↑↑μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ n • ↑↑μ (s ∆ (f ⁻¹' s)) + ↑↑μ (s ∆ (f ⁻¹' s))
[PROOFSTEP]
refine' le_trans (measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)) (add_le_add ih _)
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
ih : ↑↑μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • ↑↑μ (s ∆ (f ⁻¹' s))
⊢ ↑↑μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ ↑↑μ (s ∆ (f ⁻¹' s))
[PROOFSTEP]
replace hs : MeasurableSet (s ∆ (f ⁻¹' s)) := hs.symmDiff $ hf.measurable hs
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
n : ℕ
ih : ↑↑μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • ↑↑μ (s ∆ (f ⁻¹' s))
hs : MeasurableSet (s ∆ (f ⁻¹' s))
⊢ ↑↑μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ ↑↑μ (s ∆ (f ⁻¹' s))
[PROOFSTEP]
rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
have A : ∀ m, MeasurableSet (f^[m] ⁻¹' s) := fun m => (hf.iterate m).measurable hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m => (hf.iterate m).measure_preimage hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
have : μ (Set.univ : Set α) < (Finset.range n).sum fun m => μ (f^[m] ⁻¹' s) := by
  simpa only [B, nsmul_eq_mul, Finset.sum_const, Finset.card_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
⊢ ↑↑μ univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
[PROOFSTEP]
simpa only [B, nsmul_eq_mul, Finset.sum_const, Finset.card_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
rcases exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ => A m) this with
  ⟨i, hi, j, hj, hij, x, hxi, hxj⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
i : ℕ
hi : i ∈ Finset.range n
j : ℕ
hj : j ∈ Finset.range n
hij : i ≠ j
x : α
hxi : x ∈ f^[i] ⁻¹' s
hxj : x ∈ f^[j] ⁻¹' s
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
wlog hlt : i < j generalizing i j
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this✝ : ↑↑μ univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
i : ℕ
hi : i ∈ Finset.range n
j : ℕ
hj : j ∈ Finset.range n
hij : i ≠ j
x : α
hxi : x ∈ f^[i] ⁻¹' s
hxj : x ∈ f^[j] ⁻¹' s
this :
  ∀ (i : ℕ),
    i ∈ Finset.range n →
      ∀ (j : ℕ),
        j ∈ Finset.range n →
          i ≠ j → x ∈ f^[i] ⁻¹' s → x ∈ f^[j] ⁻¹' s → i < j → ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
hlt : ¬i < j
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
exact this j hj i hi hij.symm hxj hxi (hij.lt_or_lt.resolve_left hlt)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
x : α
i : ℕ
hi : i ∈ Finset.range n
j : ℕ
hj : j ∈ Finset.range n
hij : i ≠ j
hxi : x ∈ f^[i] ⁻¹' s
hxj : x ∈ f^[j] ⁻¹' s
hlt : i < j
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
simp only [Set.mem_preimage, Finset.mem_range] at hi hj hxi hxj
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
x : α
i j : ℕ
hij : i ≠ j
hlt : i < j
hi : i < n
hj : j < n
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Ioo 0 n ∧ f^[m] x ∈ s
[PROOFSTEP]
refine' ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f
hs : MeasurableSet s
n : ℕ
hvol : ↑↑μ univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
x : α
i j : ℕ
hij : i ≠ j
hlt : i < j
hi : i < n
hj : j < n
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
⊢ f^[j - i] (f^[i] x) ∈ s
[PROOFSTEP]
rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[m] x ∈ s
[PROOFSTEP]
rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (Set.univ : Set α)) with ⟨N, hN⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
N : ℕ
hN : ↑↑μ univ < ↑N * ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[m] x ∈ s
[PROOFSTEP]
rcases hf.exists_mem_image_mem_of_volume_lt_mul_volume hs hN with ⟨x, hx, m, hm, hmx⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
N : ℕ
hN : ↑↑μ univ < ↑N * ↑↑μ s
x : α
hx : x ∈ s
m : ℕ
hm : m ∈ Ioo 0 N
hmx : f^[m] x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[m] x ∈ s
[PROOFSTEP]
exact ⟨x, hx, m, hm.1.ne', hmx⟩


[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : PreErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ ↑↑μ s = 0 ∨ ↑↑μ sᶜ = 0
[PROOFSTEP]
simpa using hf.ae_empty_or_univ hs hs'
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : PreErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ ↑↑μ s = 0 ∨ ↑↑μ s = 1
[PROOFSTEP]
simpa [hs] using hf.measure_self_or_compl_eq_zero hs hs'
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
⊢ ∀ ⦃s : Set β⦄, MeasurableSet s → f' ⁻¹' s = s → s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
intro s hs₀ hs₁
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
replace hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
[GOAL]
case hs₁
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
[PROOFSTEP]
rw [← preimage_comp, h_comm, preimage_comp, hs₁]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
cases' hf.ae_empty_or_univ (hg.measurable hs₀) hs₁ with hs₂ hs₂ <;> [left; right]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
cases' hf.ae_empty_or_univ (hg.measurable hs₀) hs₁ with hs₂ hs₂
[GOAL]
case inl
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
left
[GOAL]
case inr
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
right
[GOAL]
case inl.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ'] ∅
[PROOFSTEP]
simpa only [ae_eq_empty, hg.measure_preimage hs₀] using hs₂
[GOAL]
case inr.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ'] univ
[PROOFSTEP]
simpa only [ae_eq_univ, ← preimage_compl, hg.measure_preimage hs₀.compl] using hs₂
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ PreErgodic f
[PROOFSTEP]
refine'
  ⟨fun hf => preErgodic_of_preErgodic_conjugate (h.symm e) hf _, fun hf => preErgodic_of_preErgodic_conjugate h hf _⟩
[GOAL]
case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ ↑(MeasurableEquiv.symm e) ∘ ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)
[PROOFSTEP]
change (e.symm ∘ e) ∘ f ∘ e.symm = f ∘ e.symm
[GOAL]
case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ (↑(MeasurableEquiv.symm e) ∘ ↑e) ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)
[PROOFSTEP]
rw [MeasurableEquiv.symm_comp_self, comp.left_id]
[GOAL]
case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ∘ ↑e
[PROOFSTEP]
change e ∘ f = e ∘ f ∘ e.symm ∘ e
[GOAL]
case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) ∘ ↑e
[PROOFSTEP]
rw [MeasurableEquiv.symm_comp_self, comp.right_id]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
[PROOFSTEP]
have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
  rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
[PROOFSTEP]
rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
[PROOFSTEP]
replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
h : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ PreErgodic f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
[PROOFSTEP]
exact
  ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with }, fun hf =>
    { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
obtain ⟨t, h₀, h₁, h₂⟩ := hf.toQuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae hs hs'
[GOAL]
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
rcases hf.ae_empty_or_univ h₀ h₂ with (h₃ | h₃) <;> [left; right]
[GOAL]
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
rcases hf.ae_empty_or_univ h₀ h₂ with (h₃ | h₃)
[GOAL]
case intro.intro.intro.inl
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
left
[GOAL]
case intro.intro.intro.inr
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
right
[GOAL]
case intro.intro.intro.inl.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ] ∅
[PROOFSTEP]
exact ae_eq_trans h₁.symm h₃
[GOAL]
case intro.intro.intro.inr.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ] univ
[PROOFSTEP]
exact ae_eq_trans h₁.symm h₃
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hsm : NullMeasurableSet s
hs : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] univ → ∀ᵐ (x : α) ∂μ, x ∈ s
[PROOFSTEP]
simp [mem_ae_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hsm : NullMeasurableSet s
hs : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ → ∀ᵐ (x : α) ∂μ, ¬x ∈ s
[PROOFSTEP]
simp [ae_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
refine' hf.quasiErgodic.ae_empty_or_univ' hs _
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
[PROOFSTEP]
refine' ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).symm.le _ h_fin
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ MeasurableSet (f ⁻¹' s)
[PROOFSTEP]
exact measurableSet_preimage hf.measurable hs
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
replace h_fin : μ (f ⁻¹' s) ≠ ∞
[GOAL]
case h_fin
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (f ⁻¹' s) ≠ ⊤
[PROOFSTEP]
rwa [hf.measure_preimage hs]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
refine' hf.quasiErgodic.ae_empty_or_univ' hs _
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
[PROOFSTEP]
exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f '' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
  (HasSubset.Subset.eventuallyLE (subset_preimage_image f s)).trans (hf.quasiMeasurePreserving.preimage_mono_ae hs')
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
h_fin : ↑↑μ s ≠ ⊤
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin