diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c9debd831..697e29672 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -17,6 +17,25 @@
   + lemma `ae_foralln`
   + lemma `ae_eqe_mul2l`
 
+- new file `ess_sup_inf.v`:
+  + lemma `measure0_ae`
+  + definition `ess_esup`
+  + lemmas `ess_supEae`, `ae_le_measureP`, `ess_supEmu0`, `ess_sup_ge`,
+    `ess_supP`, `le_ess_sup`, `eq_ess_sup`, `ess_sup_cst`, `ess_sup_ae_cst`,
+    `ess_sup_gee`, `abs_sup_eq0_ae_eq`, `abs_ess_sup_eq0`, `ess_sup_pZl`,
+    `ess_supZl`, `ess_sup_eqNyP`, `ess_supD`, `ess_sup_absD`
+  + notation `ess_supr`
+  + lemmas `ess_supr_bounded`, `ess_sup_eqr0_ae_eq`, `ess_suprZl`,
+    `ess_sup_ger`, `ess_sup_ler`, `ess_sup_cstr`, `ess_suprD`, `ess_sup_normD`
+  + definition `ess_inf`
+  + lemmas `ess_infEae`, `ess_infEN`, `ess_supEN`, `ess_infN`, `ess_supN`,
+    `ess_infP`, `ess_inf_le`, `le_ess_inf`, `eq_ess_inf`, `ess_inf_cst`,
+    `ess_inf_ae_cst`, `ess_inf_gee`, `ess_inf_pZl`, `ess_infZl`, `ess_inf_eqyP`,
+    `ess_infD`
+  + notation `ess_infr`
+  + lemmas `ess_infr_bounded`, `ess_infrZl`, `ess_inf_ger`, `ess_inf_ler`,
+    `ess_inf_cstr`
+
 ### Changed
 
 - in `measure.v`:
@@ -26,6 +45,9 @@
 
 ### Renamed
 
+- in `measure.v`
+  + definition `ess_sup` moved to `ess_sup_inf.v`
+
 ### Generalized
 
 ### Deprecated
@@ -34,6 +56,7 @@
 
 - in `measure.v`:
   + definition `almost_everywhere_notation`
+  + lemma `ess_sup_ge0`
 
 ### Infrastructure
 
diff --git a/_CoqProject b/_CoqProject
index 29135cf9d..4bd2a3f29 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -69,6 +69,7 @@ theories/homotopy_theory/homotopy.v
 theories/homotopy_theory/wedge_sigT.v
 theories/homotopy_theory/continuous_path.v
 
+theories/ess_sup_inf.v
 theories/function_spaces.v
 theories/ereal.v
 theories/cantor.v
diff --git a/theories/Make b/theories/Make
index 31a7ae13f..c9088359b 100644
--- a/theories/Make
+++ b/theories/Make
@@ -35,6 +35,7 @@ homotopy_theory/homotopy.v
 homotopy_theory/wedge_sigT.v
 homotopy_theory/continuous_path.v
 
+ess_sup_inf.v
 function_spaces.v
 cantor.v
 tvs.v
diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v
new file mode 100644
index 000000000..b477a35ae
--- /dev/null
+++ b/theories/ess_sup_inf.v
@@ -0,0 +1,367 @@
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop reals interval_inference ereal.
+From mathcomp Require Import topology normedtype sequences esum numfun.
+From mathcomp Require Import measure lebesgue_measure.
+
+(**md**************************************************************************)
+(* # Essential infimum and essential supremum                                 *)
+(*                                                                            *)
+(* ```                                                                        *)
+(*  ess_sup f == essential supremum of the function f : T -> R where T is a   *)
+(*               semiRingOfSetsType and R is a realType                       *)
+(*  ess_inf f == essential infimum                                            *)
+(* ```                                                                        *)
+(*                                                                            *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldNormedType.Exports.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+Local Open Scope ereal_scope.
+
+Section essential_supremum.
+Context d {T : semiRingOfSetsType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Type f : T -> \bar R.
+
+Definition ess_sup f := ereal_inf [set y | \forall x \ae mu, f x <= y].
+
+Lemma ess_supEae f : ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y].
+Proof. by []. Qed.
+
+End essential_supremum.
+
+Section essential_supremum_lemmas.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types (f g : T -> \bar R) (h k : T -> R) (x y : \bar R) (r : R).
+
+(* NB: note that this lemma does not depends on the new definitions introduced
+   in this file and might be move earlier in the file hierarchy later *)
+Lemma ae_le_measureP f y : measurable_fun [set: T] f ->
+  (\forall x \ae mu, f x <= y) <-> mu (f @^-1` `]y, +oo[) = 0.
+Proof.
+move=> f_meas; have fVroo_meas : d.-measurable (f @^-1` `]y, +oo[).
+  by rewrite -[_ @^-1` _]setTI; apply/f_meas=> //; exact/emeasurable_itv.
+have setCfVroo : f @^-1` `]y, +oo[ = ~` [set x | f x <= y].
+  by apply: setC_inj; rewrite preimage_setC setCitv/= set_itvxx setU0 setCK.
+split.
+  move=> [N [dN muN0 inN]]; rewrite (subset_measure0 _ dN)// => x.
+  by rewrite setCfVroo; apply: inN.
+set N := (X in mu X) => muN0; exists N; rewrite -setCfVroo.
+by split => //; exact: fVroo_meas.
+Qed.
+
+Local Notation ess_sup := (ess_sup mu).
+
+Lemma ess_supEmu0 f : measurable_fun [set: T] f ->
+   ess_sup f = ereal_inf [set y | mu (f @^-1` `]y, +oo[) = 0].
+Proof.
+by move=> ?; congr (ereal_inf _); apply/predeqP => r; exact: ae_le_measureP.
+Qed.
+
+Lemma ess_sup_ge f : \forall x \ae mu, f x <= ess_sup f.
+Proof.
+rewrite ess_supEae//; set I := (X in ereal_inf X).
+have [->|IN0] := eqVneq I set0.
+  by rewrite ereal_inf0; apply: nearW => ?; rewrite leey.
+have [u uI uinf] := ereal_inf_seq IN0.
+rewrite -(cvg_lim _ uinf)//; near=> x.
+rewrite lime_ge//; first by apply/cvgP: uinf.
+by apply: nearW; near: x; apply/ae_foralln => n; apply: uI.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_supP f y : reflect (\forall x \ae mu, f x <= y) (ess_sup f <= y).
+Proof.
+apply: (iffP (ereal_inf_leP _)) => /=; last 2 first.
+- by move=> [z fz zy]; near do apply: le_trans zy.
+- by move=> fy; exists y.
+by rewrite -ess_supEae//; exact: ess_sup_ge.
+Unshelve. all: by end_near. Qed.
+
+Lemma le_ess_sup f g : (\forall x \ae mu, f x <= g x) -> ess_sup f <= ess_sup g.
+Proof.
+move=> fg; apply/ess_supP => //.
+near do rewrite (le_trans (near fg _ _))//=.
+exact: ess_sup_ge.
+Unshelve. all: by end_near. Qed.
+
+Lemma eq_ess_sup f g : (\forall x \ae mu, f x = g x) -> ess_sup f = ess_sup g.
+Proof.
+move=> fg; apply/eqP; rewrite eq_le !le_ess_sup//=;
+  by apply: filterS fg => x ->.
+Qed.
+
+Lemma ess_sup_cst x : 0 < mu [set: T] -> ess_sup (cst x) = x.
+Proof.
+move=> muT_gt0; apply/eqP; rewrite eq_le; apply/andP; split.
+  by apply/ess_supP => //; apply: nearW.
+have ae_proper := ae_properfilter_algebraOfSetsType muT_gt0.
+by near (almost_everywhere mu) => y; near: y; apply: ess_sup_ge.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_ae_cst f y : 0 < mu [set: T] ->
+  (\forall x \ae mu, f x = y) -> ess_sup f = y.
+Proof. by move=> muT_gt0 /= /eq_ess_sup->; rewrite ess_sup_cst. Qed.
+
+Lemma ess_sup_gee f a : 0 < mu [set: T] ->
+  (\forall x \ae mu, a <= f x) -> a <= ess_sup f.
+Proof. by move=> *; rewrite -(ess_sup_cst a)//; apply: le_ess_sup. Qed.
+
+Lemma abs_sup_eq0_ae_eq f : ess_sup (abse \o f) = 0 -> f = \0 %[ae mu].
+Proof.
+move=> ess_sup_f_eq0; near=> x => _ /=; apply/eqP.
+rewrite -abse_eq0 eq_le abse_ge0 andbT; near: x.
+by apply/ess_supP; rewrite ess_sup_f_eq0.
+Unshelve. all: by end_near. Qed.
+
+Lemma abs_ess_sup_eq0 f : mu [set: T] > 0 ->
+  f = \0 %[ae mu] -> ess_sup (abse \o f) = 0.
+Proof.
+move=> muT_gt0 f0; apply/eqP; rewrite eq_le; apply/andP; split.
+  by apply/ess_supP => /=; near do rewrite (near f0 _ _)//= normr0//.
+by rewrite -[0]ess_sup_cst// le_ess_sup//=; near=> x; rewrite abse_ge0.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_pZl f r : (0 < r)%R ->
+  ess_sup (cst r%:E \* f) = r%:E * ess_sup f.
+Proof.
+move=> /[dup] /ltW r_ge0 r_gt0.
+gen have esc_le : r f r_ge0 r_gt0 /
+    ess_sup (cst r%:E \* f) <= r%:E * ess_sup f.
+  by apply/ess_supP; near do rewrite /cst/= lee_pmul2l//; apply/ess_supP.
+apply/eqP; rewrite eq_le esc_le// -lee_pdivlMl//=.
+apply: le_trans (esc_le _ _ _ _); rewrite ?invr_gt0 ?invr_ge0//.
+by under eq_fun do rewrite muleA -EFinM mulVf ?mul1e ?gt_eqF//.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_supZl f r : mu [set: T] > 0 -> (0 <= r)%R ->
+  ess_sup (cst r%:E \* f) = r%:E * ess_sup f.
+Proof.
+move=> muTN0; case: ltgtP => // [r_gt0|<-] _; first exact: ess_sup_pZl.
+by under eq_fun do rewrite mul0e; rewrite mul0e ess_sup_cst.
+Qed.
+
+Lemma ess_sup_eqNyP f : ess_sup f = -oo <-> \forall x \ae mu, f x = -oo.
+Proof.
+rewrite (rwP eqP) -leeNy_eq (eq_near (fun=> rwP eqP)).
+by under eq_near do rewrite -leeNy_eq; apply/(rwP2 idP (ess_supP _ _)).
+Qed.
+
+Lemma ess_supD f g : ess_sup (f \+ g) <= ess_sup f + ess_sup g.
+Proof.
+by apply/ess_supP; near do rewrite leeD//; apply/ess_supP.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_absD f g :
+  ess_sup (abse \o (f \+ g)) <= ess_sup (abse \o f) + ess_sup (abse \o g).
+Proof.
+rewrite (le_trans _ (ess_supD _ _))// le_ess_sup//.
+by apply/nearW => x; apply/lee_abs_add.
+Qed.
+
+End essential_supremum_lemmas.
+Arguments ess_sup_ae_cst {d T R mu f}.
+Arguments ess_supP {d T R mu f y}.
+
+Section real_essential_supremum.
+Context d {T : semiRingOfSetsType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types f : T -> R.
+
+Notation ess_supr f := (ess_sup mu (EFin \o f)).
+
+End real_essential_supremum.
+
+Section real_essential_supremum_lemmas.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types (f : T -> R) (r : R).
+
+Notation ess_supr f := (ess_sup mu (EFin \o f)).
+
+Lemma ess_supr_bounded f : ess_supr f < +oo ->
+  exists M, \forall x \ae mu, (f x <= M)%R.
+Proof.
+set g := EFin \o f => ltfy; have [|supfNy] := eqVneq (ess_sup mu g) -oo.
+  by move=> /ess_sup_eqNyP fNy; exists 0%:R; apply: filterS fNy.
+have supf_fin : ess_supr f \is a fin_num by case: ess_sup ltfy supfNy.
+by exists (fine (ess_supr f)); near do rewrite -lee_fin fineK//; apply/ess_supP.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_sup_eqr0_ae_eq f : ess_supr (normr \o f) = 0 -> f = 0%R %[ae mu].
+Proof.
+under [X in ess_sup _ X]eq_fun do rewrite /= -abse_EFin.
+move=> /abs_sup_eq0_ae_eq; apply: filterS => x /= /(_ _)/eqP.
+by rewrite eqe => /(_ _)/eqP.
+Qed.
+
+Lemma ess_suprZl f r : mu [set: T] > 0 -> (0 <= r)%R ->
+  ess_supr (cst r \* f)%R = r%:E * ess_supr f.
+Proof. by move=> muT_gt0 r_ge0; rewrite -ess_supZl. Qed.
+
+Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) ->
+  x <= ess_supr f.
+Proof. by move=> muT f0; apply/ess_sup_gee => //=; apply: nearW. Qed.
+
+Lemma ess_sup_ler f y : (forall t, (f t)%:E <= y) -> ess_supr f <= y.
+Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed.
+
+Lemma ess_sup_cstr y : 0 < mu [set: T] -> ess_supr (cst y) = y%:E.
+Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed.
+
+Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g.
+Proof. by rewrite (le_trans _ (ess_supD _ _ _)). Qed.
+
+Lemma ess_sup_normD f g :
+  ess_supr (normr \o (f \+ g)) <= ess_supr (normr \o f) + ess_supr (normr \o g).
+Proof.
+rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//.
+by apply/nearW => x; apply/ler_normD.
+Qed.
+
+End real_essential_supremum_lemmas.
+Notation ess_supr mu f := (ess_sup mu (EFin \o f)).
+
+Section essential_infimum.
+Context d {T : semiRingOfSetsType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types f : T -> \bar R.
+
+Definition ess_inf f := ereal_sup [set y | \forall x \ae mu, y <= f x].
+
+Lemma ess_infEae f : ess_inf f = ereal_sup [set y | \forall x \ae mu, y <= f x].
+Proof. by []. Qed.
+
+End essential_infimum.
+
+Section essential_infimum_lemmas.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types (f : T -> \bar R) (x y : \bar R) (r : R).
+
+Local Notation ess_inf := (ess_inf mu).
+Local Notation ess_sup := (ess_sup mu).
+
+Lemma ess_infEN f : ess_inf f = - ess_sup (\- f).
+Proof.
+rewrite ess_supEae ess_infEae ereal_infEN oppeK; congr (ereal_sup _).
+apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]].
+  by exists (- y); rewrite ?oppeK//=; apply: filterS y_le => x; rewrite leeN2.
+by apply: filterS y_ge => x; rewrite leeNl.
+Qed.
+
+Lemma ess_supEN f : ess_sup f = - ess_inf (\- f).
+Proof.
+by rewrite ess_infEN oppeK; apply/eq_ess_sup/nearW => ?; rewrite oppeK.
+Qed.
+
+Lemma ess_infN f : ess_inf (\- f) = - ess_sup f.
+Proof. by rewrite ess_supEN oppeK. Qed.
+
+Lemma ess_supN f : ess_sup (\- f) = - ess_inf f.
+Proof. by rewrite ess_infEN oppeK. Qed.
+
+Lemma ess_infP f y : reflect (\forall x \ae mu, y <= f x) (y <= ess_inf f).
+Proof.
+by rewrite ess_infEN leeNr; apply: (iffP ess_supP);
+   apply: filterS => x; rewrite leeN2.
+Qed.
+
+Lemma ess_inf_le f : \forall x \ae mu, ess_inf f <= f x.
+Proof. exact/ess_infP. Qed.
+
+Lemma le_ess_inf f g : (\forall x \ae mu, f x <= g x) -> ess_inf f <= ess_inf g.
+Proof.
+move=> fg; apply/ess_infP => //.
+near do rewrite (le_trans _ (near fg _ _))//=.
+exact: ess_inf_le.
+Unshelve. all: by end_near. Qed.
+
+Lemma eq_ess_inf f g : (\forall x \ae mu, f x = g x) -> ess_inf f = ess_inf g.
+Proof.
+move=> fg; apply/eqP; rewrite eq_le !le_ess_inf//=;
+  by apply: filterS fg => x ->.
+Qed.
+
+Lemma ess_inf_cst x : 0 < mu [set: T] -> ess_inf (cst x) = x.
+Proof.
+by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- x)) ?oppeK//=; apply: nearW.
+Qed.
+
+Lemma ess_inf_ae_cst f y : 0 < mu [set: T] ->
+  (\forall x \ae mu, f x = y) -> ess_inf f = y.
+Proof. by move=> muT_gt0 /= /eq_ess_inf->; rewrite ess_inf_cst. Qed.
+
+Lemma ess_inf_gee f y : 0 < mu [set: T] ->
+  (\forall x \ae mu, y <= f x) -> y <= ess_inf f.
+Proof. by move=> *; rewrite -(ess_inf_cst y)//; apply: le_ess_inf. Qed.
+
+Lemma ess_inf_pZl f r : (0 < r)%R -> ess_inf (cst r%:E \* f) = r%:E * ess_inf f.
+Proof.
+move=> r_gt0; rewrite !ess_infEN muleN; congr (- _).
+by under eq_fun do rewrite -muleN; rewrite ess_sup_pZl.
+Qed.
+
+Lemma ess_infZl f r : mu [set: T] > 0 -> (0 <= r)%R ->
+  ess_inf (cst r%:E \* f) = r%:E * ess_inf f.
+Proof.
+move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_inf_pZl.
+by under eq_fun do rewrite mul0e; rewrite mul0e ess_inf_cst.
+Qed.
+
+Lemma ess_inf_eqyP f : ess_inf f = +oo <-> \forall x \ae mu, f x = +oo.
+Proof.
+rewrite (rwP eqP) -leye_eq (eq_near (fun=> rwP eqP)).
+by under eq_near do rewrite -leye_eq; apply/(rwP2 idP (ess_infP _ _)).
+Qed.
+
+Lemma ess_infD f g : ess_inf (f \+ g) >= ess_inf f + ess_inf g.
+Proof.
+by apply/ess_infP; near do rewrite leeD//; apply/ess_infP.
+Unshelve. all: by end_near. Qed.
+
+End essential_infimum_lemmas.
+Arguments ess_inf_ae_cst {d T R mu f}.
+Arguments ess_infP {d T R mu f y}.
+
+Section real_essential_infimum.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types (f : T -> R) (x : \bar R) (r : R).
+
+Notation ess_infr f := (ess_inf mu (EFin \o f)).
+
+Lemma ess_infr_bounded f : ess_infr f > -oo ->
+  exists M, \forall x \ae mu, (f x >= M)%R.
+Proof.
+set g := EFin \o f => ltfy; have [|inffNy] := eqVneq (ess_inf mu g) +oo.
+  by move=> /ess_inf_eqyP fNy; exists 0%:R; apply: filterS fNy.
+have inff_fin : ess_infr f \is a fin_num by case: ess_inf ltfy inffNy.
+by exists (fine (ess_infr f)); near do rewrite -lee_fin fineK//; apply/ess_infP.
+Unshelve. all: by end_near. Qed.
+
+Lemma ess_infrZl f r : mu [set: T] > 0 -> (0 <= r)%R ->
+  ess_infr (cst r \* f)%R = r%:E * ess_infr f.
+Proof. by move=> muT_gt0 r_ge0; rewrite -ess_infZl. Qed.
+
+Lemma ess_inf_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) ->
+  x <= ess_infr f.
+Proof. by move=> muT f0; apply/ess_inf_gee => //=; apply: nearW. Qed.
+
+Lemma ess_inf_ler f x : (forall t, x <= (f t)%:E) -> x <= ess_infr f.
+Proof. by move=> ?; apply/ess_infP; apply: nearW. Qed.
+
+Lemma ess_inf_cstr r : 0 < mu [set: T] -> ess_infr (cst r) = r%:E.
+Proof. by move=> muN0; rewrite (ess_inf_ae_cst r%:E)//=; apply: nearW. Qed.
+
+End real_essential_infimum.
+Notation ess_infr mu f := (ess_inf mu (EFin \o f)).
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 06385c4ac..d5dca2a07 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
 From mathcomp Require Import functions cardinality fsbigop reals ereal.
 From mathcomp Require Import topology normedtype sequences real_interval.
 From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral.
-From mathcomp Require Import numfun exp convex interval_inference.
+From mathcomp Require Import numfun exp convex interval_inference ess_sup_inf.
 
 (**md**************************************************************************)
 (* # Hoelder's Inequality                                                     *)
@@ -43,7 +43,7 @@ HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType}
               mu (f @^-1` (setT `\ 0%R))
             else
               (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E
-  | +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E
+  | +oo%E => (if mu [set: T] > 0 then ess_supr mu (normr \o f) else 0)%E
   | -oo%E => 0%E
   end.
 Canonical locked_Lnorm := Unlockable Lnorm.unlock.
@@ -68,7 +68,7 @@ Lemma Lnorm_ge0 p f : 0 <= 'N_p[f].
 Proof.
 rewrite unlock; move: p => [r/=|/=|//].
   by case: ifPn => // r0; exact: poweR_ge0.
-by case: ifPn => // /ess_sup_ge0; apply => t/=.
+by case: ifPn => // /ess_sup_ger; apply => t/=.
 Qed.
 
 Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g].
diff --git a/theories/measure.v b/theories/measure.v
index 836009a40..f1aaa5ccf 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -4160,14 +4160,21 @@ Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope.
 Notation "\forall x \ae mu , P" := (\forall x \near almost_everywhere mu, P)
   (format "\forall  x  \ae  mu ,  P",
   x name, P at level 200, at level 200): type_scope.
-Definition ae_eq d (T : semiRingOfSetsType d) (R : realType) (mu : {measure set T -> \bar R})
-  (V : T -> Type) D (f g : forall x, V x) := (\forall x \ae mu, D x -> f x = g x).
+Definition ae_eq d (T : semiRingOfSetsType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (V : T -> Type) D (f g : forall x, V x) :=
+  \forall x \ae mu, D x -> f x = g x.
 Notation "f = g %[ae mu 'in' D ]" := (\forall x \ae mu, D x -> f x = g x)
-  (format "f  =  g  '%[ae'  mu  'in'  D ]", g at next level, D at level 200, at level 70).
+  (format "f  =  g  '%[ae'  mu  'in'  D ]",
+   g at next level, D at level 200, at level 70).
 Notation "f = g %[ae mu ]" := (f = g %[ae mu in setT ])
   (format "f  =  g  '%[ae'  mu ]", g at next level, at level 70).
 
-Lemma aeW {d} {T : ringOfSetsType d} {R : realFieldType}
+Lemma measure0_ae d {T : algebraOfSetsType d} {R : realType}
+    (mu : {measure set T -> \bar R}) (P : set T) :
+  mu [set: T] = 0 -> \forall x \ae mu, P x.
+Proof. by move=> x; exists setT. Qed.
+
+Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType}
     (mu : {measure set _ -> \bar R}) (P : T -> Prop) :
   (forall x, P x) -> \forall x \ae mu, P x.
 Proof.
@@ -5421,21 +5428,3 @@ Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E ->
 Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed.
 
 End absolute_continuity_lemmas.
-
-Section essential_supremum.
-Context d {T : semiRingOfSetsType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Implicit Types f : T -> R.
-
-Definition ess_sup f :=
-  ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]).
-
-Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R ->
-  0 <= ess_sup f.
-Proof.
-move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP rf <-]; rewrite leNgt.
-apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//.
-by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)).
-Qed.
-
-End essential_supremum.