diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e1259f514..8764921cb 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -46,12 +46,18 @@
   + definition `locally_integrable`
   + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`,
     `locally_integrableB`
-  + definitions `HL_max`, `HL_maximal`
-  + lemmas `HL_max_ge0`, `HL_maximal_ge0`, `HL_maximalT_ge0`,
+  + definition `iavg`
+  + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD`
+  + definitions `HL_maximal`
+  + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`,
     `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`,
     `maximal_inequality`
 
 ### Changed
+
+- in `normedtype.v`:
+  + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns
+    duplicate-free lists of indices
   
 ### Renamed
 
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 947b727de..09ce1738c 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -47,6 +47,8 @@ Require Import esum measure lebesgue_measure numfun.
 (*                           measure over T2                                  *)
 (* locally_integrable D f == the real number-valued function f is locally     *)
 (*                           integrable on D                                  *)
+(*               iavg f A := "average" of the real-valued function f over     *)
+(*                           the set A                                        *)
 (*             HL_maximal == the Hardy–Littlewood maximal operator            *)
 (*                           input: real number-valued function               *)
 (*                           output: extended real number-valued function     *)