proposition: Lemma wlength_sigma_sub_additive (f : cumulative R) : sigma_sub_additive (wlength f).
proof: Proof. move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE. move=> [a _ <-]; rewrite wlength_itv ?lte_fin/= -EFinB => lebig. case: ifPn => a12; last by rewrite nneseries_esum ?esum_ge0. wlog wlogh : b A AE lebig / forall n, (b n).1 <= (b n).2. move=> /= h. set A' := fun n => if (b n).1 >= (b n).2 then set0 else A n. set b' := fun n => if (b n).1 >= (b n).2 then (0, 0) else b n. rewrite [X in (_ <= X)%E](_ : _ = \sum_(n <oo) wlength f (A' n))%E; last first. apply: (@eq_eseriesr _ (wlength f \o A) (wlength f \o A')) => k. rewrite /= /A' AE; case: ifPn => // bn. by rewrite set_itv_ge//= bnd_simp -leNgt. apply: (h b'). - move=> k; rewrite /A'; case: ifPn => // bk. by rewrite set_itv_ge//= bnd_simp -leNgt /b' bk. - by rewrite AE /b' (negbTE bk). - apply: (subset_trans lebig); apply subset_bigcup => k _. rewrite /A' AE; case: ifPn => bk //. by rewrite subset0 set_itv_ge//= bnd_simp -leNgt. - by move=> k; rewrite /b'; case: ifPn => //; rewrite -ltNge => /ltW. apply/lee_addgt0Pr => _/posnumP[e]. rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//. apply: le_trans (epsilon_trick _ _ _) => //=. have [c ce] := nondecreasing_right_continuousP a.1 f [gt0 of e%:num / 2]. have [D De] : exists D : nat -> {posnum R}, forall i, f ((b i).2 + (D i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1. suff : forall i, exists di : {posnum R}, f ((b i).2 + di%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1. by move/choice => -[g hg]; exists g. move=> k; apply nondecreasing_right_continuousP => //. by rewrite divr_gt0 // exprn_gt0. have acbd : `[ a.1 + c%:num / 2, a.2] `<=` \bigcup_i `](b i).1, (b i).2 + (D i)%:num[%classic. apply: (@subset_trans _ `]a.1, a.2]). move=> r; rewrite /= !in_itv/= => /andP [+ ->]. by rewrite andbT; apply: lt_le_trans; rewrite ltrDl. apply: (subset_trans lebig) => r [n _ Anr]; exists n => //. move: Anr; rewrite AE /= !in_itv/= => /andP [->]/= /le_lt_trans. by apply; rewrite ltrDl. have := @segment_compact _ (a.1 + c%:num / 2) a.2; rewrite compact_cover. have obd k : [set: nat] k -> open `](b k).1, ((b k).2 + (D k)%:num)[%classic. by move=> _; exact: interval_open. move=> /(_ _ _ _ obd acbd){obd acbd}. case=> X _ acXbd. rewrite /cover in acXbd. rewrite -EFinD. apply: (@le_trans _ _ (\sum_(i <- X) (wlength f `](b i).1, (b i).2]%classic) + \sum_(i <- X) (f ((b i).2 + (D i)%:num)%R - f (b i).2)%:E)%E). apply: (@le_trans _ _ (f a.2 - f (a.1 + c%:num / 2))%:E). rewrite lee_fin -addrA -opprD lerB// (le_trans _ ce)//. rewrite cumulative_is_nondecreasing//. by rewrite lerD2l ler_pdivrMr// ler_pMr// ler1n. apply: (@le_trans _ _ (\sum_(i <- X) (f ((b i).2 + (D i)%:num) - f (b i).1)%:E)%E). rewrite sumEFin lee_fin cumulative_content_sub_fsum//. by move=> k kX; rewrite (@le_trans _ _ (b k).2)// lerDl. apply: subset_trans. exact/(subset_trans _ acXbd)/subset_itv_oc_cc. move=> x [k kX] kx; rewrite -bigcup_fset; exists k => //. by move: x kx; exact: subset_itv_oo_oc. rewrite addeC -big_split/=; apply: lee_sum => k _. by rewrite !(EFinB, wlength_itv_bnd)// addeA subeK. rewrite -big_split/= nneseries_esum//; last by move=> k _; rewrite adde_ge0. rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite//= set_fsetK. rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX. by rewrite AE lee_add2l// lee_fin lerBlDl natrX De. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) HB(structures) mathcomp.classical(mathcomp_extra boolp classical_sets) mathcomp.classical(functions fsbigop cardinality) reals ereal signed topology numfun normedtype sequences esum real_interval measure realfun