[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⟩
