proposition: Lemma sintegralD : sintegral m (f \+ g)%R = sintegral m f + sintegral m g.
proof: Proof. rewrite !sintegralE; set F := f @` _; set G := g @` _; set FG := _ @` _. pose pf x := f @^-1` [set x]; pose pg y := g @^-1` [set y]. transitivity (\sum_(z \in FG) z%:E * \sum_(a \in F) m (pf a `&` pg (z - a)%R)). apply: eq_fsbigr => z _; rewrite preimage_add -fsbig_setU// measure_fsbig//. by move=> x Fx; exact: measurableI. exact/trivIset_setIr/trivIset_preimage1. under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//. transitivity (\sum_(x \in F) \sum_(y \in G) (x + y)%:E * m (pf x `&` pg y)). apply: eq_fsbigr => x _; rewrite /pf /pg (fsbig_widen G setT)//=; last first. by move=> y [_ /= /preimage10->]; rewrite setI0 measure0 mule0. rewrite (fsbig_widen FG setT)//=; last first. move=> z [_ /= FGz]; rewrite [X in m X](_ : _ = set0) ?measure0 ?mule0//. rewrite -subset0 => //= {x}i /= [<-] /(canLR (@addrNK _ _)). by apply: contra_not FGz => <-; exists i; rewrite //= addrC. rewrite (reindex_fsbigT (+%R x))//=. by apply: eq_fsbigr => y; rewrite addrC addrK. transitivity (\sum_(x \in F) \sum_(y \in G) x%:E * m (pf x `&` pg y) + \sum_(x \in F) \sum_(y \in G) y%:E * m (pf x `&` pg y)). do 2![rewrite -fsbig_split//; apply: eq_fsbigr => _ /set_mem [? _ <-]]. by rewrite EFinD ge0_muleDl// ?lee_fin. congr (_ + _)%E; last rewrite exchange_fsbig//; apply: eq_fsbigr => x _. by rewrite -ge0_mule_fsumr// additive_nnsfunr nnsfun_cover setIT. by rewrite -ge0_mule_fsumr// additive_nnsfunl nnsfun_cover setTI. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun