Refactoring lemmas about composition in Lebesgue Measure (#925)

favor use of `measurable_fun_comp` Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]> Co-authored-by: affeldt-aist <[email protected]>
math-comp · May 15, 2023 · f30efd2 · f30efd2
1 parent 6d08bc0
commit f30efd2
Show file tree

Hide file tree

Showing 5 changed files with 129 additions and 116 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -12,6 +12,8 @@
   + lemma `measurable_fun_bigcup`
 - in `sequences.v`:
   + lemma `eq_eseriesl`
+- in `lebesgue_measure.v`:
+  + lemma `measurable_fun_expR`
 
 - in file `topology.v`,
   + new definitions `basis`, and `second_countable`.
@@ -44,6 +46,8 @@
 
 ### Changed
 
+- in `lebesgue_measure.v`
+  + `measurable_funrM`, `measurable_funN`, `measurable_fun_exprn`
 - in `lebesgue_integral.v`:
   + lemma `xsection_ndseq_closed` generalized from a measure to a family of measures
 
@@ -63,13 +67,19 @@
 
 ### Deprecated
 
+- in `lebesgue_measure.v`:
+  + lemma `measurable_fun_sqr` (use `measurable_fun_exprn` instead)
+  + lemma `measurable_fun_opp` (use `measurable_funN` instead)
+
 ### Removed
 
 - in `normedtype.v`:
   + instance `Proper_dnbhs_realType`
 - in `measure.v`:
   + instances `ae_filter_algebraOfSetsType`, `ae_filter_measurableType`,
   `ae_properfilter_measurableType`
+- in `lebesgue_measure.v`:
+  + lemma `emeasurable_funN` (use `measurable_funT_comp`) instead
 - in `lebesgue_integral.v`
   + lemma `emeasurable_funN` (already in `lebesgue_measure.v`)
 

diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -146,7 +146,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 split. Qed.
 HB.instance Definition _ x := @cst_mfun_subproof x.
 Definition cst_mfun x := [the {mfun aT >-> rT} of cst x].
 
@@ -239,6 +239,9 @@ Proof.
 by move=> mA; apply/measurable_funTS; rewrite (_ : \1__ = mindic R mA).
 Qed.
 
+#[global] Hint Extern 0  (measurable_fun _ (\1__ : _ -> _)) =>
+  (exact: measurable_fun_indic ) : core.
+
 Section sfun_pred.
 Context {d} {aT : measurableType d} {rT : realType}.
 Definition sfun : {pred _ -> _} := [predI @mfun _ aT rT & fimfun].
@@ -1599,12 +1602,10 @@ 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 exact: emeasurable_fun_max.
 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].
+  by apply: emeasurable_fun_max => //; exact: measurable_funT_comp.
 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 /=.
@@ -1700,7 +1701,7 @@ Qed.
 Lemma emeasurable_funB D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \- g).
 Proof.
-by move=> mf mg mD; apply: emeasurable_funD => //; exact: emeasurable_funN.
+by move=> mf mg mD; apply: emeasurable_funD => //; exact: measurable_funT_comp.
 Qed.
 
 Lemma emeasurable_funM D f g :
@@ -1757,7 +1758,7 @@ 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.
 
@@ -2144,7 +2145,7 @@ 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.
+  apply/EFin_measurable_fun/measurable_funT_comp => //=. 
   - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
 rewrite -[RHS]ge0_integralM//; last 2 first.
   - exact/EFin_measurable_fun/measurable_funTS.
@@ -2154,12 +2155,12 @@ 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.
+  - move=> r; apply/EFin_measurable_fun/measurable_funT_comp => //=. 
+   apply: measurable_funT_comp => //= . 
   - by move=> n x _; rewrite EFinM mule_ge0// nnfun_muleindic_ge0.
 apply: eq_fsbigr => r _; rewrite ge0_integralM//.
 - by rewrite !integralM_indic_nnsfun//= integral_mscale_indic// muleCA.
-- exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic.
+- apply/EFin_measurable_fun/measurable_funT_comp => //= . 
 - by move=> t _; rewrite nnfun_muleindic_ge0.
 Qed.
 
@@ -2355,18 +2356,14 @@ 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))).
+    - by move=> y; apply/EFin_measurable_fun; exact: measurable_funM.
     - 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)).
+  - by move=> r; apply/EFin_measurable_fun; exact: measurable_funM.
   - by move=> r x _; rewrite nnfun_muleindic_ge0.
 by apply: eq_integral => x _; rewrite fsumEFin// -fimfunE.
 Qed.
@@ -2401,7 +2398,7 @@ rewrite ge0_integral_fsum//.
   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.
+-  move=> r; apply/EFin_measurable_fun/measurable_funT_comp => //=.
 - by move=> r x _; rewrite nnfun_muleindic_ge0.
 Qed.
 
@@ -2439,7 +2436,7 @@ 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.
+  apply: measurable_funT_comp => //. 
   - 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)).
