feat(measure_theory/ess_sup): monotonicity of ess_sup/ess_inf w.r.t. …

…the measure (#7917)

src/measure_theory/ess_sup.lean

@@ -26,7 +26,7 @@ sense). We do not define that quantity here, which is simply the supremum of a m
 * `ess_inf f μ := μ.ae.liminf f`
 -/
 
-open measure_theory
+open measure_theory filter
 open_locale ennreal
 
 variables {α β : Type*} [measurable_space α] {μ : measure α}
@@ -43,7 +43,7 @@ def ess_sup (f : α → β) (μ : measure α) := μ.ae.limsup f
 def ess_inf (f : α → β) (μ : measure α) := μ.ae.liminf f
 
 lemma ess_sup_congr_ae {f g : α → β} (hfg : f =ᵐ[μ] g) : ess_sup f μ = ess_sup g μ :=
-filter.limsup_congr hfg
+limsup_congr hfg
 
 lemma ess_inf_congr_ae {f g : α → β} (hfg : f =ᵐ[μ] g) :  ess_inf f μ = ess_inf g μ :=
 @ess_sup_congr_ae α (order_dual β) _ _ _ _ _ hfg
@@ -54,45 +54,70 @@ section complete_lattice
 variable [complete_lattice β]
 
 @[simp] lemma ess_sup_measure_zero {f : α → β} : ess_sup f 0 = ⊥ :=
-le_bot_iff.mp (Inf_le (by simp [set.mem_set_of_eq, filter.eventually_le, ae_iff]))
+le_bot_iff.mp (Inf_le (by simp [set.mem_set_of_eq, eventually_le, ae_iff]))
 
 @[simp] lemma ess_inf_measure_zero {f : α → β} : ess_inf f 0 = ⊤ :=
 @ess_sup_measure_zero α (order_dual β) _ _ _
 
 lemma ess_sup_mono_ae {f g : α → β} (hfg : f ≤ᵐ[μ] g) : ess_sup f μ ≤ ess_sup g μ :=
-filter.limsup_le_limsup hfg
+limsup_le_limsup hfg
 
 lemma ess_inf_mono_ae {f g : α → β} (hfg : f ≤ᵐ[μ] g) : ess_inf f μ ≤ ess_inf g μ :=
-filter.liminf_le_liminf hfg
+liminf_le_liminf hfg
 
 lemma ess_sup_const (c : β) (hμ : μ ≠ 0) : ess_sup (λ x : α, c) μ = c :=
 begin
-  haveI hμ_ne_bot : μ.ae.ne_bot := by rwa [filter.ne_bot_iff, ne.def, ae_eq_bot],
-  exact filter.limsup_const c,
+  haveI hμ_ne_bot : μ.ae.ne_bot := by rwa [ne_bot_iff, ne.def, ae_eq_bot],
+  exact limsup_const c,
+end
+
+lemma ess_sup_le_of_ae_le {f : α → β} (c : β) (hf : f ≤ᵐ[μ] (λ _, c)) : ess_sup f μ ≤ c :=
+begin
+  refine (ess_sup_mono_ae hf).trans _,
+  by_cases hμ : μ = 0,
+  { simp [hμ], },
+  { rwa ess_sup_const, },
 end
 
 lemma ess_inf_const (c : β) (hμ : μ ≠ 0) : ess_inf (λ x : α, c) μ = c :=
 @ess_sup_const α (order_dual β) _ _ _ _ hμ
 
+lemma le_ess_inf_of_ae_le {f : α → β} (c : β) (hf : (λ _, c) ≤ᵐ[μ] f) : c ≤ ess_inf f μ :=
+@ess_sup_le_of_ae_le α (order_dual β) _ _ _ _ c hf
+
 lemma ess_sup_const_bot : ess_sup (λ x : α, (⊥ : β)) μ = (⊥ : β) :=
-filter.limsup_const_bot
+limsup_const_bot
 
 lemma ess_inf_const_top : ess_inf (λ x : α, (⊤ : β)) μ = (⊤ : β) :=
-filter.liminf_const_top
+liminf_const_top
 
 lemma order_iso.ess_sup_apply {γ} [complete_lattice γ] (f : α → β) (μ : measure α)
   (g : β ≃o γ) :
   g (ess_sup f μ) = ess_sup (λ x, g (f x)) μ :=
 begin
   refine order_iso.limsup_apply g _ _ _ _,
