proposition: Lemma hlength_sigma_sub_additive : sigma_sub_additive (hlength : set (ocitv_type R) -> _).
proof: Proof. move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE. move=> [a _ <-]; rewrite hlength_itv ?lte_fin/= -EFinB => lebig. case: ifPn => a12; last by rewrite nneseries_esum// esum_ge0. apply/lee_addgt0Pr => _ /posnumP[e]. rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//. apply: le_trans (epsilon_trick _ _ _) => //=. have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1)%:R. by rewrite divr_gt0// ltr0n// expn_gt0. have eVn_ge0 n := ltW (eVn_gt0 n). pose Aoo i : set (ocitv_type R) := `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R[%classic. pose Aoc i : set (ocitv_type R) := `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R]%classic. have: `[a.1 + e%:num / 2, a.2] `<=` \bigcup_i Aoo i. apply: (@subset_trans _ `]a.1, a.2]). move=> x; rewrite /= !in_itv /= => /andP[+ -> //]. by move=> /lt_le_trans-> //; rewrite ltrDl. apply: (subset_trans lebig); apply: subset_bigcup => i _; rewrite AE /Aoo/=. move=> x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=. by rewrite ltrDl. have := @segment_compact _ (a.1 + e%:num / 2) a.2; rewrite compact_cover. move=> /[apply]-[i _|X _ Xc]; first exact: interval_open. have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i. move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix. by exists i => //; apply: subset_itv_oo_oc Aooix. have /[apply] := @content_sub_fsum _ _ _ [the content _ _ of hlength : set (ocitv_type R) -> _] _ [set` X]. move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans. rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD. by case: ltP => //; rewrite lee_fin subr_le0. rewrite nneseries_esum//; last by move=> *; rewrite adde_ge0//= ?lee_fin. rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite// ?set_fsetK//=. rewrite fsbig_finite//= set_fsetK//. rewrite lee_sum // => i _; rewrite ?AE// !hlength_itv/= ?lte_fin -?EFinD/=. do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW. by rewrite addrAC. by rewrite addrAC lee_fin lerD// subr_le0 leNgt. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure