From a6d72f6efade3b6e31eec36d5f398ee715edadd6 Mon Sep 17 00:00:00 2001
From: Alessandro Bruni <brun@itu.dk>
Date: Tue, 22 Oct 2024 10:18:03 +0200
Subject: [PATCH] Added `essential_supremum_ereal` Added documentation and
 changelog

Co-authored-by: @jmmarulang
---
 CHANGELOG_PR_ESS_SUP.md | 22 ++++++++++++++++++++++
 theories/measure.v      | 21 +++++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 CHANGELOG_PR_ESS_SUP.md

diff --git a/CHANGELOG_PR_ESS_SUP.md b/CHANGELOG_PR_ESS_SUP.md
new file mode 100644
index 000000000..f40d3786b
--- /dev/null
+++ b/CHANGELOG_PR_ESS_SUP.md
@@ -0,0 +1,22 @@
+# Changelog (unreleased)
+
+## [Unreleased]
+
+### Added
+- in `measure.v`:
+  + definition `ess_supe`
+  + lemma `ess_supe_ge0`
+
+### Changed
+
+### Renamed
+
+### Generalized
+
+### Deprecated
+
+### Removed
+
+### Infrastructure
+
+### Misc
diff --git a/theories/measure.v b/theories/measure.v
index a00237c84..9dc99d2c4 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -277,6 +277,8 @@ From HB Require Import structures.
 (*  m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1     *)
 (*  ess_sup f == essential supremum of the function f : T -> R where T is a   *)
 (*               semiRingOfSetsType and R is a realType                       *)
+(*  ess_supe f == essential supremum of the function f : T -> \bar R where    *)
+(*                T is a semiRingOfSetsType and R is a realType               *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -5264,3 +5266,22 @@ by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)).
 Qed.
 
 End essential_supremum.
+
+Section essential_supremum_ereal.
+Context d {T : semiRingOfSetsType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Implicit Types f : T -> \bar R.
+
+Definition ess_supe f :=
+  ereal_inf ([set r | mu (f @^-1` `]r, +oo[) = 0]).
+
+Lemma ess_supe_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t) ->
+  0 <= ess_supe f.
+Proof.
+move=> muT f0; apply: lb_ereal_inf.
+by case=> //= [r|] /eqP rf; rewrite leNgt;
+  apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//;
+  apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)).
+Qed.
+
+End essential_supremum_ereal.