proposition: Lemma P_semi_sigma_additive : semi_sigma_additive P.
proof: Proof. move=> F mFi disjF mUF. move=> X /=. rewrite /nbhs /=. rewrite -[Y in ereal_nbhs Y]fineK ?P_fin //=. case => x /= xpos. rewrite /ball_ => xball. rewrite /nbhs /= /nbhs /=. rewrite /eventually /=. rewrite /filter_from /=. suff: exists N, forall k, (N <= k)%nat -> P (\bigcup_n F n) = P (\bigcup_(i < k) F i). case=> N HN. exists N => //. move=> j /= ij. rewrite -[y in X y]fineK; last by apply/sum_fin_numP => *; exact: P_fin. apply: xball => /=. rewrite [X in X < x](_ : _ = 0) //. apply/eqP. rewrite normr_eq0 subr_eq0. apply/eqP; congr fine. rewrite (HN j) // /P. rewrite esum_bigcupT //; last exact: d0. rewrite esum_fset //; last by move=> *; apply esum_ge0 => *; exact: d0. rewrite big_mkord. by rewrite -fsbigop.fsbig_ord. rewrite P_fssum. set f := fun t => if fibration_of_partition [set: nat] F t is Some i then i else 0%N. exists (\max_(t <- finsupp d | `[< (\bigcup_i F i)%classic t >]) f t).+1. move=> k Nk. rewrite P_fssum. suff : (\bigcup_n F n `&` [set` finsupp d] = \bigcup_(i < k) F i `&` [set` finsupp d])%classic by move ->. rewrite (bigcupID `I_k) setIUl 2!setTI -[RHS]setU0. congr setU. rewrite setI_bigcupl bigcup0 // => i. rewrite /mkset /=. apply: contra_notP. case/eqP/set0P => t [] Fit tfd. apply:(leq_ltn_trans _ Nk). suff-> : i = f t. apply bigop.leq_bigmax_seq => //. by apply/asboolP; exists i . rewrite /f /=. by rewrite (fibration_of_partitionE disjF _ Fit). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(finmap) Reals mathcomp(mathcomp_extra) mathcomp(classical_sets boolp cardinality Rstruct reals) mathcomp(ereal topology esum measure probability) ssrR realType_ext Reals_ext ssr_ext ssralg_ext bigop_ext fdist convex mathcomp(measure probability)