fixing names

CHANGELOG_UNRELEASED.md

@@ -51,7 +51,7 @@
   + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`,
     `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`,
 	  `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`,
-    `total_variation_jordan_decompE`, `fine_neg_tv_nondecreasing`,
+    `total_variation_pos_neg_tvE`, `fine_neg_tv_nondecreasing`,
     `neg_tv_bounded_variation`, `total_variation_right_continuous`,
     `neg_tv_right_continuous`, `total_variation_opp`,
     `total_variation_left_continuous`, `total_variation_continuous`,

theories/realfun.v

@@ -1879,11 +1879,10 @@ have [y [s' s'E]] : exists y s', s = y :: s'.
   by case: {itvas itvws IH} s sub => // y s' ?; exists y, s'.
 apply: le_trans; first apply IH => //.
   case: itvws => /= /andP [_]; rewrite s'E /= => /andP [ay ys' lyb].
-  by split => //; apply/andP; split => //; apply: (lt_trans wa).
-rewrite variationD => //; last exact: itv_partition1.
-apply: le_variation.
+  by split => //; apply/ (path_lt_head wa)/andP; split => //.
+by rewrite variationD => //; [exact: le_variation | exact: itv_partition1].
 Qed.
-  
+
 End variation.
 
 Section bounded_variation.
@@ -2160,8 +2159,8 @@ apply: lee_add => //; apply: le_trans; last exact: total_variation_ge.
 by rewrite lee_fin ler_norm.
 Qed.
 
-Lemma total_variation_jordan_decompE a b f : BV a b f ->
-  {in `[a, b], f =1 (fine \o neg_tv a (\- f)) \- (fine \o neg_tv a f)}.
+Lemma bounded_variation_pos_neg_tvE a b f : BV a b f ->
+  {in `[a, b], f =1 (fine \o pos_tv a f) \- (fine \o neg_tv a f)}.
 Proof.
 move=> bdabf x; rewrite in_itv /= => /andP [ax xb].
 have ffin: TV a x f \is a fin_num.
@@ -2170,13 +2169,13 @@ have ffin: TV a x f \is a fin_num.
 have Nffin : TV a x (\- f) \is a fin_num.
   apply/bounded_variationP => //; apply/bounded_variationN.
   exact: (bounded_variationl ax xb).
-rewrite /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //; first last.
+rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //.
+- rewrite addeAC oppeD //= ?fin_num_adde_defl //.
+  by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr.
+- by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split.
+- by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split.
 - by rewrite fin_numM // fin_numD; apply/andP; split.
 - by rewrite fin_numM // fin_numD; apply/andP; split.
-- by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split.
-- by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split.
-rewrite addeAC oppeD //= ?fin_num_adde_defl //.
-by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr.
 Qed.
 
 Lemma fine_neg_tv_nondecreasing a b f : BV a b f ->