@@ -2549,7 +2546,7 @@ 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.
+  apply: measurable_funT_comp => //.
   - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0.
 transitivity (\sum_(i \in range f)
     (\sum_(n <oo) i%:E * \int[m_ n]_x (\1_(f @^-1` [set i]) x)%:E)).
@@ -2689,7 +2686,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.
@@ -2725,8 +2721,7 @@ Notation mu_int := (integrable mu D).
 
 Lemma integrable0 : mu_int (cst 0).
 Proof.
-split; first exact: measurable_fun_cst.
-under eq_integral do rewrite (gee0_abs (lexx 0)).
+split => //; under eq_integral do rewrite (gee0_abs (lexx 0)).
 by rewrite integral0.
 Qed.
 
@@ -2997,7 +2992,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//.
@@ -3043,7 +3038,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
     by case: fint => _ foo; rewrite ge0_fin_numE//; exact: integral_ge0.
   apply: ge0_le_integral => //.
   - by move=> *; rewrite lee_fin /indic.
-  - exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic.
+  - apply/EFin_measurable_fun/measurable_funT_comp => //=.  
   - by apply: measurable_funT_comp => //; case: fint.
   - move=> x Dx; rewrite /= indicE.
     have [|xE] := boolP (x \in E); last by rewrite mule0.
@@ -3172,7 +3167,7 @@ rewrite (ge0_integralD mu mD); last 4 first.
   - by [].
   - by apply/emeasurable_fun_funepos/emeasurable_funD; [case: if1|case: if2].
   - by [].
-  - by apply/emeasurable_fun_funepos/emeasurable_funN => //; case: if1.
+  - by apply/emeasurable_fun_funepos/measurable_funT_comp => //; case: if1.
 move=> ->.
 rewrite (ge0_integralD mu mD); last 4 first.
   - by move=> x _; exact: adde_ge0.
@@ -3307,7 +3302,7 @@ have : 0 <= \int[mu]_(x in D) `|f x|  <= `|M|%:E * mu Df_neq0.
   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.
+  - apply: emeasurable_funM => //.
     by apply: measurable_funT_comp => //; exact: measurable_fun_indic.
   - move=> x Dx.
     rewrite (le_trans (le_f_M _ Dx))// lee_fin /f' indicE.
@@ -3368,8 +3363,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.
@@ -3387,8 +3381,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_.
@@ -3548,8 +3541,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/=.
@@ -3569,7 +3561,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.
@@ -4146,13 +4137,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.
@@ -4235,7 +4226,7 @@ have CB : C `<=` B.
     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.
+  exact/measurable_funeM/EFin_measurable_fun.
 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.
@@ -4276,7 +4267,7 @@ have CB : C `<=` B.
     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.
+  exact/measurable_funeM/EFin_measurable_fun.
 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.
@@ -4426,7 +4417,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.
@@ -4526,7 +4517,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.
@@ -4622,14 +4613,14 @@ 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 => //.
+  - move=> i; apply/EFin_measurable_fun / measurable_funT_comp => //=.
     exact/measurable_fun_prod1/measurable_fun_indic.
   - 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.
 - by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE.
-- exact/EFin_measurable_fun/measurable_fun_prod1/measurable_fun_indic.
+- exact/EFin_measurable_fun/measurable_fun_prod1.
 - by move=> y _; rewrite lee_fin.
 Qed.
 
@@ -4645,14 +4636,14 @@ 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.
+  - move=> i; apply/EFin_measurable_fun/ measurable_funT_comp => //=.
+    exact/measurable_fun_prod2.
   - 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.
 - by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE.
-- exact/EFin_measurable_fun/measurable_fun_prod2/measurable_fun_indic.
+- exact/EFin_measurable_fun/measurable_fun_prod2.
 - by move=> x _; rewrite lee_fin.
 Qed.
 
@@ -4671,13 +4662,13 @@ Proof.
 under [LHS]eq_integral
   do rewrite EFinf; rewrite ge0_integral_fsum //; last 2 first.
   - move=> r.
-    exact/EFin_measurable_fun/measurable_funrM/measurable_fun_indic.
+    apply/EFin_measurable_fun/measurable_funT_comp => //=.
   - by move=> r /= z _; exact: nnfun_muleindic_ge0.
 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.
+    - exact/EFin_measurable_fun.
     - by move=> /= x _; rewrite lee_fin.
     - by rewrite lee_fin.
   rewrite indic_fubini_tonelli1// -ge0_integralM//; last by rewrite lee_fin.
@@ -4698,13 +4689,13 @@ 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.
+  apply/EFin_measurable_fun/measurable_funT_comp => //=.
   - 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.
+    - exact/EFin_measurable_fun.
     - by move=> /= x _; rewrite lee_fin.
     - by rewrite lee_fin.
   rewrite indic_fubini_tonelli2// -ge0_integralM//; last by rewrite lee_fin.