proposition: Lemma total_variation_right_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 ctsf bvf; have ? : a <= b by apply:ltW; apply: (le_lt_trans ax). apply/cvgrPdist_lt=> _/posnumP[eps]. have ? : Filter (nbhs x^'+) by exact: at_right_proper_filter. have xbl := ltW xb. have xbfin : TV x b f \is a fin_num. by apply/bounded_variationP => //; exact: (bounded_variationr _ _ bvf). have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num / 2) _ xbfin. case=> ? [l + <- <-]; rewrite -/(total_variation x b f). move: l => [|i j]. by move=> /itv_partition_nil /eqP; rewrite lt_eqF. move=> [/= /andP[xi ij /eqP ijb]] tv_eps. apply: filter_app (nbhs_right_ge _). apply: filter_app (nbhs_right_lt xi). have e20 : 0 < eps%:num / 2 by []. move/cvgrPdist_lt/(_ (eps%:num/2) e20) : ctsf; apply: filter_app. near=> t => fxt ti xt; have ta : a <= t by exact: (le_trans ax). have tb : t <= b by rewrite (le_trans (ltW ti))// -ijb path_lt_le_last. rewrite -fineB; last 2 first. by apply/bounded_variationP => //; exact: bounded_variationl bvf. by apply/bounded_variationP => //; exact: bounded_variationl bvf. rewrite (total_variationD _ ax xt). have tbfin : TV t b f \is a fin_num. by apply/bounded_variationP => //; exact: (@bounded_variationr _ a). have xtfin : TV x t f \is a fin_num. apply/bounded_variationP => //; apply: (@bounded_variationl _ _ _ b) => //. exact: (@bounded_variationr _ a). rewrite oppeD ?fin_num_adde_defl// addeA subee //; first last. by apply/bounded_variationP => //; exact: (@bounded_variationl _ _ _ b). rewrite sub0e fineN normrN ger0_norm; last first. by rewrite fine_ge0// total_variation_ge0. move: (tv_eps); rewrite (total_variationD f _ tb) //. move: xt; rewrite le_eqVlt => /predU1P[->|xt]. by rewrite total_variationxx/=. have : variation x b f (i :: j) <= variation x t f (t :: nil) + variation t b f (i :: j). rewrite variationD//; last 2 first. exact: itv_partition1. by rewrite /itv_partition/= ti ij ijb. exact: le_variation. rewrite -lee_fin => /lt_le_trans /[apply]. rewrite {1}variation_prev; last exact: itv_partition1. rewrite /= -addeA -lte_subr_addr; last by rewrite fin_numD; apply/andP. rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. move/lt_trans; apply. rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lteD2lE //. rewrite -addeA. apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). rewrite [in leRHS]variation_prev; last exact: itv_partition1. rewrite gee_addl // sube_le0; apply: ereal_sup_ub => /=. exists (variation t b f (i :: j)) => //; apply: variations_variation. by rewrite /itv_partition/= ijb ij ti. by rewrite /variation/= big_nat_recr//= big_nil add0r distrC lte_fin. 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)