proposition: Lemma integrable_ae : {ae mu, forall x, D x -> f x \is a fin_num}.
proof: Proof. have [muD0|muD0] := eqVneq (mu D) 0. by exists D; split => // t /= /not_implyP[]. pose E := [set x | `|f x| = +oo /\ D x ]. have mE : measurable E. rewrite (_ : E = D `&` f @^-1` [set -oo; +oo]). by apply: (measurable_int fint) => //; exact: measurableU. rewrite /E predeqE => t; split=> [[/eqP]|[Dt [|]/= ->//]]. by rewrite eqe_absl leey andbT /preimage/= => /orP[|]/eqP; tauto. have [ET|ET] := eqVneq E setT. have foo t : `|f t| = +oo by have [] : E t by rewrite ET. suff: \int[mu]_(x in D) `|f x| = +oo. by case: (integrableP _ _ _ fint) => _; rewrite ltey => /eqP. by rewrite -(integral_csty mD muD0)//; exact: eq_integral. suff: mu E = 0. move=> muE0; exists E; split => // t /= /not_implyP[Dt]. by rewrite fin_num_abs => /negP; rewrite -leNgt leye_eq => /eqP. have [->|/set0P E0] := eqVneq E set0; first by rewrite measure0. have [M M0 muM] : exists2 M, (0 <= M)%R & forall n, n%:R%:E * mu (E `&` D) <= M%:E. exists (fine (\int[mu]_(x in D) `|f x|)); first exact/fine_ge0/integral_ge0. move=> n; rewrite -integral_indic// -ge0_integralZl//; last 2 first. - exact: measurableT_comp. - by move=> *; rewrite lee_fin. rewrite fineK//; last first. case: (integrableP _ _ _ fint) => _ foo. by rewrite ge0_fin_numE// integral_ge0. apply: ge0_le_integral => //. - by move=> *; rewrite lee_fin /indic. - exact/EFin_measurable_fun/measurableT_comp. - by apply: measurableT_comp => //; apply: measurable_int fint. - move=> x Dx; rewrite /= indicE. have [|xE] := boolP (x \in E); last by rewrite mule0. by rewrite /E inE /= => -[->]; rewrite leey. apply/eqP/negPn/negP => /eqP muED0; move/not_forallP : muM; apply. have [muEDoo|] := ltP (mu (E `&` D)) +oo; last first. by rewrite leye_eq => /eqP ->; exists 1%N; rewrite mul1e leye_eq. exists `|ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1. apply/negP; rewrite -ltNge. rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first. by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)). rewrite lte_fin -ltr_pdivrMr. rewrite -natr1 natr_absz ger0_norm. by rewrite (le_lt_trans (ceil_ge _))// ltrDl. by rewrite ceil_ge0// divr_ge0//; apply/le0R/measure_ge0; exact: measurableI. rewrite -lte_fin fineK. rewrite lt0e measure_ge0 andbT. suff: E `&` D = E by move=> ->; exact/eqP. by rewrite predeqE => t; split=> -[]. by rewrite ge0_fin_numE// measure_ge0//; exact: measurableI. 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