-  all_goals { by filter.is_bounded_default},
+  all_goals { is_bounded_default, },
 end
 
 lemma order_iso.ess_inf_apply {γ} [complete_lattice γ] (f : α → β) (μ : measure α)
   (g : β ≃o γ) :
   g (ess_inf f μ) = ess_inf (λ x, g (f x)) μ :=
 @order_iso.ess_sup_apply α (order_dual β) _ _  (order_dual γ) _ _ _ g.dual
 
+lemma ess_sup_mono_measure {f : α → β} {μ ν : measure α} (hμν : ν ≪ μ) :
+  ess_sup f ν ≤ ess_sup f μ :=
+begin
+  refine limsup_le_limsup_of_le (measure.ae_le_iff_absolutely_continuous.mpr hμν) _ _,
+  all_goals { is_bounded_default, },
+end
+
+lemma ess_inf_antimono_measure {f : α → β} {μ ν : measure α} (hμν : μ ≪ ν) :
+  ess_inf f ν ≤ ess_inf f μ :=
+begin
+  refine liminf_le_liminf_of_le (measure.ae_le_iff_absolutely_continuous.mpr hμν) _ _,
+  all_goals { is_bounded_default, },
+end
+
 end complete_lattice
 
 section complete_linear_order
@@ -108,22 +133,22 @@ end complete_linear_order
 
 namespace ennreal
 
+variables {f : α → ℝ≥0∞}
+
 lemma ae_le_ess_sup (f : α → ℝ≥0∞) : ∀ᵐ y ∂μ, f y ≤ ess_sup f μ :=
 eventually_le_limsup f
 
-@[simp] lemma ess_sup_eq_zero_iff {f : α → ℝ≥0∞} : ess_sup f μ = 0 ↔ f =ᵐ[μ] 0 :=
+@[simp] lemma ess_sup_eq_zero_iff : ess_sup f μ = 0 ↔ f =ᵐ[μ] 0 :=
 limsup_eq_zero_iff
 
-lemma ess_sup_const_mul {f : α → ℝ≥0∞} {a : ℝ≥0∞} :
-  ess_sup (λ (x : α), a * (f x)) μ = a * ess_sup f μ :=
+lemma ess_sup_const_mul {a : ℝ≥0∞} : ess_sup (λ (x : α), a * (f x)) μ = a * ess_sup f μ :=
 limsup_const_mul
 
 lemma ess_sup_add_le (f g : α → ℝ≥0∞) : ess_sup (f + g) μ ≤ ess_sup f μ + ess_sup g μ :=
 limsup_add_le f g
 
 lemma ess_sup_liminf_le {ι} [encodable ι] [linear_order ι] (f : ι → α → ℝ≥0∞) :
-  ess_sup (λ x, filter.at_top.liminf (λ n, f n x)) μ
-    ≤ filter.at_top.liminf (λ n, ess_sup (λ x, f n x) μ) :=
+  ess_sup (λ x, at_top.liminf (λ n, f n x)) μ ≤ at_top.liminf (λ n, ess_sup (λ x, f n x) μ) :=
 by { simp_rw ess_sup, exact ennreal.limsup_liminf_le_liminf_limsup (λ a b, f b a), }
 
 end ennreal

src/order/liminf_limsup.lean

@@ -281,6 +281,18 @@ lemma liminf_le_liminf {α : Type*} [conditionally_complete_lattice β] {f : fil
   f.liminf u ≤ f.liminf v :=
 @limsup_le_limsup (order_dual β) α _ _ _ _ h hv hu
 
+lemma limsup_le_limsup_of_le {α β} [conditionally_complete_lattice β] {f g : filter α} (h : f ≤ g)
+  {u : α → β} (hf : f.is_cobounded_under (≤) u . is_bounded_default)
+  (hg : g.is_bounded_under (≤) u . is_bounded_default) :
+  f.limsup u ≤ g.limsup u :=
+Limsup_le_Limsup_of_le (map_mono h) hf hg
+
+lemma liminf_le_liminf_of_le {α β} [conditionally_complete_lattice β] {f g : filter α} (h : g ≤ f)
+  {u : α → β} (hf : f.is_bounded_under (≥) u . is_bounded_default)
+  (hg : g.is_cobounded_under (≥) u . is_bounded_default) :
+  f.liminf u ≤ g.liminf u :=
+Liminf_le_Liminf_of_le (map_mono h) hf hg
+
 theorem Limsup_principal {s : set α} (h : bdd_above s) (hs : s.nonempty) :
   (𝓟 s).Limsup = Sup s :=
 by simp [Limsup]; exact cInf_upper_bounds_eq_cSup h hs