proposition: Lemma negligible_integrable (D N : set T) (f : T -> \bar R) : measurable N -> measurable D -> measurable_fun D f -> mu N = 0 -> mu.-integrable D f <-> mu.-integrable (D `\` N) f.
proof: Proof. move=> mN mD mf muN0. pose mCN := measurableC mN. pose oneCN : {nnsfun T >-> R} := [the {nnsfun T >-> R} of mindic R mCN]. pose oneN : {nnsfun T >-> R} := [the {nnsfun T >-> R} of mindic R mN]. have /integrableP intone : mu.-integrable D (fun x => f x * (oneN x)%:E). apply/integrableP; split. apply: emeasurable_funM=> //; apply/EFin_measurable_fun. exact: measurable_funTS. rewrite (eq_integral (fun x => `|f x| * (\1_N x)%:E)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_N t)%:E) // lee_fin. rewrite -integral_setI_indic// (@integral_abs_eq0 D)//. - exact: measurableI. - by apply: (subset_measure0 _ _ _ muN0) => //; exact: measurableI. have h1 : mu.-integrable D f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E). split=> [/integrableP intf | /integrableP intCf]. apply/integrableP; split. apply: emeasurable_funM=> //; apply/EFin_measurable_fun => //. exact: measurable_funTS. rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E) // lee_fin. rewrite -integral_setI_indic//; case: intf => _; apply: le_lt_trans. by apply: subset_integral => //; [exact:measurableI|exact:measurableT_comp]. apply/integrableP; split => //; rewrite (funID mN f) -/oneCN -/oneN. have ? : measurable_fun D (fun x : T => f x * (oneCN x)%:E). by apply: emeasurable_funM=> //; exact/EFin_measurable_fun/measurable_funTS. have ? : measurable_fun D (fun x : T => f x * (oneN x)%:E). apply: emeasurable_funM => //. exact/EFin_measurable_fun/measurable_funTS. apply: (@le_lt_trans _ _ (\int[mu]_(x in D) (`|f x * (oneCN x)%:E| + `|f x * (oneN x)%:E|))). apply: ge0_le_integral => //. - by apply: measurableT_comp => //; exact: emeasurable_funD. - by move=> ? ?; apply: adde_ge0. - by apply: emeasurable_funD; exact: measurableT_comp. - by move=> *; rewrite lee_abs_add. rewrite ge0_integralD//; [|exact: measurableT_comp|exact: measurableT_comp]. by apply: lte_add_pinfty; [case: intCf|case: intone]. have h2 : mu.-integrable (D `\` N) f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E). split=> [/integrableP intCf | /integrableP intCf]; apply/integrableP. split. apply: emeasurable_funM=> //; apply/EFin_measurable_fun => //. exact: measurable_funTS. rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E)// lee_fin. rewrite -integral_setI_indic //; case: intCf => _; apply: le_lt_trans. apply: subset_integral => //; [exact: measurableI|exact: measurableD|]. by apply: measurableT_comp => //; apply: measurable_funS mf => // ? []. split. move=> mDN A mA; rewrite setDE (setIC D) -setIA; apply: measurableI => //. exact: mf. rewrite integral_setI_indic//. case: intCf => _; rewrite (eq_integral (fun x => `|f x| * (\1_(~` N) x)%:E))//. by move=> t _; rewrite abseM (@gee0_abs _ (\1_(~` N) t)%:E)// lee_fin. by apply: (iff_trans h1); exact: iff_sym. 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