α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
have A : ∀ m, MeasurableSet (f^[m] ⁻¹' s) := fun m => (hf.iterate m).measurable hs
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m => (hf.iterate m).measure_preimage hs
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
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]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
rcases exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ => A m) this with
  ⟨i, hi, j, hj, hij, x, hxi, hxj⟩
case intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this✝ : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
hlt : ¬i < j
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s

α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
wlog hlt : i < j generalizing i j
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
simp only [Set.mem_preimage, Finset.mem_range] at hi hj hxi hxj
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
refine' ⟨(f^[i]) x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, _⟩
no goals
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this : ↑↑μ Set.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
rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]
no goals
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
⊢ ↑↑μ Set.univ < Finset.sum (Finset.range n) fun m => ↑↑μ (f^[m] ⁻¹' s)
simpa only [B, nsmul_eq_mul, Finset.sum_const, Finset.card_range]
no goals
case intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type ?u.272685
γ : Type ?u.272688
δ : Type ?u.272691
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 : ↑↑μ Set.univ < ↑n * ↑↑μ s
A : ∀ (m : ℕ), MeasurableSet (f^[m] ⁻¹' s)
B : ∀ (m : ℕ), ↑↑μ (f^[m] ⁻¹' s) = ↑↑μ s
this✝ : ↑↑μ Set.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 ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
hlt : ¬i < j
⊢ ∃ x, x ∈ s ∧ ∃ m, m ∈ Set.Ioo 0 n ∧ (f^[m]) x ∈ s
exact this j hj i hi hij.symm hxj hxi (hij.lt_or_lt.resolve_left hlt)