proposition: Lemma neg_tv_right_continuous a x b f : a <= x -> x < b -> BV a b f -> f @ x^'+ --> f x -> fine \o neg_tv a f @ x^'+ --> fine (neg_tv a f x).
proof: Proof. move=> ax ? bvf fcts; have xb : x <= b by exact: ltW. have xbfin : TV a x f \is a fin_num. by apply/bounded_variationP => //; exact: bounded_variationl bvf. apply: fine_cvg; rewrite /neg_tv fineM // ?fin_numB ?xbfin //= EFinM. under eq_fun => i do rewrite EFinN. apply: (@cvg_trans _ (((TV a n f - (f n)%:E) * 2^-1%:E)%E @[n --> x^'+])). exact: cvg_id. apply: cvgeMr; first by []. rewrite fineD; [|by []..]. rewrite EFinB; apply: cvgeB; [by []| |]. apply/ fine_cvgP; split; first exists (b - x). - by rewrite /= subr_gt0. - move=> t /= xtbx xt; have ? : a <= t. by apply: ltW; apply: (le_lt_trans ax). apply/bounded_variationP => //. apply: bounded_variationl bvf => //. move: xtbx; rewrite distrC ger0_norm ?subr_ge0; last by exact: ltW. by rewrite ltrBrDr -addrA [-_ + _]addrC subrr addr0 => /ltW. by apply: total_variation_right_continuous => //; last exact: bvf. apply: cvg_comp; first exact: fcts. apply/ fine_cvgP; split; first by near=> t => //. by have -> : fine \o EFin = id by move=> ?; rewrite funeqE => ? /=. 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)