feat(*): add various order-related lemmas (#16918)

These all came up while preparing to introduce the definition of ergodic maps but it seems better to PR them separately.





Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/nat/basic.lean

@@ -150,6 +150,8 @@ open set
 theorem zero_union_range_succ : {0} ∪ range succ = univ :=
 by { ext n, cases n; simp }
 
+@[simp] protected lemma range_succ : range succ = {i | 0 < i} := by ext (_ | i); simp [succ_pos]
+
 variables {α : Type*}
 
 theorem range_of_succ (f : ℕ → α) : {f 0} ∪ range (f ∘ succ) = range f :=

src/data/set/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 import order.symm_diff
+import logic.function.iterate
 
 /-!
 # Basic properties of sets
@@ -1359,7 +1360,9 @@ rfl
 @[simp] theorem preimage_set_of_eq {p : α → Prop} {f : β → α} : f ⁻¹' {a | p a} = {a | p (f a)} :=
 rfl
 
-@[simp] theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl
+@[simp] lemma preimage_id_eq : preimage (id : α → α) = id := rfl
+
+theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl
 
 @[simp] theorem preimage_id' {s : set α} : (λ x, x) ⁻¹' s = s := rfl
 
@@ -1377,6 +1380,15 @@ by { split_ifs with hb hb, exacts [preimage_const_of_mem hb, preimage_const_of_n
 
 theorem preimage_comp {s : set γ} : (g ∘ f) ⁻¹' s = f ⁻¹' (g ⁻¹' s) := rfl
 
+lemma preimage_comp_eq : preimage (g ∘ f) = preimage f ∘ preimage g := rfl
+
+@[simp] lemma preimage_iterate_eq {f : α → α} {n : ℕ} :
+  set.preimage (f^[n]) = ((set.preimage f)^[n]) :=
+begin
+  induction n with n ih, { simp, },
+  rw [iterate_succ, iterate_succ', set.preimage_comp_eq, ih],
+end
+
 lemma preimage_preimage {g : β → γ} {f : α → β} {s : set γ} :
   f ⁻¹' (g ⁻¹' s) = (λ x, g (f x)) ⁻¹' s :=
 preimage_comp.symm

src/dynamics/fixed_points/basic.lean

@@ -71,6 +71,10 @@ calc fb (g x) = g (fa x) : (h.eq x).symm
 protected lemma apply {x : α} (hx : is_fixed_pt f x) : is_fixed_pt f (f x) :=
 by convert hx
 
+lemma preimage_iterate {s : set α} (h : is_fixed_pt (set.preimage f) s) (n : ℕ) :
+  is_fixed_pt (set.preimage (f^[n])) s :=
+by { rw set.preimage_iterate_eq, exact h.iterate n, }
+
 end is_fixed_pt
 
 @[simp] lemma injective.is_fixed_pt_apply_iff (hf : injective f) {x : α} :

src/measure_theory/measurable_space.lean

@@ -267,7 +267,6 @@ begin
   exact (hf ht).inter h.measurable_set.of_compl,
 end
 
-
 end measurable_functions
 
 section constructions
@@ -1462,4 +1461,18 @@ instance : boolean_algebra (subtype (measurable_set : set α → Prop)) :=
   .. measurable_set.subtype.bounded_order,
   .. measurable_set.subtype.distrib_lattice }
 
+@[measurability] lemma measurable_set_limsup {s : ℕ → set α} (hs : ∀ n, measurable_set $ s n) :
+  measurable_set $ filter.limsup s filter.at_top :=
+begin
+  simp only [filter.limsup_eq_infi_supr_of_nat', supr_eq_Union, infi_eq_Inter],
+  exact measurable_set.Inter (λ n, measurable_set.Union $ λ m, hs $ m + n),
+end
+
+@[measurability] lemma measurable_set_liminf {s : ℕ → set α} (hs : ∀ n, measurable_set $ s n) :
+  measurable_set $ filter.liminf s filter.at_top :=
+begin
+  simp only [filter.liminf_eq_supr_infi_of_nat', supr_eq_Union, infi_eq_Inter],
+  exact measurable_set.Union (λ n, measurable_set.Inter $ λ m, hs $ m + n),
+end
+
 end measurable_set

src/measure_theory/measure/measure_space.lean

@@ -527,6 +527,42 @@ begin
   exact λ ⟨i, hi⟩, ⟨i + (m - n), by simpa only [add_assoc, tsub_add_cancel_of_le hnm] using hi⟩
 end
 
+lemma measure_liminf_eq_zero {s : ℕ → set α} (h : ∑' i, μ (s i) ≠ ⊤) : μ (liminf s at_top) = 0 :=
+begin
+  rw ← le_zero_iff,
+  have : liminf s at_top ≤ limsup s at_top :=
+    liminf_le_limsup (by is_bounded_default) (by is_bounded_default),
+  exact (μ.mono this).trans (by simp [measure_limsup_eq_zero h]),
+end
+
+lemma limsup_ae_eq_of_forall_ae_eq (s : ℕ → set α) {t : set α} (h : ∀ n, s n =ᵐ[μ] t) :
+  -- Need `@` below because of diamond; see gh issue #16932
+  @limsup (set α) ℕ _ s at_top =ᵐ[μ] t :=
+begin
+  simp_rw ae_eq_set at h ⊢,
+  split,
+  { rw at_top.limsup_sdiff s t,
+    apply measure_limsup_eq_zero,
+    simp [h], },
+  { rw at_top.sdiff_limsup s t,
+    apply measure_liminf_eq_zero,
+    simp [h], },
+end
+
+lemma liminf_ae_eq_of_forall_ae_eq (s : ℕ → set α) {t : set α} (h : ∀ n, s n =ᵐ[μ] t) :
+  -- Need `@` below because of diamond; see gh issue #16932
+  @liminf (set α) ℕ _ s at_top =ᵐ[μ] t :=
+begin
+  simp_rw ae_eq_set at h ⊢,
+  split,
+  { rw at_top.liminf_sdiff s t,
+    apply measure_liminf_eq_zero,
+    simp [h], },
+  { rw at_top.sdiff_liminf s t,
+    apply measure_limsup_eq_zero,
+    simp [h], },
+end
+
 lemma measure_if {x : β} {t : set β} {s : set α} :
   μ (if x ∈ t then s else ∅) = indicator t (λ _, μ s) x :=
 by { split_ifs; simp [h] }
@@ -2006,6 +2042,32 @@ lemma preimage_null (h : quasi_measure_preserving f μa μb) {s : set β} (hs :
   μa (f ⁻¹' s) = 0 :=
 preimage_null_of_map_null h.ae_measurable (h.2 hs)
 
+lemma limsup_preimage_iterate_ae_eq {f : α → α} (hf : quasi_measure_preserving f μ μ)
+  (hs : f⁻¹' s =ᵐ[μ] s) :
+  -- Need `@` below because of diamond; see gh issue #16932
+  @limsup (set α) ℕ _ (λ n, (preimage f)^[n] s) at_top =ᵐ[μ] s :=
+begin
+  have : ∀ n, (preimage f)^[n] s =ᵐ[μ] s,
+  { intros n,
+    induction n with n ih, { simp, },
+    simpa only [iterate_succ', comp_app] using ae_eq_trans (hf.ae_eq ih) hs, },
+  exact (limsup_ae_eq_of_forall_ae_eq (λ n, (preimage f)^[n] s) this).trans (ae_eq_refl _),
+end
+
+lemma liminf_preimage_iterate_ae_eq {f : α → α} (hf : quasi_measure_preserving f μ μ)
+  (hs : f⁻¹' s =ᵐ[μ] s) :
+  -- Need `@` below because of diamond; see gh issue #16932
+  @liminf (set α) ℕ _ (λ n, (preimage f)^[n] s) at_top =ᵐ[μ] s :=
+begin
+  -- Need `@` below because of diamond; see gh issue #16932
+  rw [← ae_eq_set_compl_compl, @filter.liminf_compl (set α)],
+  rw [← ae_eq_set_compl_compl, ← preimage_compl] at hs,
+  convert hf.limsup_preimage_iterate_ae_eq hs,
+  ext1 n,
+  simp only [← set.preimage_iterate_eq, comp_app, preimage_compl],
+end
+
+
 end quasi_measure_preserving
 
 /-! ### The `cofinite` filter -/
@@ -2530,6 +2592,24 @@ lemma is_probability_measure_map [is_probability_measure μ] {f : α → β} (hf
   is_probability_measure (map f μ) :=
 ⟨by simp [map_apply_of_ae_measurable, hf]⟩
 
+@[simp] lemma one_le_prob_iff [is_probability_measure μ] : 1 ≤ μ s ↔ μ s = 1 :=
+⟨λ h, le_antisymm prob_le_one h, λ h, h ▸ le_refl _⟩
+
+/-- Note that this is not quite as useful as it looks because the measure takes values in `ℝ≥0∞`.
+Thus the subtraction appearing is the truncated subtraction of `ℝ≥0∞`, rather than the
+better-behaved subtraction of `ℝ`. -/
+lemma prob_compl_eq_one_sub [is_probability_measure μ] (hs : measurable_set s) :
+  μ sᶜ = 1 - μ s :=
+by simpa only [measure_univ] using measure_compl hs (measure_lt_top μ s).ne
+
+@[simp] lemma prob_compl_eq_zero_iff [is_probability_measure μ] (hs : measurable_set s) :
+  μ sᶜ = 0 ↔ μ s = 1 :=
+by simp only [prob_compl_eq_one_sub hs, tsub_eq_zero_iff_le, one_le_prob_iff]
+
+@[simp] lemma prob_compl_eq_one_iff [is_probability_measure μ] (hs : measurable_set s) :
+  μ sᶜ = 1 ↔ μ s = 0 :=
+by rwa [← prob_compl_eq_zero_iff hs.compl, compl_compl]
+
 end is_probability_measure
 
 section no_atoms

src/measure_theory/measure/measure_space_def.lean

@@ -376,6 +376,18 @@ lemma ae_eq_set {s t : set α} :
   s =ᵐ[μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0 :=
 by simp [eventually_le_antisymm_iff, ae_le_set]
 
+@[simp] lemma measure_symm_diff_eq_zero_iff {s t : set α} :
+  μ (s ∆ t) = 0 ↔ s =ᵐ[μ] t :=
+by simp [ae_eq_set, symm_diff_def]
+
+@[simp] lemma ae_eq_set_compl_compl {s t : set α} :
+  sᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] t :=
+by simp only [← measure_symm_diff_eq_zero_iff, compl_symm_diff_compl]
+
+lemma ae_eq_set_compl {s t : set α} :
+  sᶜ =ᵐ[μ] t ↔ s =ᵐ[μ] tᶜ :=
+by rw [← ae_eq_set_compl_compl, compl_compl]
+
 lemma ae_eq_set_inter {s' t' : set α} (h : s =ᵐ[μ] t) (h' : s' =ᵐ[μ] t') :
   (s ∩ s' : set α) =ᵐ[μ] (t ∩ t' : set α) :=
 h.inter h'

src/order/complete_lattice.lean

@@ -818,6 +818,15 @@ supr_subtype
 lemma infi_subtype'' {ι} (s : set ι) (f : ι → α) : (⨅ i : s, f i) = ⨅ (t : ι) (H : t ∈ s), f t :=
 infi_subtype
 
+lemma bsupr_const {ι : Sort*} {a : α} {s : set ι} (hs : s.nonempty) : (⨆ i ∈ s, a) = a :=
+begin
+  haveI : nonempty s := set.nonempty_coe_sort.mpr hs,
+  rw [← supr_subtype'', supr_const],
+end
+
+lemma binfi_const {ι : Sort*} {a : α} {s : set ι} (hs : s.nonempty) : (⨅ i ∈ s, a) = a :=
+@bsupr_const αᵒᵈ _ ι _ s hs
+
 theorem supr_sup_eq : (⨆ x, f x ⊔ g x) = (⨆ x, f x) ⊔ (⨆ x, g x) :=
 le_antisymm
   (supr_le $ λ i, sup_le_sup (le_supr _ _) $ le_supr _ _)
@@ -846,14 +855,22 @@ by rw [supr_sup_eq, supr_const]
 lemma inf_infi [nonempty ι] {f : ι → α} {a : α} : a ⊓ (⨅ x, f x) = ⨅ x, a ⊓ f x :=
 by rw [infi_inf_eq, infi_const]
 
-lemma binfi_inf {p : ι → Prop} {f : Π i (hi : p i), α} {a : α} (h : ∃ i, p i) :
-  (⨅ i (h : p i), f i h) ⊓ a = ⨅ i (h : p i), f i h ⊓ a :=
+lemma bsupr_sup {p : ι → Prop} {f : Π i, p i → α} {a : α} (h : ∃ i, p i) :
+  (⨆ i (h : p i), f i h) ⊔ a = ⨆ i (h : p i), f i h ⊔ a :=
 by haveI : nonempty {i // p i} := (let ⟨i, hi⟩ := h in ⟨⟨i, hi⟩⟩);
-  rw [infi_subtype', infi_subtype', infi_inf]
+  rw [supr_subtype', supr_subtype', supr_sup]
 
-lemma inf_binfi {p : ι → Prop} {f : Π i (hi : p i), α} {a : α} (h : ∃ i, p i) :
+lemma sup_bsupr {p : ι → Prop} {f : Π i, p i → α} {a : α} (h : ∃ i, p i) :
+  a ⊔ (⨆ i (h : p i), f i h) = ⨆ i (h : p i), a ⊔ f i h :=
+by simpa only [sup_comm] using bsupr_sup h
+
+lemma binfi_inf {p : ι → Prop} {f : Π i, p i → α} {a : α} (h : ∃ i, p i) :
+  (⨅ i (h : p i), f i h) ⊓ a = ⨅ i (h : p i), f i h ⊓ a :=
+@bsupr_sup αᵒᵈ ι _ p f _ h
+
+lemma inf_binfi {p : ι → Prop} {f : Π i, p i → α} {a : α} (h : ∃ i, p i) :
   a ⊓ (⨅ i (h : p i), f i h) = ⨅ i (h : p i), a ⊓ f i h :=
-by simpa only [inf_comm] using binfi_inf h
+@sup_bsupr αᵒᵈ ι _ p f _ h
 
 /-! ### `supr` and `infi` under `Prop` -/
 
@@ -1161,6 +1178,14 @@ end
 lemma inf_infi_nat_succ (u : ℕ → α) : u 0 ⊓ (⨅ i, u (i + 1)) = ⨅ i, u i :=
 @sup_supr_nat_succ αᵒᵈ _ u
 
+lemma infi_nat_gt_zero_eq (f : ℕ → α) :
+  (⨅ (i > 0), f i) = ⨅ i, f (i + 1) :=
+by simpa only [(by simp : ∀ (i : ℕ), i > 0 ↔ i ∈ range nat.succ)] using infi_range
+
+lemma supr_nat_gt_zero_eq (f : ℕ → α) :
+  (⨆ (i > 0), f i) = ⨆ i, f (i + 1) :=
+@infi_nat_gt_zero_eq αᵒᵈ _ f
+
 end
 
 section complete_linear_order

src/order/liminf_limsup.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Johannes Hölzl, Rémy Degenne
 -/
 import order.filter.cofinite
+import order.hom.complete_lattice
 
 /-!
 # liminfs and limsups of functions and filters
@@ -607,6 +608,25 @@ lemma le_limsup_of_frequently_le' {α β} [complete_lattice β]
   x ≤ limsup u f :=
 @liminf_le_of_frequently_le' _ βᵒᵈ _ _ _ _ h
 
+/-- If `f : α → α` is a morphism of complete lattices, then the limsup of its iterates of any
+`a : α` is a fixed point. -/
+@[simp] lemma complete_lattice_hom.apply_limsup_iterate (f : complete_lattice_hom α α) (a : α) :
+  f (limsup (λ n, f^[n] a) at_top) = limsup (λ n, f^[n] a) at_top :=
+begin
+  rw [limsup_eq_infi_supr_of_nat', map_infi],
+  simp_rw [_root_.map_supr, ← function.comp_apply f, ← function.iterate_succ' f, ← nat.add_succ],
+  conv_rhs { rw infi_split _ ((<) (0 : ℕ)), },
+  simp only [not_lt, le_zero_iff, infi_infi_eq_left, add_zero, infi_nat_gt_zero_eq, left_eq_inf],
+  refine (infi_le (λ i, ⨆ j, (f^[j + (i + 1)]) a) 0).trans _,
+  simp only [zero_add, function.comp_app, supr_le_iff],
+  exact λ i, le_supr (λ i, (f^[i] a)) (i + 1),
+end
+
+/-- If `f : α → α` is a morphism of complete lattices, then the liminf of its iterates of any
+`a : α` is a fixed point. -/
+lemma complete_lattice_hom.apply_liminf_iterate (f : complete_lattice_hom α α) (a : α) :
+  f (liminf (λ n, f^[n] a) at_top) = liminf (λ n, f^[n] a) at_top :=
+(complete_lattice_hom.dual f).apply_limsup_iterate _
 variables {f g : filter β} {p q : β → Prop} {u v : β → α}
 
 lemma blimsup_mono (h : ∀ x, p x → q x) :
@@ -678,8 +698,72 @@ end
   bliminf u f (λ x, p x ∨ q x) = bliminf u f p ⊓ bliminf u f q :=
 @blimsup_or_eq_sup αᵒᵈ β _ f p q u
 
+lemma sup_limsup [ne_bot f] (a : α) :
+  a ⊔ limsup u f = limsup (λ x, a ⊔ u x) f :=
+begin
+  simp only [limsup_eq_infi_supr, supr_sup_eq, sup_binfi_eq],
+  congr, ext s, congr, ext hs, congr,
+  exact (bsupr_const (nonempty_of_mem hs)).symm,
+end
+
+lemma inf_liminf [ne_bot f] (a : α) :
+  a ⊓ liminf u f = liminf (λ x, a ⊓ u x) f :=
+@sup_limsup αᵒᵈ β _ f _ _ _
+
+lemma sup_liminf (a : α) :
+  a ⊔ liminf u f = liminf (λ x, a ⊔ u x) f :=
+begin
+  simp only [liminf_eq_supr_infi],
+  rw [sup_comm, bsupr_sup (⟨univ, univ_mem⟩ : ∃ (i : set β), i ∈ f)],
+  simp_rw [binfi_sup_eq, @sup_comm _ _ a],
+end
+
+lemma inf_limsup (a : α) :
+  a ⊓ limsup u f = limsup (λ x, a ⊓ u x) f :=
+@sup_liminf αᵒᵈ β _ f _ _
+
 end complete_distrib_lattice
 
+section complete_boolean_algebra
+
+variables [complete_boolean_algebra α] (f : filter β) (u : β → α)
+
+lemma limsup_compl :
+  (limsup u f)ᶜ = liminf (compl ∘ u) f :=
+by simp only [limsup_eq_infi_supr, liminf_eq_supr_infi, compl_infi, compl_supr]
+
+lemma liminf_compl :
+  (liminf u f)ᶜ = limsup (compl ∘ u) f :=
+by simp only [limsup_eq_infi_supr, liminf_eq_supr_infi, compl_infi, compl_supr]
+
+lemma limsup_sdiff (a : α) :
+  (limsup u f) \ a = limsup (λ b, (u b) \ a) f :=
+begin
+  simp only [limsup_eq_infi_supr, sdiff_eq],
+  rw binfi_inf (⟨univ, univ_mem⟩ : ∃ (i : set β), i ∈ f),
+  simp_rw [inf_comm, inf_bsupr_eq, inf_comm],
+end
+
+lemma liminf_sdiff [ne_bot f] (a : α) :
+  (liminf u f) \ a = liminf (λ b, (u b) \ a) f :=
+by simp only [sdiff_eq, @inf_comm _ _ _ aᶜ, inf_liminf]
+
+lemma sdiff_limsup [ne_bot f] (a : α) :
+  a \ limsup u f = liminf (λ b, a \ u b) f :=
+begin
+  rw ← compl_inj_iff,
+  simp only [sdiff_eq, liminf_compl, (∘), compl_inf, compl_compl, sup_limsup],
+end
+
+lemma sdiff_liminf (a : α) :
+  a \ liminf u f = limsup (λ b, a \ u b) f :=
+begin
+  rw ← compl_inj_iff,
+  simp only [sdiff_eq, limsup_compl, (∘), compl_inf, compl_compl, sup_liminf],
+end
+
+end complete_boolean_algebra
+
 section set_lattice
 
 variables {p : ι → Prop} {s : ι → set α}