From e327f7e465f7fa094562c967d7dd16f2ad89527b Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 23 Aug 2023 00:07:24 +0900
Subject: [PATCH] fixes

---
 CHANGELOG_UNRELEASED.md      | 23 ++++++++++-------------
 theories/lebesgue_integral.v |  7 -------
 2 files changed, 10 insertions(+), 20 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2f4510e49b..515f5c8a16 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -23,18 +23,6 @@
 - in `exp.v`:
   + lemmas `concave_ln`, `conjugate_powR`
 
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_mulrr`
-
-- in `constructive_ereal.v`:
-  + lemma `eqe_pdivr_mull`
-
-- new file `hoelder.v`:
-  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
-  + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
-  + lemma `hoelder`
-
 - in file `lebesgue_integral.v`,
   + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and 
     `lebesgue_differentiation_continuous`.
@@ -51,8 +39,17 @@
 - in file `topology.v`,
   + new definition `regular_space`.
   + new lemma `ent_closure`.
+
+- in `lebesgue_measure.v`:
+  + lemma `measurable_mulrr`
+
+- in `constructive_ereal.v`:
+  + lemma `eqe_pdivr_mull`
+
 - new file `hoelder.v`:
-  + 
+  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
+  + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
+  + lemma `hoelder`
 
 ### Changed
 
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 5b354e6edc..2013f246f6 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -67,13 +67,6 @@ Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
 Reserved Notation "m1 '\x' m2" (at level 40, m2 at next level).
 Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level).
 
-Reserved Notation "'N[ mu ]_  p [ F ]"
-  (at level 5, F at level 36, mu at level 10,
-  format "'[' ''N[' mu ]_ p '/  ' [ F ] ']'").
-Reserved Notation "''N_' p [ F ]" (* for use as a local notation *)
-  (at level 5, F at level 36,
-  format "'[' ''N_' p '/  ' [ F ] ']'").
-
 #[global]
 Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.