proposition: Lemma iavgD f g A : measurable A -> mu A < +oo -> measurable_fun A f -> measurable_fun A g -> iavg (f \+ g)%R A <= iavg f A + iavg g A.
proof: Proof. move=> mA Aoo mf mg; have [r0|r0] := eqVneq (mu A) 0. by rewrite /iavg r0/= invr0 !mul0e adde0. rewrite -muleDr//=; last by rewrite ge0_adde_def// inE integral_ge0. rewrite lee_pmul2l//; last first. by rewrite lte_fin invr_gt0// fine_gt0// Aoo andbC/= lt0e r0/=. rewrite -ge0_integralD//=; [|by do 2 apply: measurableT_comp..]. apply: ge0_le_integral => //=. - by do 2 apply: measurableT_comp => //; exact: measurable_funD. - by move=> /= x _; rewrite adde_ge0. - by apply: measurableT_comp => //; apply: measurable_funD => //; exact: measurableT_comp. - by move=> /= x _; exact: ler_normD. 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