diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 15dd9a1e68..0020e71e4f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -13,6 +13,39 @@
 - in `lebesgue_integral.v`:
   + `sigma_finite_measure` instance on product measure `\x`
 
+- in file `normedtype.v`,
+  + new lemma `continuous_within_itvP`.
+
+- in file `realfun.v`,
+  + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, 
+    `variation`, `variations`, `bounded_variation`, `total_variation`, 
+    `neg_tv`, and `pos_tv`.
+
+  + new lemmas `left_right_continuousP`, `nondecreasing_funN`, 
+    `nonincreasing_funN`, `has_ubound_ereal_sup`, `sup_le`, `ereal_supy`, 
+    `path_lt_filter0`, `path_lt_filterT`, `last_filter_lt`, `last_filter`, 
+    `path_inv`, `path_lt_le_last`, `itv_partition_nil`, `itv_partition1`, 
+    `itv_partition_cons`, `itv_partitionxx`, `itv_partition_le`, 
+    `itv_partition_tail`, `itv_partition_cat`, `itv_partition_nth_size`, 
+    `itv_partition_nth_ge`, `itv_partition_nth_le`, 
+    `nondecreasing_fun_itv_partition`, `nonincreasing_fun_itv_partition`, 
+    `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, 
+    `notin_itv_partition`, `itv_partition_rev`, `variationE`, `variation_nil`, 
+    `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, 
+    `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, 
+    `le_variation`, `variation_opp_rev`, `variation_rev_opp`, 
+    `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`, 
+    `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`, 
+    `bounded_variationl`, `bounded_variationr`, `variations_opp`, 
+    `nondecreasing_bounded_variation`, `total_variationxx`, 
+    `total_variation_ge`, `total_variation_ge0`, 
+    `nondecreasing_total_variation`, `bounded_variationP`, `total_variationN`, 
+    `total_variation_le`, `total_variationD`, `neg_TV_increasing`, 
+    `total_variation_jordan_decompE`, `neg_TV_increasing_fin`, 
+    `neg_TV_bounded_variation`, `TV_right_continuous`, 
+    `neg_TV_right_continuous`, `total_variation_opp`, `TV_left_continuous`, and 
+    `TV_continuous`.
+
 ### Changed
   
 ### Renamed
diff --git a/theories/realfun.v b/theories/realfun.v
index dea77b14ba..bd21d1181f 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -21,6 +21,16 @@ From HB Require Import structures.
 (*                                                                            *)
 (*   derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and       *)
 (*                                        continuous up to the boundary       *)
+(*       itv_partition a b s == s is a partition of the interval `[a,b]       *)
+(*        itv_partitionL s c == the left side of splitting a partition at c   *)
+(*        itv_partitionR s c == the right side of splitting a partition at c  *)
+(*        variation a b f s  == the sum of f at all points in the partition s *)
+(*         variations a b f  == the set of all variation of f between a and b *)
+(*  bounded_variation a b f  == all variations of f are bounded               *)
+(*    total_variation a b f  == the sup over all variations of f from a to b  *)
+(*             neg_tv a f x  == the decreasing component of f                 *)
+(*             pos_tv a f x  == the increasing component of f                 *)
+(*                                                                            *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* * Limit superior and inferior for functions:                               *)