From e4eb08cd579f49917c5694b0e55b36aee5098fa2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 17 Aug 2023 17:29:42 +0900 Subject: [PATCH] fix changelog --- CHANGELOG_UNRELEASED.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0576b04f34..74325bee69 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -30,14 +30,11 @@ - in `constructive_ereal.v`: + lemma `eqe_pdivr_mull` -- in `lebesgue_integral.v`: - + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `|| f ||_p `` +- 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` -- new file `hoelder.v`: - + - ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized