proposition: Lemma integralD_EFin : \int[mu]_(x in D) (g1 \+ g2) x = \int[mu]_(x in D) g1 x + \int[mu]_(x in D) g2 x.
proof: Proof. suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g2^\- x) = \int[mu]_(x in D) ((g1 \+ g2)^\- x) + \int[mu]_(x in D) (g1^\+ x) + \int[mu]_(x in D) (g2^\+ x). move=> h; rewrite [in LHS]integralE. move/eqP : h; rewrite -[in eqRHS]addeA [in eqRHS]addeC. have g12pos : \int[mu]_(x in D) (g1^\+ x) + \int[mu]_(x in D) (g2^\+ x) \is a fin_num. rewrite ge0_fin_numE//. by rewrite lte_add_pinfty//; exact: integral_funepos_lt_pinfty. by rewrite adde_ge0// integral_ge0. have g12neg : \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g2^\- x) \is a fin_num. rewrite ge0_fin_numE//. by rewrite lte_add_pinfty// ; exact: integral_funeneg_lt_pinfty. by rewrite adde_ge0// integral_ge0. rewrite -sube_eq; last 2 first. - rewrite ge0_fin_numE. apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty. exact: integral_funepos_lt_pinfty (integrableD _ _ _). rewrite adde_ge0//; last exact: integral_ge0. by rewrite adde_ge0// integral_ge0. - by rewrite fin_num_adde_defr. rewrite -(addeA (\int[mu]_(x in D) (g1 \+ g2)^\+ x)). rewrite (addeC (\int[mu]_(x in D) (g1 \+ g2)^\+ x)) -[eqbLHS]addeA. rewrite (addeC (\int[mu]_(x in D) g1^\- x + \int[mu]_(x in D) g2^\- x)). rewrite eq_sym -(sube_eq g12pos) ?fin_num_adde_defl// => /eqP <-. rewrite fin_num_oppeD; last first. rewrite ge0_fin_numE; first exact: integral_funeneg_lt_pinfty if2. exact: integral_ge0. by rewrite addeACA (integralE _ _ g1) (integralE _ _ g2). have : (g1 \+ g2)^\+ \+ g1^\- \+ g2^\- = (g1 \+ g2)^\- \+ g1^\+ \+ g2^\+. rewrite funeqE => x. apply/eqP; rewrite -2!addeA [in eqRHS]addeC -sube_eq; last 2 first. by rewrite /funepos /funeneg -!fine_max. by rewrite /funepos /funeneg -!fine_max. rewrite addeAC eq_sym -sube_eq; last 2 first. by rewrite /funepos /funeneg -!fine_max. by rewrite /funepos /funeneg -!fine_max. apply/eqP. rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) -funeD_posD. by rewrite -[RHS]/((_ \- _) x) -funeD_Dpos. move/(congr1 (fun y => \int[mu]_(x in D) (y x) )). rewrite (ge0_integralD mu mD); last 4 first. - by move=> x _; rewrite adde_ge0. - apply: emeasurable_funD; last exact: measurable_funeneg. exact/measurable_funepos/emeasurable_funD. - by []. - exact: measurable_funeneg. rewrite (ge0_integralD mu mD); last 4 first. - by []. - exact/measurable_funepos/emeasurable_funD. - by []. - exact/measurable_funepos/measurableT_comp. move=> ->. rewrite (ge0_integralD mu mD); last 4 first. - by move=> x _; exact: adde_ge0. - apply: emeasurable_funD; last exact: measurable_funepos. exact/measurable_funeneg/emeasurable_funD. - by []. - exact: measurable_funepos. rewrite (ge0_integralD mu mD) //; last exact: measurable_funepos. exact/measurable_funeneg/emeasurable_funD. 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