proposition: Lemma total_variation_left_continuous a b x f : a < x -> x <= b -> f @ x^'- --> f x -> BV a b f -> fine \o TV a ^~ f @ x^'- --> fine (TV a x f).
proof: Proof. move=> ax xb fNcts bvf. apply/cvg_at_leftNP; rewrite total_variation_opp. have bvNf : BV (-b) (-a) (f \o -%R). by case: bvf => M; rewrite -variations_opp => ?; exists M. have bx : - b <= - x by rewrite lerNl opprK. have xa : - x < - a by rewrite ltrNl opprK. have ? : - x <= - a by exact: ltW. have ? : Filter (nbhs (-x)^'+) by exact: at_right_proper_filter. have -> : fine (TV (-x) (-a) (f \o -%R)) = fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) (-x) (f \o -%R)). apply/eqP; rewrite -subr_eq opprK addrC. rewrite -fineD; last 2 first. by apply/bounded_variationP => //; exact: bounded_variationl bvNf. by apply/bounded_variationP => //; exact: bounded_variationr bvNf. by rewrite -total_variationD. have /near_eq_cvg/cvg_trans : {near (- x)^'+, (fun t => fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) t (f \o -%R))) =1 (fine \o (TV a)^~ f) \o -%R}. apply: filter_app (nbhs_right_lt xa). apply: filter_app (nbhs_right_ge _). near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx). have ? : t <= -a by exact: ltW. apply/eqP; rewrite eq_sym -subr_eq opprK addrC. rewrite /= [TV a _ f]total_variation_opp opprK -fineD; last first. by apply/bounded_variationP => //; apply: bounded_variationr bvNf. by apply/bounded_variationP => //; apply: bounded_variationl bvNf. by rewrite -total_variationD. apply. apply: cvgB; first exact: cvg_cst. apply: (total_variation_right_continuous _ _ _ bvNf). - by rewrite lerNl opprK //. - by rewrite ltrNl opprK //. by apply/cvg_at_leftNP; rewrite /= opprK. Unshelve. all: by end_near. 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)