From cca14fcda6196b8c37408c5146df4bbe55c66dfb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 2 May 2023 17:58:31 +0900 Subject: [PATCH] test with hints --- theories/kernel.v | 78 +++------ theories/lebesgue_integral.v | 326 +++++++++++++++-------------------- theories/lebesgue_measure.v | 30 ++-- theories/measure.v | 13 ++ 4 files changed, 190 insertions(+), 257 deletions(-) diff --git a/theories/kernel.v b/theories/kernel.v index 34b51f234f..d0ea66b3c7 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -120,8 +120,7 @@ Definition kseries : X -> {measure set Y -> \bar R} := fun x => [the measure _ _ of mseries (k ^~ x) 0]. Lemma measurable_fun_kseries (U : set Y) : - measurable U -> - measurable_fun setT (kseries ^~ U). + measurable U -> measurable_fun setT (kseries ^~ U). Proof. move=> mU. by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel. @@ -210,8 +209,7 @@ Definition kzero : X -> {measure set Y -> \bar R} := fun _ : X => [the measure _ _ of mzero]. Let measurable_fun_kzero U : measurable U -> - measurable_fun setT (kzero ^~ U). -Proof. by move=> ?/=; exact: measurable_fun_cst. Qed. + measurable_fun setT (kzero ^~ U). Proof. by []. Qed. HB.instance Definition _ := @isKernel.Build _ _ X Y R kzero measurable_fun_kzero. @@ -422,13 +420,12 @@ have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. have CXY : C `<=` XY. move=> _ [A mA [B mB <-]]; split; first exact: measurableM. rewrite phiM. - apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI. - by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA). + by apply: emeasurable_funM => //; [exact/measurable_kernel/measurableI|auto]. suff monoB : monotone_class setT XY by exact: monotone_class_subset. split => //; [exact: CXY| |exact: xsection_ndseq_closed]. move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD. suff : phi (A `\` B) = (fun x => phi A x - phi B x). - by move=> ->; exact: emeasurable_funB. + by move=> ->; auto. rewrite funeqE => x; rewrite /phi/= xsectionD// measureD. - by rewrite setIidr//; exact: le_xsection. - exact: measurable_xsection. @@ -454,9 +451,9 @@ Let phi A := fun x => k x (xsection A x). Let XY := [set A | measurable A /\ measurable_fun setT (phi A)]. Lemma measurable_fun_xsection_finite_kernel A : - A \in measurable -> measurable_fun setT (phi A). + measurable A -> measurable_fun setT (phi A). Proof. -move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[]. +move: A; suff : measurable `<=` XY by move=> + A => /[apply] -[]. move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ = (fun x => mrestr (k x) measurableT (xsection A x))); last first. by apply/funext => x//=; rewrite /mrestr setIT. @@ -487,15 +484,12 @@ rewrite (_ : (fun x => _) = transitivity (lim (fun n => \int[l x]_y (k_ n (x, y))%:E)); last first. rewrite is_cvg_lim_esupE//. apply: ereal_nondecreasing_is_cvg => m n mn. - apply: ge0_le_integral => //. + apply: ge0_le_integral => //; [|by auto| |by auto|]. - by move=> y _; rewrite lee_fin. - - exact/EFin_measurable_fun/measurable_fun_prod1. - by move=> y _; rewrite lee_fin. - - exact/EFin_measurable_fun/measurable_fun_prod1. - by move=> y _; rewrite lee_fin; exact/lefP/ndk_. - rewrite -monotone_convergence//. + rewrite -monotone_convergence//; [|by auto| |]. - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k. - - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod1. - by move=> n y _; rewrite lee_fin. - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_. apply: measurable_fun_lim_esup => n. @@ -505,22 +499,15 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE. rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n)) (\int[l x]_y (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))); last first. - apply/funext => x; rewrite -ge0_integral_fsum//. + apply/funext => x; rewrite -ge0_integral_fsum//; [|by auto|]. - by apply: eq_integral => y _; rewrite -fsumEFin. - - move=> r. - apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=. - rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//. - exact/measurable_funP. - by move=> m y _; rewrite nnfun_muleindic_ge0. apply: emeasurable_fun_fsum => // r. rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E * \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. apply/funext => x; under eq_integral do rewrite EFinM. have [r0|r0] := leP 0%R r. - rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin. - apply/EFin_measurable_fun/measurable_fun_prod1 => /=. - rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//. - exact/measurable_funP. + by rewrite ge0_integralM//; [auto|move=> y _; rewrite lee_fin]. rewrite integral0_eq; last first. by move=> y _; rewrite preimage_nnfun0// indic0 mule0. by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0. @@ -785,7 +772,6 @@ apply: measurable_fun_if => //. [set t | k t setT == +oo]); last first. by apply/seteqP; split=> x /= /orP//. by apply: measurableU; exact: kernel_measurable_eq_cst. -- exact: measurable_fun_cst. - apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel. apply/EFin_measurable_fun; rewrite setTI. apply: (@measurable_fun_comp _ _ _ _ _ _ [set r : R | r != 0%R]). @@ -793,8 +779,7 @@ apply: measurable_fun_if => //. + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey. + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. exact: inv_continuous. - + apply: measurable_funT_comp; last exact/measurable_funS/measurable_kernel. - exact: measurable_fun_fine. + + by apply: measurable_funT_comp => //; exact/measurable_funS/measurable_kernel. Qed. Section knormalize. @@ -815,15 +800,12 @@ rewrite (_ : (fun _ => _) = (fun x => else f x U * (fine (f x setT))^-1%:E)); last first. apply/funext => x; case: ifPn => [/orP[->//|->]|]; first by case: ifPn. by rewrite negb_or=> /andP[/negbTE -> /negbTE ->]. -apply: measurable_fun_if => //; - [exact: kernel_measurable_fun_eq_cst|exact: measurable_fun_cst|]. +apply: measurable_fun_if => //; first exact: kernel_measurable_fun_eq_cst. apply: measurable_fun_if => //. - rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]). exact: kernel_measurable_neq_cst. by apply/seteqP; split => [x /negbT//|x /negbTE]. -- apply: (@measurable_funS _ _ _ _ setT) => //. - exact: kernel_measurable_fun_eq_cst. -- exact: measurable_fun_cst. +- exact/measurable_funTS/kernel_measurable_fun_eq_cst. - apply: emeasurable_funM. by have := measurable_kernel f U mU; exact: measurable_funS. apply/EFin_measurable_fun. @@ -834,7 +816,7 @@ apply: measurable_fun_if => //. by rewrite ge0_fin_numE// lt_neqAle leey ftoo. + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. exact: inv_continuous. - + apply: measurable_funT_comp => /=; first exact: measurable_fun_fine. + + apply: measurable_funT_comp => //=. by have := measurable_kernel f _ measurableT; exact: measurable_funS. Qed. @@ -937,7 +919,6 @@ apply: (@le_lt_trans _ _ (\int[l x]__ r%:num%:E)). apply: ge0_le_integral => //. - have /measurable_fun_prod1 := measurable_kernel k _ measurableT. exact. - - exact/measurable_fun_cst. - by move=> y _; exact/ltW/hr. by rewrite integral_cst//= EFinM lte_pmul2l. Qed. @@ -1026,7 +1007,7 @@ Let k_2_ge0 n x : (0 <= k_2 n x)%R. Proof. by []. Qed. HB.instance Definition _ n := @isNonNegFun.Build _ _ _ (k_2_ge0 n). Let mk_2 n : measurable_fun setT (k_2 n). -Proof. by apply: measurable_funT_comp => //; exact: measurable_fun_snd. Qed. +Proof. exact: measurable_funT_comp. Qed. HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n). @@ -1086,19 +1067,13 @@ Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) : \int[(l \; k) x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E). Proof. under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//. -rewrite ge0_integral_fsum//; last 2 first. - - move=> r; apply/EFin_measurable_fun/measurable_funrM. - have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). +rewrite ge0_integral_fsum//; [|by auto|]; last first. - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under [in RHS]eq_integral. move=> y _. under eq_integral. by move=> z _; rewrite fimfunE -fsumEFin//; over. - rewrite /= ge0_integral_fsum//; last 2 first. - - move=> r; apply/EFin_measurable_fun/measurable_funrM. - have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). + rewrite /= ge0_integral_fsum//; [|by auto|]; last first. - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under eq_fsbigr. move=> r _. @@ -1138,8 +1113,7 @@ move=> f0 mf. have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z). transitivity (\int[(l \; k) x]_z (lim (EFin \o f_^~ z))). by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f. -rewrite monotone_convergence//; last 3 first. - by move=> n; exact/EFin_measurable_fun. +rewrite monotone_convergence//; [|by auto| |]; last 2 first. by move=> n z _; rewrite lee_fin. by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin. rewrite (_ : (fun _ => _) = @@ -1147,23 +1121,19 @@ rewrite (_ : (fun _ => _) = by apply/funext => n; rewrite integral_kcomp_nnsfun. transitivity (\int[l x]_y lim (fun n => \int[k (x, y)]_z (f_ n z)%:E)). rewrite -monotone_convergence//; last 3 first. - - move=> n; apply: measurable_fun_integral_kernel => //. + - move=> n; apply: measurable_fun_integral_kernel => //; last by auto. + move=> U mU; have := measurable_kernel k _ mU. by move=> /measurable_fun_prod1; exact. + by move=> z; rewrite lee_fin. - + exact/EFin_measurable_fun. - by move=> n y _; apply: integral_ge0 => // z _; rewrite lee_fin. - - move=> y _ a b ab; apply: ge0_le_integral => //. + - move=> y _ a b ab; apply: ge0_le_integral => //; [|by auto| |by auto|]. + by move=> z _; rewrite lee_fin. - + exact/EFin_measurable_fun. + by move=> z _; rewrite lee_fin. - + exact/EFin_measurable_fun. + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin. -apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first. - - by move=> n; exact/EFin_measurable_fun. - - by move=> n z _; rewrite lee_fin. - - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin. -by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f. +apply: eq_integral => y _; rewrite -monotone_convergence//; [|auto| |]. +- by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f. +- by move=> n z _; rewrite lee_fin. +- by move=> z _ a b /ndf_ /lefP; rewrite lee_fin. Qed. End integral_kcomp. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index e9b430901a..ab80811dd9 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -57,6 +57,31 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +#[global] Hint Extern 0 (measurable_fun _ (fun _ => _%:E)) => + (apply/EFin_measurable_fun) : core. +#[global] Hint Extern 0 (measurable_fun _ (fun x => (_) (_, x))) => + (apply: measurable_fun_prod1) : core. +#[global] Hint Extern 0 (measurable_fun _ (fun x => (_) (x, _))) => + (apply: measurable_fun_prod2) : core. +#[global] Hint Extern 0 (measurable_fun _ (fun _ => (_ * _)%R)) => + (apply: measurable_funrM) : core. +#[global] Hint Extern 0 (measurable_fun _ (\- _)%E) => + (apply: emeasurable_funN) : core. +#[global] Hint Extern 0 (measurable_fun _ (_ + _)%R) => + (apply: measurable_funD) : core. +#[global] Hint Extern 0 (measurable_fun _ (_ - _)%R) => + (apply: measurable_funB) : core. +#[global] Hint Extern 0 (measurable_fun _ (_ * _)%R) => + (apply: measurable_funM) : core. +#[global] Hint Extern 0 (measurable_fun _ (_ \max _)%R) => + (apply: measurable_fun_max) : core. +#[global] Hint Extern 0 (measurable_fun _ (fun x => maxe _ _)%E) => + (apply: emeasurable_fun_max) : core. +#[global] Hint Extern 0 (measurable_fun _ _^\+)%E => + (apply: emeasurable_fun_funepos) : core. +#[global] Hint Extern 0 (measurable_fun _ _^\-)%E => + (apply: emeasurable_fun_funeneg) : core. + Reserved Notation "\int [ mu ]_ ( i 'in' D ) F" (at level 36, F at level 36, mu at level 10, i, D at level 50, format "'[' \int [ mu ]_ ( i 'in' D ) '/ ' F ']'"). @@ -95,7 +120,7 @@ Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope. Lemma measurable_sfunP {d} {aT : measurableType d} {rT : realType} (f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y). -Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. +Proof. by rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. HB.structure Definition NonNegSimpleFun d (aT : measurableType d) (rT : realType) := @@ -146,7 +171,7 @@ Definition mfunchoiceMixin := [choiceMixin of {mfun aT >-> rT} by <:]. Canonical mfunchoiceType := ChoiceType {mfun aT >-> rT} mfunchoiceMixin. Lemma cst_mfun_subproof x : @isMeasurableFun d aT rT (cst x). -Proof. by split; apply: measurable_fun_cst. Qed. +Proof. by []. Qed. HB.instance Definition _ x := @cst_mfun_subproof x. Definition cst_mfun x := [the {mfun aT >-> rT} of cst x]. @@ -161,12 +186,7 @@ Section ring. Context d (aT : measurableType d) (rT : realType). Lemma mfun_subring_closed : subring_closed (@mfun _ aT rT). -Proof. -split=> [|f g|f g]; rewrite !inE/=. -- exact: measurable_fun_cst. -- exact: measurable_funB. -- exact: measurable_funM. -Qed. +Proof. by split=> [|f g|f g]; rewrite !inE//=; auto. Qed. Canonical mfun_add := AddrPred mfun_subring_closed. Canonical mfun_zmod := ZmodPred mfun_subring_closed. Canonical mfun_mul := MulrPred mfun_subring_closed. @@ -225,7 +245,7 @@ HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_mfun k). Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f]. Lemma max_mfun_subproof f g : @isMeasurableFun d aT rT (f \max g). -Proof. by split; apply: measurable_fun_max. Qed. +Proof. by split; auto. Qed. HB.instance Definition _ f g := max_mfun_subproof f g. Definition max_mfun f g := [the {mfun aT >-> _} of f \max g]. @@ -238,6 +258,8 @@ Lemma measurable_fun_indic d (T : measurableType d) (R : realType) Proof. by move=> mA; apply/measurable_funTS; rewrite (_ : \1__ = mindic R mA). Qed. +#[global] Hint Extern 0 (measurable_fun _ (\1_ _)) => + solve [exact: measurable_fun_indic] : core. Section sfun_pred. Context {d} {aT : measurableType d} {rT : realType}. @@ -1591,12 +1613,6 @@ Unshelve. all: by end_near. Qed. End semi_linearity. -Lemma emeasurable_funN d (T : measurableType d) (R : realType) D (f : T -> \bar R) : - measurable D -> measurable_fun D f -> measurable_fun D (fun x => - f x)%E. -Proof. -by move=> mD mf; apply: measurable_funT_comp => //; exact: emeasurable_fun_minus. -Qed. - Section approximation_sfun. Context d (T : measurableType d) (R : realType) (f : T -> \bar R). Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f). @@ -1605,12 +1621,9 @@ Lemma approximation_sfun : exists g : {sfun T >-> R}^nat, (forall x, D x -> EFin \o g^~x --> f x). Proof. have fp0 : (forall x, 0 <= f^\+ x)%E by []. -have mfp : measurable_fun D f^\+%E. - by apply: emeasurable_fun_max => //; exact: measurable_fun_cst. +have mfp : measurable_fun D f^\+%E by auto. have fn0 : (forall x, 0 <= f^\- x)%E by []. -have mfn : measurable_fun D f^\-%E. - by apply: emeasurable_fun_max => //; - [exact: emeasurable_funN | exact: measurable_fun_cst]. +have mfn : measurable_fun D f^\-%E by auto. have [fp_ [fp_nd fp_cvg]] := approximation mD mfp (fun x _ => fp0 x). have [fn_ [fn_nd fn_cvg]] := approximation mD mfn (fun x _ => fn0 x). exists (fun n => [the {sfun T >-> R} of fp_ n \+ cst (-1) \* fn_ n]) => x /=. @@ -1763,10 +1776,21 @@ Qed. Lemma measurable_funeM D (f : T -> \bar R) (k : \bar R) : measurable_fun D f -> measurable_fun D (fun x => k * f x)%E. -Proof. by move=> mf; exact/(emeasurable_funM _ mf)/measurable_fun_cst. Qed. +Proof. by move=> mf; exact/(emeasurable_funM _ mf). Qed. End emeasurable_fun. +#[global] Hint Extern 0 (measurable_fun _ (_ \- _)%E) => + (apply: emeasurable_funB) : core. +#[global] Hint Extern 0 (measurable_fun _ (_ \+ _)%E) => + (apply: emeasurable_funD) : core. +#[global] Hint Extern 0 (measurable_fun _ (_ \* _)%E) => + (apply: emeasurable_funM) : core. +#[global] Hint Extern 0 (measurable_fun _ (fun _ => _ * _)%E) => + (apply: emeasurable_funM) : core. +#[global] Hint Extern 0 (measurable_fun _ (fun _ => _ * _)%E) => + (apply: measurable_funeM) : core. + Section ge0_integral_sum. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -1999,7 +2023,7 @@ Lemma ge0_integralM (k : \bar R) : (forall x, D x -> 0 <= f x) -> Proof. move=> f0; move: k => [k|_|//]; first exact: ge0_integralM_EFin. pose g : (T -> \bar R)^nat := fun n x => n%:R%:E * f x. -have mg n : measurable_fun D (g n) by apply: measurable_funeM. +have mg n : measurable_fun D (g n) by exact: measurable_funeM. have g0 n x : D x -> 0 <= g n x. by move=> Dx; apply: mule_ge0; [rewrite lee_fin|exact:f0]. have nd_g x : D x -> nondecreasing_seq (g^~x). @@ -2081,9 +2105,7 @@ move=> fk0 mfk; have [k0|k0] := ltP k 0%R. rewrite integral0_eq//; last by move=> x _; rewrite fk0// indic0 mulr0. by rewrite integral0_eq ?mule0// => x _; rewrite fk0// indic0. under eq_integral do rewrite EFinM. -rewrite ge0_integralM//. -- exact/EFin_measurable_fun/measurable_fun_indic. -- by move=> y _; rewrite lee_fin. +by rewrite ge0_integralM//; [auto |move=> y _; rewrite lee_fin]. Qed. Lemma integralM_indic_nnsfun (f : {nnsfun T >-> R}) (k : R) : @@ -2112,9 +2134,7 @@ Let integral_mscale_nnsfun (h : {nnsfun T >-> R}) : \int[mscale k m]_(x in D) (h x)%:E = k%:num%:E * \int[m]_(x in D) (h x)%:E. Proof. under [LHS]eq_integral do rewrite fimfunE -fsumEFin//. -rewrite [LHS]ge0_integral_fsum//; last 2 first. - - move=> r. - exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. +rewrite [LHS]ge0_integral_fsum//; [|by auto|]; last first. - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0. rewrite -[RHS]ge0_integralM//; last 2 first. - exact/EFin_measurable_fun/measurable_funTS. @@ -2124,12 +2144,10 @@ under [RHS]eq_integral. by move=> r; rewrite EFinM nnfun_muleindic_ge0. over. rewrite [RHS]ge0_integral_fsum//; last 2 first. - - move=> r; apply/EFin_measurable_fun/measurable_funrM/measurable_funrM. - exact/measurable_fun_indic. + - by move=> r; apply/EFin_measurable_fun; auto. - by move=> n x _; rewrite EFinM mule_ge0// nnfun_muleindic_ge0. -apply: eq_fsbigr => r _; rewrite ge0_integralM//. +apply: eq_fsbigr => r _; rewrite ge0_integralM//; [|by auto|]. - by rewrite !integralM_indic_nnsfun//= integral_mscale_indic// muleCA. -- exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. - by move=> t _; rewrite nnfun_muleindic_ge0. Qed. @@ -2280,7 +2298,7 @@ rewrite monotone_convergence //. rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0. rewrite lee_fin; apply: le_trans MDm. by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm. -- by move=> n; exact: measurable_fun_cst. +- by rewrite /g. - by move=> n x Dx; rewrite lee_fin. - by move=> t Dt n m nm; rewrite /g lee_fin ler_nat. Qed. @@ -2305,14 +2323,13 @@ Proof. move=> mf f0. have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t). transitivity (lim (fun n => \int[pushforward mu mphi]_x (f_ n x)%:E)). - rewrite -monotone_convergence//. + rewrite -monotone_convergence//; [|by auto| |]. - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: f_f. - - by move=> n; exact/EFin_measurable_fun. - by move=> n y _; rewrite lee_fin. - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/ndf_. rewrite (_ : (fun _ => _) = (fun n => \int[mu]_x (EFin \o f_ n \o phi) x)). rewrite -monotone_convergence//; last 3 first. - - move=> n /=; apply: measurable_funT_comp; first exact: measurable_fun_EFin. + - move=> n /=; apply: measurable_funT_comp => //. by apply: measurable_funT_comp => //; exact: measurable_sfun. - by move=> n x _ /=; rewrite lee_fin. - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. @@ -2324,19 +2341,13 @@ have mfnphi r : measurable (f_ n @^-1` [set r] \o phi). transitivity (\sum_(k \in range (f_ n)) \int[mu]_x (k * \1_((f_ n @^-1` [set k]) \o phi) x)%:E). under eq_integral do rewrite fimfunE -fsumEFin//. - rewrite ge0_integral_fsum//; last 2 first. - - move=> y; apply/EFin_measurable_fun; apply: measurable_funM. - exact: measurable_fun_cst. - by rewrite (_ : \1_ _ = mindic R (measurable_sfunP (f_ n) (measurable_set1 y))). + rewrite ge0_integral_fsum//; [|by auto|]; last first. - by move=> y x _; rewrite nnfun_muleindic_ge0. apply: eq_fsbigr => r _; rewrite integralM_indic_nnsfun// integral_indic//=. rewrite (integralM_indic _ (fun r => f_ n @^-1` [set r] \o phi))//. by congr (_ * _); rewrite [RHS](@integral_indic). by move=> r0; rewrite preimage_nnfun0. -rewrite -ge0_integral_fsum//; last 2 first. - - move=> r; apply/EFin_measurable_fun; apply: measurable_funM. - exact: measurable_fun_cst. - by rewrite (_ : \1_ _ = mindic R (mfnphi r)). +rewrite -ge0_integral_fsum//; [|by auto|]; last first. - by move=> r x _; rewrite nnfun_muleindic_ge0. by apply: eq_integral => x _; rewrite fsumEFin// -fimfunE. Qed. @@ -2357,21 +2368,20 @@ transitivity (lim (fun n => \int[\d_ a]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//. - apply: eq_integral => x Dx; apply/esym/cvg_lim => //; apply: f_f. by rewrite inE in Dx. - - by move=> n; apply/EFin_measurable_fun; exact/measurable_funTS. + - by move=> n; exact/EFin_measurable_fun/measurable_funTS. - by move=> *; rewrite lee_fin. - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. rewrite (_ : (fun _ => _) = (fun n => (f_ n a)%:E)). by apply/cvg_lim => //; exact: f_f. apply/funext => n. under eq_integral do rewrite fimfunE// -fsumEFin//. -rewrite ge0_integral_fsum//. +rewrite ge0_integral_fsum//; [|by auto|]. - under eq_fsbigr do rewrite integralM_indic_nnsfun//. rewrite /= (fsbigD1 (f_ n a))//=; last by exists a. rewrite integral_indic//= diracE mem_set// mule1. rewrite fsbig1 ?adde0// => r /= [_ rfna]. rewrite integral_indic//= diracE memNset ?mule0//=. by apply/not_andP; left; exact/nesym. -- by move=> r; exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. - by move=> r x _; rewrite nnfun_muleindic_ge0. Qed. @@ -2379,8 +2389,8 @@ Lemma integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) : \int[\d_ a]_(x in D) f x = (\1_D a)%:E * f a. Proof. have [/[!inE] aD|aD] := boolP (a \in D). - rewrite integralE ge0_integral_dirac//; last exact/emeasurable_fun_funepos. - rewrite ge0_integral_dirac//; last exact/emeasurable_fun_funeneg. + rewrite integralE ge0_integral_dirac//; last by auto. + rewrite ge0_integral_dirac//; last by auto. by rewrite [in RHS](funeposneg f) indicE mem_set// mul1e. rewrite indicE (negbTE aD) mul0e -(integral_measure_zero D f)//. apply: eq_measure_integral => //= S mS DS; rewrite /dirac indicE memNset// => /DS. @@ -2408,8 +2418,7 @@ Let integralT_measure_sum (f : {nnsfun T >-> R}) : Proof. under eq_integral do rewrite fimfunE -fsumEFin//. rewrite ge0_integral_fsum//; last 2 first. - - move=> r /=; apply: measurable_funT_comp => //. - exact/measurable_funrM/measurable_fun_indic. + - by move=> r /=; apply: measurable_funT_comp => //; auto. - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0. transitivity (\sum_(i \in range f) (\sum_(n < N) i%:E * \int[m_ n]_x (\1_(f @^-1` [set i]) x)%:E)). @@ -2518,8 +2527,7 @@ Lemma integral_measure_series_nnsfun (D : set T) (mD : measurable D) Proof. under eq_integral do rewrite fimfunE -fsumEFin//. rewrite ge0_integral_fsum//; last 2 first. - - move=> r /=; apply: measurable_funT_comp => //. - exact/measurable_funrM/measurable_fun_indic. + - by move=> r /=; apply: measurable_funT_comp => //; auto. - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0. transitivity (\sum_(i \in range f) (\sum_(n /= _ [g /= gf] <-. rewrite -integralT_nnsfun (integral_measure_series_nnsfun _ mD). apply: lee_nneseries => n _. by apply: integral_ge0 => // x _; rewrite lee_fin. -rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //. +rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //; [|by auto| |]. - by move=> x _; rewrite lee_fin. -- exact/EFin_measurable_fun. - by move=> x _; rewrite erestrict_ge0. - exact/(measurable_restrict _ mD). Qed. @@ -2659,7 +2666,6 @@ move=> mg a0; have ? : measurable (D `&` [set x | a%:E <= `|g x|]). apply: (@le_trans _ _ (\int[mu]_(x in D `&` [set x | `|g x| >= a%:E]) `|g x|)). rewrite -integral_cstr//; apply: ge0_le_integral => //. - by move=> x _ /=; exact/ltW. - - exact/EFin_measurable_fun/measurable_fun_cst. - by apply: measurable_funT_comp => //; exact: measurable_funS mg. - by move=> x /= []. by apply: subset_integral => //; exact: measurable_funT_comp. @@ -2695,7 +2701,7 @@ Notation mu_int := (integrable mu D). Lemma integrable0 : mu_int (cst 0). Proof. -split; first exact: measurable_fun_cst. +split => //. under eq_integral do rewrite (gee0_abs (lexx 0)). by rewrite integral0. Qed. @@ -2719,12 +2725,12 @@ Qed. Lemma integrableN f : mu_int f -> mu_int (-%E \o f). Proof. move=> [mf foo]; split; last by rewrite /comp; under eq_fun do rewrite abseN. -by rewrite /comp; apply: measurable_funT_comp =>//; exact: emeasurable_fun_minus. +by rewrite /comp; exact: measurable_funT_comp. Qed. Lemma integrablerM (k : R) f : mu_int f -> mu_int (fun x => k%:E * f x). Proof. -move=> [mf foo]; split; first exact: measurable_funeM. +move=> [mf foo]; split; first by auto. under eq_fun do rewrite abseM. by rewrite ge0_integralM// ?lte_mul_pinfty//; exact: measurable_funT_comp. Qed. @@ -2736,10 +2742,10 @@ Qed. Lemma integrableD f g : mu_int f -> mu_int g -> mu_int (f \+ g). Proof. -move=> [mf foo] [mg goo]; split; first exact: emeasurable_funD. +move=> [mf foo] [mg goo]; split; first by auto. apply: (@le_lt_trans _ _ (\int[mu]_(x in D) (`|f x| + `|g x|))). apply: ge0_le_integral => //. - - by apply: measurable_funT_comp => //; exact: emeasurable_funD. + - by apply: measurable_funT_comp => //; auto. - by apply: emeasurable_funD; apply: measurable_funT_comp. - by move=> *; exact: lee_abs_add. by rewrite ge0_integralD //; [exact: lte_add_pinfty| @@ -2783,7 +2789,7 @@ Lemma integral_funeneg_lt_pinfty f : mu_int f -> \int[mu]_(x in D) f^\- x < +oo. Proof. move=> [mf]; apply: le_lt_trans; apply: ge0_le_integral => //. -- by apply: emeasurable_fun_funeneg => //; exact: emeasurable_funN. +- exact: emeasurable_fun_funeneg. - exact: measurable_funT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. rewrite lee0_abs// /funeneg. @@ -2796,7 +2802,7 @@ Lemma integral_funepos_lt_pinfty f : mu_int f -> \int[mu]_(x in D) f^\+ x < +oo. Proof. move=> [mf]; apply: le_lt_trans; apply: ge0_le_integral => //. -- by apply: emeasurable_fun_funepos => //; exact: emeasurable_funN. +- exact: emeasurable_fun_funepos. - exact: measurable_funT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. rewrite lee0_abs// /funepos. @@ -2967,7 +2973,7 @@ Lemma finite_measure_integrable_cst d (T : measurableType d) (R : realType) (mu : {finite_measure set T -> \bar R}) k : mu.-integrable [set: T] (EFin \o cst k). Proof. -split; first exact/EFin_measurable_fun/measurable_fun_cst. +split; first exact/EFin_measurable_fun. have [k0|k0] := leP 0 k. - under eq_integral do rewrite /= ger0_norm//. rewrite integral_cstr//= lte_mul_pinfty// fin_num_fun_lty//. @@ -3272,13 +3278,12 @@ have le_f_M t : D t -> `|f t| <= M%:E * (f' t)%:E. have : 0 <= \int[mu]_(x in D) `|f x| <= `|M|%:E * mu Df_neq0. rewrite integral_ge0//= /Df_neq0 -{2}(setIid D) setIAC -integral_indic//. rewrite -/Df_neq0 -ge0_integralM//; last 2 first. - - by apply: measurable_funT_comp=> //; exact: measurable_fun_indic. + - exact: measurable_funT_comp. - by move=> x ?; rewrite lee_fin. apply: ge0_le_integral => //. - exact: measurable_funT_comp. - by move=> x Dx; rewrite mule_ge0// lee_fin. - - apply: emeasurable_funM; first exact: measurable_fun_cst. - by apply: measurable_funT_comp => //; exact: measurable_fun_indic. + - by apply: emeasurable_funM => //; exact: measurable_funT_comp. - move=> x Dx. rewrite (le_trans (le_f_M _ Dx))// lee_fin /f' indicE. by case: (_ \in _) => //; rewrite ?mulr1 ?mulr0// ler_norm. @@ -3338,8 +3343,7 @@ have -> : (fun x => `|f x|) = (fun x => lim (f_^~ x)). by rewrite min_l// subrr normr0. transitivity (lim (fun n => \int[mu]_(x in D) (f_ n x) )). apply/esym/cvg_lim => //; apply: cvg_monotone_convergence => //. - - move=> n; apply: emeasurable_fun_min => //; first exact: measurable_funT_comp. - exact: measurable_fun_cst. + - by move=> n; apply: emeasurable_fun_min => //; exact: measurable_funT_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. @@ -3357,8 +3361,7 @@ have f_bounded n x : D x -> `|f_ n x| <= n%:R%:E. 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: emeasurable_fun_min => //; - [exact: measurable_funT_comp|exact: measurable_fun_cst]. + by apply: emeasurable_fun_min => //; exact: measurable_funT_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_. @@ -3372,8 +3375,7 @@ move=> mN mD ND mf muN0; rewrite integralEindic//. 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. apply/ae_eq_integral_abs => //. - apply: emeasurable_funM => //; first exact: (measurable_funS mD). - exact/EFin_measurable_fun/measurable_fun_indic. + by apply: emeasurable_funM => //; [exact: (measurable_funS mD)|auto]. exists N; split => // t /= /not_implyP[_]; rewrite indicE. by have [|] := boolP (t \in N); rewrite ?inE ?mule0. Qed. @@ -3420,8 +3422,7 @@ have h1 : mu.-integrable D f <-> mu.-integrable D (fun x => f x * (oneCN x)%:E). 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. + by 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 => //. @@ -3480,13 +3481,9 @@ Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) : Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. rewrite integralEindic// [RHS]integralEindic//. -rewrite (negligible_integral mN)//; last 2 first. - - apply: emeasurable_funM => //. - exact/EFin_measurable_fun/measurable_fun_indic. +rewrite (negligible_integral mN)//; [|by auto|]; last first. - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. -rewrite [RHS](negligible_integral mN)//; last 2 first. - - apply: emeasurable_funM => //. - exact/EFin_measurable_fun/measurable_fun_indic. +rewrite [RHS](negligible_integral mN)//; [|by auto|]; last first. - by move=> x Dx; apply: mule_ge0 => //; [exact: g0|rewrite lee_fin]. - apply: eq_integral => x;rewrite in_setD => /andP[_ xN]. apply: contrapT; rewrite indicE; have [|?] := boolP (x \in D). @@ -3501,11 +3498,8 @@ Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) : ae_eq D f g -> integral mu D f = integral mu D g. Proof. move=> mD mf mg /ae_eq_funeposneg[Dfgp Dfgn]. -rewrite integralE// [in RHS]integralE//; congr (_ - _). - by apply: ge0_ae_eq_integral => //; [exact: emeasurable_fun_funepos| - exact: emeasurable_fun_funepos]. -by apply: ge0_ae_eq_integral => //; [exact: emeasurable_fun_funeneg| - exact: emeasurable_fun_funeneg]. +by rewrite integralE// [in RHS]integralE//; congr (_ - _); + apply: ge0_ae_eq_integral => //; auto. Qed. End ae_eq_integral. @@ -3518,8 +3512,7 @@ Lemma integral_cst d (T : measurableType d) (R : realType) forall r, \int[mu]_(x in D) (cst r) x = r * mu D. Proof. move=> mD; have [D0 r|D0 [r| |]] := eqVneq (mu D) 0. - by rewrite (ae_eq_integral (cst 0))// ?integral0 ?D0 ?mule0//; - [exact: measurable_fun_cst|exact: measurable_fun_cst|exact: ae_eq0]. + by rewrite (ae_eq_integral (cst 0))// ?integral0 ?D0 ?mule0//; exact: ae_eq0. - by rewrite integral_cstr. - by rewrite integral_csty// gt0_mulye// lt0e D0/=. - by rewrite integral_cstNy// gt0_mulNye// lt0e D0/=. @@ -3539,7 +3532,6 @@ move=> mg a0; have ? : measurable (D `&` [set x | (a%:E <= `|g x|)%E]). apply: (@le_trans _ _ (\int[mu]_(x in D `&` [set x | `|g x| >= a%:E]) f `|g x|)). rewrite -integral_cst//; apply: ge0_le_integral => //. - by move=> x _ /=; rewrite f0 // lee_fin ltW. - - exact/measurable_fun_cst. - by move=> x _ /=; rewrite f0. - apply: measurable_funT_comp => //; apply: measurable_funT_comp => //. exact: measurable_funS mg. @@ -3864,7 +3856,7 @@ Qed. Let mgg n : measurable_fun D (fun x => 2%:E * g x - g_ n x). Proof. apply/emeasurable_funB => //; first by apply: measurable_funeM; case: ig. -by apply/measurable_funT_comp => //; exact: emeasurable_funB. +by apply/measurable_funT_comp => //; auto. Qed. Let gg_ge0 n x : D x -> 0 <= 2%:E * g x - g_ n x. @@ -3899,7 +3891,7 @@ rewrite [X in _ <= X -> _](_ : _ = \int[mu]_(x in D) (2%:E * g x) + - - by move=> x Dx /=; rewrite abse_id (le_trans (absfg _ Dx))// lee_abs. suff: mu.-integrable D (fun x => `|f_ n x| + `|f x|). apply: le_integrable => //. - - by apply: measurable_funT_comp => //; exact: emeasurable_funB. + - by apply: measurable_funT_comp => //; auto. - move=> x Dx. by rewrite /g_ abse_id (le_trans (lee_abs_sub _ _))// lee_abs. apply: integrableD; [by []| by []|]. @@ -3919,7 +3911,7 @@ have h n : `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | <= \int[mu]_(x in D) g_ n x. rewrite -(integralB _ _ dominated_integrable)//; last first. by apply: le_integrable ig => // x Dx /=; rewrite (gee0_abs (g0 Dx)) absfg. - by apply: le_abse_integral => //; exact: emeasurable_funB. + by apply: le_abse_integral => //; auto. suff: (fun n => `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x |) --> 0. move/cvg_abse0P/cvge_sub0; apply. rewrite fin_numElt (_ : -oo = - +oo)// -lte_absl. @@ -3996,7 +3988,7 @@ split. + apply: measurable_funT_comp => //; apply: emeasurable_funB => //. apply/(measurable_restrict _ (measurableD _ _) _ _).1 => //. by apply: (measurable_funS mD) => // x []. - + by rewrite /g_; apply: measurable_funT_comp => //; exact: emeasurable_funB. + + by rewrite /g_; apply: measurable_funT_comp => //; auto. + exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f_' /f' /restrict mem_set. - have := @dominated_cvg _ _ _ _ _ mD _ _ _ mu_ f_f' finv ig' f_g'. @@ -4050,13 +4042,13 @@ Implicit Types (A : set (T1 * T2)). Lemma measurable_xsection A x : measurable A -> measurable (xsection A x). Proof. move=> mA; rewrite (xsection_indic R) -(setTI (_ @^-1` _)). -by apply: measurable_fun_prod1 => //; exact/measurable_fun_indic. +exact: measurable_fun_prod1. Qed. Lemma measurable_ysection A y : measurable A -> measurable (ysection A y). Proof. move=> mA; rewrite (ysection_indic R) -(setTI (_ @^-1` _)). -by apply: measurable_fun_prod2 => //; exact/measurable_fun_indic. +exact: measurable_fun_prod2. Qed. End measurable_section. @@ -4135,23 +4127,21 @@ have CI : setI_closed C. have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. have CB : C `<=` B. move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableM. - have -> : phi (X1 `*` X2) = (fun x => m2D X2 * (\1_X1 x)%:E)%E. - rewrite funeqE => x; rewrite indicE /phi /m2/= /mrestr. - have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionM. - by rewrite mule0 notin_xsectionM// set0I measure0. - exact/measurable_funeM/EFin_measurable_fun/measurable_fun_indic. + suff -> : phi (X1 `*` X2) = (fun x => m2D X2 * (\1_X1 x)%:E)%E by auto. + rewrite funeqE => x; rewrite indicE /phi /m2/= /mrestr. + have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionM. + by rewrite mule0 notin_xsectionM// set0I measure0. suff monoB : monotone_class setT B by exact: monotone_class_subset. split => //; [exact: CB| |exact: xsection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. -have -> : phi (X `\` Y) = (fun x => phi X x - phi Y x)%E. - rewrite funeqE => x; rewrite /phi/= xsectionD// /m2D measureD. - - by rewrite setIidr//; exact: le_xsection. - - exact: measurable_xsection. - - exact: measurable_xsection. - - move: m2D_bounded => [M m2M]. - rewrite (lt_le_trans (m2M (xsection X x) _))// ?leey//. - exact: measurable_xsection. -exact: emeasurable_funB. +suff -> : phi (X `\` Y) = (fun x => phi X x - phi Y x)%E by auto. +rewrite funeqE => x; rewrite /phi/= xsectionD// /m2D measureD. +- by rewrite setIidr//; exact: le_xsection. +- exact: measurable_xsection. +- exact: measurable_xsection. +- move: m2D_bounded => [M m2M]. + rewrite (lt_le_trans (m2M (xsection X x) _))// ?leey//. + exact: measurable_xsection. Qed. End xsection. @@ -4176,15 +4166,14 @@ have CI : setI_closed C. have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. have CB : C `<=` B. move=> X [X1 mX1 [X2 mX2 <-{X}]]; split; first exact: measurableM. - have -> : psi (X1 `*` X2) = (fun x => m1D X1 * (\1_X2 x)%:E)%E. - rewrite funeqE => y; rewrite indicE /psi /m1/= /mrestr. - have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionM. - by rewrite mule0 notin_ysectionM// set0I measure0. - exact/measurable_funeM/EFin_measurable_fun/measurable_fun_indic. + suff -> : psi (X1 `*` X2) = (fun x => m1D X1 * (\1_X2 x)%:E)%E by auto. + rewrite funeqE => y; rewrite indicE /psi /m1/= /mrestr. + have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionM. + by rewrite mule0 notin_ysectionM// set0I measure0. suff monoB : monotone_class setT B by exact: monotone_class_subset. split => //; [exact: CB| |exact: ysection_ndseq_closed]. move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD. -rewrite (_ : psi _ = (psi X \- psi Y)%E); first exact: emeasurable_funB. +rewrite (_ : psi _ = (psi X \- psi Y)%E); first by auto. rewrite funeqE => y; rewrite /psi/= ysectionD// /m1D measureD. - by rewrite setIidr//; exact: le_ysection. - exact: measurable_ysection. @@ -4330,7 +4319,7 @@ rewrite (eq_integral (fun x => m2 A2 * (\1_A1 x)%:E)); last first. [rewrite in_xsectionM// mule1|rewrite mule0 notin_xsectionM]. rewrite ge0_integralM//; last by move=> x _; rewrite lee_fin. - by rewrite muleC integral_indic// setIT. -- by apply: measurable_funT_comp => //; exact/measurable_fun_indic. +- exact: measurable_funT_comp. Qed. End product_measure1E. @@ -4430,7 +4419,7 @@ have mA1A2 : measurable (A1 `*` A2) by apply: measurableM. transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //. rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E). rewrite ge0_integralM//; last 2 first. - - by apply: measurable_funT_comp => //; exact/measurable_fun_indic. + - exact: measurable_funT_comp. - by move=> y _; rewrite lee_fin. by rewrite integral_indic ?setIT ?mul1e. rewrite funeqE => y; rewrite indicE. @@ -4525,15 +4514,12 @@ Lemma sfun_fubini_tonelli_FE : F = fun x => Proof. rewrite funeqE => x; rewrite /F /fubini_F [in LHS]/=. under eq_fun do rewrite fimfunE -fsumEFin//. -rewrite ge0_integral_fsum //; last 2 first. - - move=> i; apply/EFin_measurable_fun => //; apply: measurable_funrM => //. - exact/measurable_fun_prod1/measurable_fun_indic. +rewrite ge0_integral_fsum //; [|by auto|]; last first. - by move=> r y _; rewrite EFinM nnfun_muleindic_ge0. apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}]. under eq_fun do rewrite EFinM. -rewrite ge0_integralM//; last by rewrite lee_fin. +rewrite ge0_integralM//; [|by auto| |by rewrite lee_fin]. - by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE. -- exact/EFin_measurable_fun/measurable_fun_prod1/measurable_fun_indic. - by move=> y _; rewrite lee_fin. Qed. @@ -4548,15 +4534,12 @@ Lemma sfun_fubini_tonelli_GE : G = fun y => Proof. rewrite funeqE => y; rewrite /G /fubini_G [in LHS]/=. under eq_fun do rewrite fimfunE -fsumEFin//. -rewrite ge0_integral_fsum //; last 2 first. - - move=> i; apply/EFin_measurable_fun => //; apply: measurable_funrM => //. - exact/measurable_fun_prod2/measurable_fun_indic. +rewrite ge0_integral_fsum //; [|by auto|]; last first. - by move=> r x _; rewrite EFinM nnfun_muleindic_ge0. apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}]. under eq_fun do rewrite EFinM. -rewrite ge0_integralM//; last by rewrite lee_fin. +rewrite ge0_integralM//; [|by auto| |by rewrite lee_fin]. - by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE. -- exact/EFin_measurable_fun/measurable_fun_prod2/measurable_fun_indic. - by move=> x _; rewrite lee_fin. Qed. @@ -4580,8 +4563,7 @@ under [LHS]eq_integral transitivity (\sum_(k \in range f) \int[m1]_x (k%:E * (fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x))). apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}]. - rewrite ge0_integralM//; last 3 first. - - exact/EFin_measurable_fun/measurable_fun_indic. + rewrite ge0_integralM//; [|by auto| |]; last 2 first. - by move=> /= x _; rewrite lee_fin. - by rewrite lee_fin. rewrite indic_fubini_tonelli1// -ge0_integralM//; last by rewrite lee_fin. @@ -4601,14 +4583,12 @@ Lemma sfun_fubini_tonelli2 : \int[m1 \x^ m2]_z (f z)%:E = \int[m2]_y G y. Proof. under [LHS]eq_integral do rewrite EFinf; rewrite ge0_integral_fsum //; last 2 first. - - move=> i. - exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic. + - by move=> i; auto. - by move=> r /= z _; exact: nnfun_muleindic_ge0. transitivity (\sum_(k \in range f) \int[m2]_x (k%:E * (fubini_G m1 (EFin \o \1_(f @^-1` [set k])) x))). apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}]. - rewrite ge0_integralM//; last 3 first. - - exact/EFin_measurable_fun/measurable_fun_indic. + rewrite ge0_integralM//; [|by auto| |]; last 2 first. - by move=> /= x _; rewrite lee_fin. - by rewrite lee_fin. rewrite indic_fubini_tonelli2// -ge0_integralM//; last by rewrite lee_fin. @@ -4654,8 +4634,7 @@ apply: (emeasurable_fun_cvg (F_ g)) => //. rewrite /F_ /F /fubini_F [in X in _ --> X](_ : (fun _ => _) = fun y => lim (EFin \o g ^~ (x, y))); last first. by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: g_f. - apply: cvg_monotone_convergence => //. - - by move=> n; apply/EFin_measurable_fun => //; exact/measurable_fun_prod1. + apply: cvg_monotone_convergence => //; [by auto| |]. - by move=> n y _; rewrite lee_fin//; exact: fun_ge0. - by move=> y _ a b ab; rewrite lee_fin; exact/lefP/g_nd. Qed. @@ -4668,8 +4647,7 @@ apply: (emeasurable_fun_cvg (G_ g)) => //. - move=> y _; rewrite /G_ /G /fubini_G [in X in _ --> X](_ : (fun _ => _) = fun x => lim (EFin \o g ^~ (x, y))); last first. by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: g_f. - apply: cvg_monotone_convergence => //. - - by move=> n; apply/EFin_measurable_fun => //; exact/measurable_fun_prod2. + apply: cvg_monotone_convergence => //; [by auto| |]. - by move=> n x _; rewrite lee_fin; exact: fun_ge0. - by move=> x _ a b ab; rewrite lee_fin; exact/lefP/g_nd. Qed. @@ -4679,14 +4657,12 @@ Proof. have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). have F_F x : F x = lim (F_ g ^~ x). rewrite [RHS](_ : _ = lim (fun n => \int[m2]_y (EFin \o g n) (x, y)))//. - rewrite -monotone_convergence//; last 3 first. - - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod1. + rewrite -monotone_convergence//; [|by move=> ? /=; auto| |]; last 2 first. - by move=> n /= y _; rewrite lee_fin; exact: fun_ge0. - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: g_f. rewrite [RHS](_ : _ = lim (fun n => \int[m1 \x m2]_z (EFin \o g n) z)). - rewrite -monotone_convergence //; last 3 first. - - by move=> n; exact/EFin_measurable_fun. + rewrite -monotone_convergence //; [|by move=> ? /=; auto| |]; last 2 first. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f. @@ -4698,11 +4674,9 @@ rewrite -monotone_convergence //; first exact: eq_integral. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F. - move=> n x _; apply: integral_ge0 => // y _ /=; rewrite lee_fin. exact: fun_ge0. -- move=> x /= _ a b ab; apply: ge0_le_integral => //. +- move=> x /= _ a b ab; apply: ge0_le_integral; [by []| |by auto| |by auto|]. + by move=> y _; rewrite lee_fin; exact: fun_ge0. - + exact/EFin_measurable_fun/measurable_fun_prod1. + by move=> *; rewrite lee_fin; exact: fun_ge0. - + exact/EFin_measurable_fun/measurable_fun_prod1. + by move=> y _; rewrite lee_fin; move/g_nd : ab => /lefP; exact. Qed. @@ -4712,14 +4686,12 @@ have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). have G_G y : G y = lim (G_ g ^~ y). rewrite /G /fubini_G. rewrite [RHS](_ : _ = lim (fun n => \int[m1]_x (EFin \o g n) (x, y)))//. - rewrite -monotone_convergence//; last 3 first. - - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod2. + rewrite -monotone_convergence//; [|by move=> ? /=; auto| |]; last 2 first. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - by move=> x /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. by apply: eq_integral => x _; apply/esym/cvg_lim => //; exact: g_f. rewrite [RHS](_ : _ = lim (fun n => \int[m1 \x m2]_z (EFin \o g n) z)). - rewrite -monotone_convergence //; last 3 first. - - by move=> n; exact/EFin_measurable_fun. + rewrite -monotone_convergence //; [|by move=> /= ?; auto| |]; last 2 first. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f. @@ -4731,11 +4703,9 @@ rewrite [RHS](_ : _ = lim (fun n => \int[m2]_y G_ g n y))//. rewrite -monotone_convergence //; first exact: eq_integral. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G. - by move=> n y _; apply: integral_ge0 => // x _ /=; rewrite lee_fin fun_ge0. -- move=> y /= _ a b ab; apply: ge0_le_integral => //. +- move=> y /= _ a b ab; apply: ge0_le_integral => //; [|by auto| |by auto| ]. + by move=> x _; rewrite lee_fin fun_ge0. - + exact/EFin_measurable_fun/measurable_fun_prod2. + by move=> *; rewrite lee_fin fun_ge0. - + exact/EFin_measurable_fun/measurable_fun_prod2. + by move=> x _; rewrite lee_fin; move/g_nd : ab => /lefP; exact. Qed. @@ -4801,7 +4771,7 @@ have : m1.-integrable setT (fun x => \int[m2]_y `|f (x, y)|). - by move=> *; exact: integral_ge0. - by move=> *; rewrite gee0_abs//; exact: integral_ge0. move/integrable_ae => /(_ measurableT); apply: filterS => x /= /(_ I) im2f. -by split; [exact/measurable_fun_prod1|by move/fin_numPlt : im2f => /andP[]]. +by split; [auto|by move/fin_numPlt : im2f => /andP[]]. Qed. Lemma ae_integrable2 : @@ -4813,7 +4783,7 @@ have : m2.-integrable setT (fun y => \int[m1]_x `|f (x, y)|). - by move=> *; exact: integral_ge0. - by move=> *; rewrite gee0_abs//; exact: integral_ge0. move/integrable_ae => /(_ measurableT); apply: filterS => x /= /(_ I) im2f. -by split; [exact/measurable_fun_prod2|move/fin_numPlt : im2f => /andP[]]. +by split; [auto|move/fin_numPlt : im2f => /andP[]]. Qed. Let F := fubini_F m2 f. @@ -4844,13 +4814,10 @@ Proof. split=> //; apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //. - exact: measurable_funT_comp. - by move=> x _; exact: integral_ge0. -- move=> x _; apply: le_trans. - apply: le_abse_integral => //; apply: emeasurable_fun_funepos => //. - exact: measurable_fun_prod1. +- move=> x _; apply: le_trans; first by apply: le_abse_integral => //; auto. apply: ge0_le_integral => //. - - apply: measurable_funT_comp => //. - by apply: emeasurable_fun_funepos => //; exact: measurable_fun_prod1. - - by apply: measurable_funT_comp => //; exact/measurable_fun_prod1. + - by apply: measurable_funT_comp => //; auto. + - by apply: measurable_funT_comp => //; auto. - by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addl. Qed. @@ -4859,13 +4826,10 @@ Proof. split=> //; apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //. - exact: measurable_funT_comp. - by move=> *; exact: integral_ge0. -- move=> x _; apply: le_trans. - apply: le_abse_integral => //; apply: emeasurable_fun_funeneg => //. - exact: measurable_fun_prod1. +- move=> x _; apply: le_trans; first by apply: le_abse_integral => //; auto. apply: ge0_le_integral => //. - + apply: measurable_funT_comp => //; apply: emeasurable_fun_funeneg => //. - exact: measurable_fun_prod1. - + by apply: measurable_funT_comp => //; exact: measurable_fun_prod1. + + by apply: measurable_funT_comp => //; auto. + + by apply: measurable_funT_comp => //; auto. + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addr. Qed. @@ -4897,13 +4861,10 @@ Proof. split=> //; apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //. - exact: measurable_funT_comp. - by move=> *; exact: integral_ge0. -- move=> y _; apply: le_trans. - apply: le_abse_integral => //; apply: emeasurable_fun_funepos => //. - exact: measurable_fun_prod2. +- move=> y _; apply: le_trans; first by apply: le_abse_integral => //; auto. apply: ge0_le_integral => //. - - apply: measurable_funT_comp => //. - by apply: emeasurable_fun_funepos => //; exact: measurable_fun_prod2. - - by apply: measurable_funT_comp => //; exact: measurable_fun_prod2. + - by apply: measurable_funT_comp => //; auto. + - by apply: measurable_funT_comp => //; auto. - by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addl. Qed. @@ -4912,28 +4873,23 @@ Proof. split=> //; apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //. - exact: measurable_funT_comp. - by move=> *; exact: integral_ge0. -- move=> y _; apply: le_trans. - apply: le_abse_integral => //; apply: emeasurable_fun_funeneg => //. - exact: measurable_fun_prod2. +- move=> y _; apply: le_trans; first by apply: le_abse_integral => //; auto. apply: ge0_le_integral => //. - + apply: measurable_funT_comp => //. - by apply: emeasurable_fun_funeneg => //; exact: measurable_fun_prod2. - + by apply: measurable_funT_comp => //; exact: measurable_fun_prod2. + + by apply: measurable_funT_comp => //; auto. + + by apply: measurable_funT_comp => //; auto. + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addr. Qed. Lemma fubini1 : \int[m1]_x F x = \int[m1 \x m2]_z f z. Proof. rewrite FE integralB; [|by[]|exact: integrable_Fplus|exact: integrable_Fminus]. -by rewrite [in RHS]integralE ?fubini_tonelli1//; - [exact: emeasurable_fun_funeneg|exact: emeasurable_fun_funepos]. +by rewrite [in RHS]integralE ?fubini_tonelli1//; auto. Qed. Lemma fubini2 : \int[m2]_x G x = \int[m1 \x m2]_z f z. Proof. rewrite GE integralB; [|by[]|exact: integrable_Gplus|exact: integrable_Gminus]. -by rewrite [in RHS]integralE ?fubini_tonelli2//; - [exact: emeasurable_fun_funeneg|exact: emeasurable_fun_funepos]. +by rewrite [in RHS]integralE ?fubini_tonelli2//; auto. Qed. Theorem Fubini : @@ -4965,12 +4921,11 @@ transitivity (\sum_(n t _; exact: integral_ge0. rewrite [X in measurable_fun _ X](_ : _ = fun x => \sum_(n x. - by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1. + by apply/funext => x; rewrite ge0_integral_measure_series//; auto. apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0. by move=> k; apply: measurable_fun_fubini_tonelli_F. apply: eq_eseriesr => n _; apply: eq_integral => x _. - by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod1. + by rewrite ge0_integral_measure_series//; auto. transitivity (\sum_(n n _; rewrite integral_nneseries//. by move=> m; exact: measurable_fun_fubini_tonelli_F. @@ -4987,8 +4942,7 @@ transitivity (\int[mseries s2 0]_y \sum_(n n; apply: measurable_fun_fubini_tonelli_G. by move=> n y _; exact: integral_ge0. transitivity (\int[mseries s2 0]_y \int[mseries s1 0]_x f (x, y)). - apply: eq_integral => y _. - by rewrite ge0_integral_measure_series//; exact/measurable_fun_prod2. + by apply: eq_integral => y _; rewrite ge0_integral_measure_series//; auto. transitivity (\int[m2]_y \int[mseries s1 0]_x f (x, y)). by apply: eq_measure_integral => A mA _ /=; rewrite sfinite_measure_seqP. apply: eq_integral => y _; apply: eq_measure_integral => A mA _ /=. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 0621ec8fed..b589f5eb4f 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -859,6 +859,8 @@ move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then case: ifPn => B0; apply/measurableI => //; last exact: measurable_EFin. by apply: measurableU; [exact: measurable_EFin|exact: measurableU]. Qed. +#[global] Hint Extern 0 (measurable_fun _ fine) => + solve [exact: measurable_fun_fine] : core. Section lebesgue_measure_itv. Variable R : realType. @@ -1707,8 +1709,7 @@ rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first. rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP]. apply/measurable_funU; [exact: measurable_itv|exact: measurable_itv|split]. - apply/(@measurable_restrict _ _ _ _ _ setT)=> //; first exact: measurable_itv. - rewrite (_ : _ \_ _ = cst (0:R)); first exact: measurable_fun_cst. - apply/funext => y; rewrite patchE. + rewrite (_ : _ \_ _ = cst (0:R))//; apply/funext => y; rewrite patchE. by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW. - have : {in `]0, +oo[%classic, continuous (@ln R)}. by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. @@ -1719,11 +1720,10 @@ Qed. Lemma measurable_fun_power_pos (R : realType) p : measurable_fun [set: R] (@power_pos R ^~ p). Proof. -apply: measurable_fun_if => //. +apply: measurable_fun_if => [//| |//|]. - apply: (measurable_fun_bool true); rewrite (_ : _ @^-1` _ = [set 0])//. by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx. -- exact: measurable_fun_cst. -- rewrite setTI; apply: (@measurable_fun_comp _ _ _ _ _ _ setT) => //. +- rewrite setTI; apply: measurable_funT_comp => //. by apply: continuous_measurable_fun; exact: continuous_expR. rewrite (_ : _ @^-1` _ = [set~ 0]); last first. by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP. @@ -1771,6 +1771,8 @@ End standard_emeasurable_fun. solve [exact: measurable_fun_abse] : core. #[global] Hint Extern 0 (measurable_fun _ EFin) => solve [exact: measurable_fun_EFin] : core. +#[global] Hint Extern 0 (measurable_fun _ (-%E : \bar _ -> \bar _)) => + exact: emeasurable_fun_minus : core. (* NB: real-valued function *) Lemma EFin_measurable_fun d (T : measurableType d) (R : realType) (D : set T) @@ -1790,13 +1792,10 @@ Proof. move=> mf;rewrite (_ : er_map _ = fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. by apply: funext=> -[]. -apply: measurable_fun_ifT => /=. -+ apply: (measurable_fun_bool true). - rewrite /preimage/= -[X in measurable X]setTI. - by apply/emeasurable_fin_num => //; exact: measurable_fun_id. -+ apply/EFin_measurable_fun/measurable_funT_comp => //. - exact/measurable_fun_fine. -+ exact: measurable_fun_id. +apply: measurable_fun_ifT => //=. +- apply: (measurable_fun_bool true). + by rewrite /preimage/= -[X in measurable X]setTI; exact/emeasurable_fin_num. +- exact/EFin_measurable_fun/measurable_funT_comp. Qed. Section emeasurable_fun. @@ -1844,15 +1843,12 @@ Proof. by apply: measurable_funT_comp => //; exact: emeasurable_fun_minus. Qed. Lemma emeasurable_fun_funepos D (f : T -> \bar R) : measurable_fun D f -> measurable_fun D f^\+. -Proof. -by move=> mf; apply: emeasurable_fun_max => //; exact: measurable_fun_cst. -Qed. +Proof. by move=> mf; apply: emeasurable_fun_max. Qed. Lemma emeasurable_fun_funeneg D (f : T -> \bar R) : measurable_fun D f -> measurable_fun D f^\-. Proof. -by move=> mf; apply: emeasurable_fun_max => //; - [exact: emeasurable_funN|exact: measurable_fun_cst]. +by move=> mf; apply: emeasurable_fun_max => //; exact: emeasurable_funN. Qed. Lemma emeasurable_fun_min D (f g : T -> \bar R) : diff --git a/theories/measure.v b/theories/measure.v index 0f02589f70..315ddacb22 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1124,6 +1124,15 @@ Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Notation measurable_fun_ext := eq_measurable_fun. Arguments measurable_fun_bool {d1 T1 D f} b. +#[global] Hint Extern 0 (measurable_fun _ id) => + solve [exact: measurable_fun_id] : core. +#[global] Hint Extern 0 (measurable_fun _ (cst _)) => + solve [exact: measurable_fun_cst] : core. +#[global] Hint Extern 0 (measurable_fun _ (fun=> _)) => + solve [exact: measurable_fun_cst] : core. +#[global] Hint Extern 0 (measurable_fun _ (GRing.one _)) => + solve [exact: measurable_fun_cst] : core. + Section measurability. Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT) @@ -4075,6 +4084,10 @@ by apply/prod_measurable_funP => /=; split; Qed. End prod_measurable_proj. +#[global] Hint Extern 0 (measurable_fun _ fst) => + solve [exact: measurable_fun_fst] : core. +#[global] Hint Extern 0 (measurable_fun _ snd) => + solve [exact: measurable_fun_snd] : core. Lemma measurable_fun_if_pair d d' (X : measurableType d) (Y : measurableType d') (x y : X -> Y) :