proposition: Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T -> \bar R) : measurable_fun D f -> \int[mu]_(x in D) `|f x| = 0 <-> ae_eq D f (cst 0).
proof: Proof. move=> mf; split=> [iDf0|Df0]. exists (D `&` [set x | f x != 0]); split; [exact: emeasurable_neq| |by move=> t /= /not_implyP [Dt /eqP ft0]]. have muDf a : (0 < a)%R -> mu (D `&` [set x | a%:E <= `|f x|]) = 0. move=> a0; apply/eqP; rewrite -measure_le0. by have := le_integral_abse mu mD mf a0; rewrite iDf0 pmule_rle0 ?lte_fin. rewrite [X in mu X](_ : _ = \bigcup_n (D `&` [set x | `|f x| >= n.+1%:R^-1%:E])); last first. rewrite predeqE => t; split=> [[Dt ft0]|[n _ /= [Dt nft]]]. have [ftoo|ftoo] := eqVneq `|f t| +oo. by exists 0%N => //; split => //=; rewrite ftoo /= leey. pose m := `|ceil (fine `|f t|)^-1|%N. have ftfin : `|f t|%E \is a fin_num by rewrite ge0_fin_numE// ltey. exists m => //; split => //=. rewrite -(@fineK _ `|f t|) // lee_fin -ler_pV2; last 2 first. - rewrite inE unitfE fine_eq0// abse_eq0 ft0/= fine_gt0//. by rewrite lt0e abse_ge0 abse_eq0 ft0 ltey. - by rewrite inE unitfE invr_eq0 pnatr_eq0 /= invr_gt0. rewrite invrK /m -natr1 natr_absz ger0_norm ?ceil_ge0//. rewrite (@le_trans _ _ ((fine `|f t|)^-1 + 1)%R) ?lerDl//. by rewrite lerD2r// ceil_ge. by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge. transitivity (limn (fun n => mu (D `&` [set x | `|f x| >= n.+1%:R^-1%:E]))). apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. - move=> i; apply: emeasurable_fun_c_infty => //. exact: measurableT_comp. - apply: bigcupT_measurable => i. by apply: emeasurable_fun_c_infty => //; exact: measurableT_comp. - move=> m n mn; apply/subsetPset; apply: setIS => t /=. by apply: le_trans; rewrite lee_fin lef_pV2 // ?ler_nat // posrE. by rewrite (_ : (fun _ => _) = cst 0) ?lim_cst//= funeqE => n /=; rewrite muDf. pose f_ := fun n x => mine `|f x| n%:R%:E. have -> : (fun x => `|f x|) = (fun x => limn (f_^~ x)). rewrite funeqE => x; apply/esym/cvg_lim => //; apply/cvg_ballP => _/posnumP[e]. near=> n; rewrite /ball /= /ereal_ball /= /f_. have [->|fxoo] := eqVneq `|f x|%E +oo. rewrite -[contract +oo](@divrr _ (1 + n%:R)%R) ?unitfE ?nat1r//=. rewrite (@ger0_norm _ n%:R)// nat1r -mulrBl -natrB// subSnn ger0_norm//. by rewrite div1r; near: n; exact: near_infty_natSinv_lt. have fxn : `|f x| <= n%:R%:E. rewrite -(@fineK _ `|f x|); last by rewrite ge0_fin_numE// ltey. rewrite lee_fin; near: n; exists (Num.bound (fine `|f x|)) => //= n/=. by rewrite -(ler_nat R); apply: le_trans; exact/ltW/archi_boundP. by rewrite min_l// subrr normr0. transitivity (limn (fun n => \int[mu]_(x in D) (f_ n x) )). apply/esym/cvg_lim => //; apply: cvg_monotone_convergence => //. - by move=> n; apply: measurable_mine => //; exact: measurableT_comp. - by move=> n t Dt; rewrite /f_ lexI abse_ge0 //= lee_fin. - move=> t Dt m n mn; rewrite /f_ lexI. have [ftm|ftm] := leP `|f t|%E m%:R%:E. by rewrite lexx /= (le_trans ftm)// lee_fin ler_nat. by rewrite (ltW ftm) /= lee_fin ler_nat. have ae_eq_f_ n : ae_eq D (f_ n) (cst 0). case: Df0 => N [mN muN0 DfN]. exists N; split => // t /= /not_implyP[Dt fnt0]. apply: DfN => /=; apply/not_implyP; split => //. apply: contra_not fnt0 => ft0. by rewrite /f_ ft0 /= normr0 min_l// lee_fin. have f_bounded n x : D x -> `|f_ n x| <= n%:R%:E. move=> Dx; rewrite /f_; have [|_] := leP `|f x| n%:R%:E. by rewrite abse_id. by rewrite gee0_abs// lee_fin. have if_0 n : \int[mu]_(x in D) `|f_ n x| = 0. apply: (@ae_eq_integral_abs_bounded _ _ _ n%:R) => //. by apply: measurable_mine => //; exact: measurableT_comp. exact: f_bounded. rewrite (_ : (fun _ => _) = cst 0) // ?lim_cst// funeqE => n. by rewrite -(if_0 n); apply: eq_integral => x _; rewrite gee0_abs// /f_. Unshelve. all: by end_near. 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