proposition: Lemma total_variation_le a b f g : a <= b -> (TV a b (f \+ g)%R <= TV a b f + TV a b g)%E.
proof: Proof. rewrite le_eqVlt => /predU1P[<-{b}|ab]. by rewrite !total_variationxx adde0. have [abf|abf] := pselect (BV a b f); last first. rewrite {2}/total_variation hasNub_ereal_sup//; last first. exact: variations_neq0. rewrite addye ?leey// -ltNye (@lt_le_trans _ _ 0%E)//. exact/total_variation_ge0/ltW. have [abg|abg] := pselect (BV a b g); last first. rewrite {3}/total_variation hasNub_ereal_sup//; last first. exact: variations_neq0. rewrite addey ?leey// -ltNye (@lt_le_trans _ _ 0%E)//. exact/total_variation_ge0/ltW. move: abf abg => [r abfr] [s abgs]. have BVabfg : BV a b (f \+ g). by apply: bounded_variationD => //; [exists r|exists s]. apply: ub_ereal_sup => y /= [r' [s' abs <-{r'} <-{y}]]. apply: (@le_trans _ _ (variation a b f s' + variation a b g s')%:E). exact: variation_le. by rewrite EFinD leeD// ereal_sup_le//; (eexists; last exact: lexx); (eexists; last reflexivity); exact: variations_variation. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)