feat(order/bounds/basic): add is_greatest_univ_iff etc (#18162)

Also add `ae_measurable_const'` and golf 2 proofs.

Author: urkud

src/measure_theory/constructions/borel_space.lean

@@ -1049,51 +1049,32 @@ begin
   exact measurable_set.Union (λ i, hf i (is_open_gt' _).measurable_set)
 end
 
-private lemma ae_measurable.is_glb_of_nonempty {ι} (hι : nonempty ι)
-  {μ : measure δ} [countable ι] {f : ι → δ → α} {g : δ → α}
+lemma ae_measurable.is_glb {ι} {μ : measure δ} [countable ι] {f : ι → δ → α} {g : δ → α}
   (hf : ∀ i, ae_measurable (f i) μ) (hg : ∀ᵐ b ∂μ, is_glb {a | ∃ i, f i b = a} (g b)) :
   ae_measurable g μ :=
 begin
+  nontriviality α,
+  haveI hα : nonempty α := infer_instance,
+  casesI is_empty_or_nonempty ι with hι hι,
+  { simp only [is_empty.exists_iff, set_of_false, is_glb_empty_iff] at hg,
+    exact ae_measurable_const' (hg.mono $ λ a ha, hg.mono $ λ b hb, (hb _).antisymm (ha _)) },
   let p : δ → (ι → α) → Prop := λ x f', is_glb {a | ∃ i, f' i = a} (g x),
-  let g_seq := λ x, ite (x ∈ ae_seq_set hf p) (g x) (⟨g x⟩ : nonempty α).some,
+  let g_seq := (ae_seq_set hf p).piecewise g (λ _, hα.some),
   have hg_seq : ∀ b, is_glb {a | ∃ i, ae_seq hf p i b = a} (g_seq b),
   { intro b,
-    haveI hα : nonempty α := nonempty.map g ⟨b⟩,
-    simp only [ae_seq, g_seq],
+    simp only [ae_seq, g_seq, set.piecewise],
     split_ifs,
     { have h_set_eq : {a : α | ∃ (i : ι), (hf i).mk (f i) b = a} = {a : α | ∃ (i : ι), f i b = a},
       { ext x,
         simp_rw [set.mem_set_of_eq, ae_seq.mk_eq_fun_of_mem_ae_seq_set hf h], },
       rw h_set_eq,
       exact ae_seq.fun_prop_of_mem_ae_seq_set hf h, },
-    { have h_singleton : {a : α | ∃ (i : ι), hα.some = a} = {hα.some},
-      { ext1 x,
-        exact ⟨λ hx, hx.some_spec.symm, λ hx, ⟨hι.some, hx.symm⟩⟩, },
-      rw h_singleton,
-      exact is_glb_singleton, }, },
+    { exact is_least.is_glb ⟨(@exists_const (hα.some = hα.some) ι _).2 rfl, λ x ⟨i, hi⟩, hi.le⟩ } },
   refine ⟨g_seq, measurable.is_glb (ae_seq.measurable hf p) hg_seq, _⟩,
-  exact (ite_ae_eq_of_measure_compl_zero g (λ x, (⟨g x⟩ : nonempty α).some) (ae_seq_set hf p)
+  exact (ite_ae_eq_of_measure_compl_zero g (λ x, hα.some) (ae_seq_set hf p)
     (ae_seq.measure_compl_ae_seq_set_eq_zero hf hg)).symm,
 end
 
-lemma ae_measurable.is_glb {ι} {μ : measure δ} [countable ι] {f : ι → δ → α} {g : δ → α}
-  (hf : ∀ i, ae_measurable (f i) μ) (hg : ∀ᵐ b ∂μ, is_glb {a | ∃ i, f i b = a} (g b)) :
-  ae_measurable g μ :=
-begin
-  by_cases hμ : μ = 0, { rw hμ, exact ae_measurable_zero_measure },
-  haveI : μ.ae.ne_bot, { simpa [ne_bot_iff] },
-  by_cases hι : nonempty ι, { exact ae_measurable.is_glb_of_nonempty hι hf hg, },
-  suffices : ∃ x, g =ᵐ[μ] λ y, g x,
-  by { exact ⟨(λ y, g this.some), measurable_const, this.some_spec⟩, },
-  have h_empty : ∀ x, {a : α | ∃ (i : ι), f i x = a} = ∅,
-  { intro x,
-    ext1 y,
-    rw [set.mem_set_of_eq, set.mem_empty_iff_false, iff_false],
-    exact λ hi, hι (nonempty_of_exists hi), },
-  simp_rw h_empty at hg,
-  exact ⟨hg.exists.some, hg.mono (λ y hy, is_glb.unique hy hg.exists.some_spec)⟩,
-end
-
 protected lemma monotone.measurable [linear_order β] [order_closed_topology β] {f : β → α}
   (hf : monotone f) : measurable f :=
 suffices h : ∀ x, ord_connected (f ⁻¹' Ioi x),

src/measure_theory/measure/ae_measurable.lean

@@ -208,6 +208,15 @@ let ⟨g, hgm, hg⟩ := h in hgm.null_measurable.congr hg.symm
 
 end ae_measurable
 
+lemma ae_measurable_const' (h : ∀ᵐ x y ∂μ, f x = f y) : ae_measurable f μ :=
+begin
+  rcases eq_or_ne μ 0 with rfl | hμ,
+  { exact ae_measurable_zero_measure },
+  { haveI := ae_ne_bot.2 hμ,
+    rcases h.exists with ⟨x, hx⟩,
+    exact ⟨const α (f x), measurable_const, eventually_eq.symm hx⟩ }
+end
+
 lemma ae_measurable_uIoc_iff [linear_order α] {f : α → β} {a b : α} :
   (ae_measurable f $ μ.restrict $ Ι a b) ↔
     (ae_measurable f $ μ.restrict $ Ioc a b) ∧ (ae_measurable f $ μ.restrict $ Ioc b a) :=
@@ -274,18 +283,15 @@ lemma ae_measurable_Ioi_of_forall_Ioc {β} {mβ : measurable_space β}
   ae_measurable g (μ.restrict (Ioi x)) :=
 begin
   haveI : nonempty α := ⟨x⟩,
-  haveI : (at_top : filter α).ne_bot := at_top_ne_bot,
   obtain ⟨u, hu_tendsto⟩ := exists_seq_tendsto (at_top : filter α),
   have Ioi_eq_Union : Ioi x = ⋃ n : ℕ, Ioc x (u n),
   { rw Union_Ioc_eq_Ioi_self_iff.mpr _,
-    rw tendsto_at_top_at_top at hu_tendsto,
-    exact λ y _, ⟨(hu_tendsto y).some, (hu_tendsto y).some_spec (hu_tendsto y).some le_rfl⟩, },
+    exact λ y _, (hu_tendsto.eventually (eventually_ge_at_top y)).exists },
   rw [Ioi_eq_Union, ae_measurable_Union_iff],
   intros n,
   cases lt_or_le x (u n),
   { exact g_meas (u n) h, },
-  { rw Ioc_eq_empty (not_lt.mpr h),
-    simp only [measure.restrict_empty],
+  { rw [Ioc_eq_empty (not_lt.mpr h), measure.restrict_empty],
     exact ae_measurable_zero_measure, },
 end
 

src/order/bounds/basic.lean

@@ -571,25 +571,25 @@ by simp only [Ici_inter_Iic.symm, subset_inter_iff, bdd_below_iff_subset_Ici,
 #### Univ
 -/
 
-lemma is_greatest_univ [preorder γ] [order_top γ] : is_greatest (univ : set γ) ⊤ :=
-⟨mem_univ _, λ x hx, le_top⟩
+@[simp] lemma is_greatest_univ_iff : is_greatest univ a ↔ is_top a :=
+by simp [is_greatest, mem_upper_bounds, is_top]
+
+lemma is_greatest_univ [order_top α] : is_greatest (univ : set α) ⊤ :=
+is_greatest_univ_iff.2 is_top_top
 
 @[simp] lemma order_top.upper_bounds_univ [partial_order γ] [order_top γ] :
   upper_bounds (univ : set γ) = {⊤} :=
 by rw [is_greatest_univ.upper_bounds_eq, Ici_top]
 
-lemma is_lub_univ [preorder γ] [order_top γ] : is_lub (univ : set γ) ⊤ :=
-is_greatest_univ.is_lub
+lemma is_lub_univ [order_top α] : is_lub (univ : set α) ⊤ := is_greatest_univ.is_lub
 
 @[simp] lemma order_bot.lower_bounds_univ [partial_order γ] [order_bot γ] :
   lower_bounds (univ : set γ) = {⊥} :=
 @order_top.upper_bounds_univ γᵒᵈ _ _
 
-lemma is_least_univ [preorder γ] [order_bot γ] : is_least (univ : set γ) ⊥ :=
-@is_greatest_univ γᵒᵈ _ _
-
-lemma is_glb_univ [preorder γ] [order_bot γ] : is_glb (univ : set γ) ⊥ :=
-is_least_univ.is_glb
+@[simp] lemma is_least_univ_iff : is_least univ a ↔ is_bot a := @is_greatest_univ_iff αᵒᵈ _ _
+lemma is_least_univ [order_bot α] : is_least (univ : set α) ⊥ := @is_greatest_univ αᵒᵈ _ _
+lemma is_glb_univ [order_bot α] : is_glb (univ : set α) ⊥ := is_least_univ.is_glb
 
 @[simp] lemma no_max_order.upper_bounds_univ [no_max_order α] : upper_bounds (univ : set α) = ∅ :=
 eq_empty_of_subset_empty $ λ b hb, let ⟨x, hx⟩ := exists_gt b in
@@ -619,10 +619,11 @@ by simp only [bdd_above, upper_bounds_empty, univ_nonempty]
 @[simp] lemma bdd_below_empty [nonempty α] : bdd_below (∅ : set α) :=
 by simp only [bdd_below, lower_bounds_empty, univ_nonempty]
 
-lemma is_glb_empty [preorder γ] [order_top γ] : is_glb ∅ (⊤:γ) :=
-by simp only [is_glb, lower_bounds_empty, is_greatest_univ]
+@[simp] lemma is_glb_empty_iff : is_glb ∅ a ↔ is_top a := by simp [is_glb]
+@[simp] lemma is_lub_empty_iff : is_lub ∅ a ↔ is_bot a := @is_glb_empty_iff αᵒᵈ _ _
 
-lemma is_lub_empty [preorder γ] [order_bot γ] : is_lub ∅ (⊥:γ) := @is_glb_empty γᵒᵈ _ _
+lemma is_glb_empty [order_top α] : is_glb ∅ (⊤:α) := is_glb_empty_iff.2 is_top_top
+lemma is_lub_empty [order_bot α] : is_lub ∅ (⊥:α) := @is_glb_empty αᵒᵈ _ _
 
 lemma is_lub.nonempty [no_min_order α] (hs : is_lub s a) : s.nonempty :=
 let ⟨a', ha'⟩ := exists_lt a in
@@ -683,11 +684,11 @@ by rw [insert_eq, upper_bounds_union, upper_bounds_singleton]
 by rw [insert_eq, lower_bounds_union, lower_bounds_singleton]
 
 /-- When there is a global maximum, every set is bounded above. -/
-@[simp] protected lemma order_top.bdd_above [preorder γ] [order_top γ] (s : set γ) : bdd_above s :=
+@[simp] protected lemma order_top.bdd_above [order_top α] (s : set α) : bdd_above s :=
 ⟨⊤, λ a ha, order_top.le_top a⟩
 
 /-- When there is a global minimum, every set is bounded below. -/
-@[simp] protected lemma order_bot.bdd_below [preorder γ] [order_bot γ] (s : set γ) : bdd_below s :=
+@[simp] protected lemma order_bot.bdd_below [order_bot α] (s : set α) : bdd_below s :=
 ⟨⊥, λ a ha, order_bot.bot_le a⟩
 
 /-!