fixes #1345

math-comp · Oct 24, 2024 · 5ad77cc · 5ad77cc
1 parent a4a0ab4
commit 5ad77cc
Show file tree

Hide file tree

Showing 8 changed files with 120 additions and 118 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -57,6 +57,9 @@
 
 ### Renamed
 
+- in `lebesgue_measure.v`:
+  + `EFin_measurable_fun` -> `measurable_EFinP`
+
 ### Generalized
 
 - in `num_topology.v` (new file):

diff --git a/theories/charge.v b/theories/charge.v
@@ -1219,7 +1219,7 @@ rewrite /Rintegral fineK; last first.
   apply: le_lt_trans intfoo.
   apply: ge0_subset_integral => //=.
   apply: measurableT_comp => //.
-  by case/integrableP : intnf => /= /EFin_measurable_fun.
+  by case/integrableP : intnf => /= /measurable_EFinP.
 rewrite -[leLHS](gee0_abs)//; last exact: integral_ge0.
 exact: (le_trans _ (abse_charge_variation _ _)).
 Qed.
@@ -1926,7 +1926,7 @@ have -> : \int[nu]_(x in E) f x =
     by move=> Ex; apply/esym/cvg_lim => //; exact: hf.
   under eq_integral => x /[!inE] /fE -> //.
   apply: monotone_convergence => //.
-  - move=> n; apply/EFin_measurable_fun.
+  - move=> n; apply/measurable_EFinP.
     by apply: (measurable_funS measurableT) => //; exact/measurable_funP.
   - by move=> n x Ex //=; rewrite lee_fin.
   - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP.
@@ -1938,7 +1938,7 @@ have -> : \int[mu]_(x in E) (f \* g) x =
   under eq_integral => x /[!inE] /fg -> //.
   apply: monotone_convergence => [//| | |].
   - move=> n; apply/emeasurable_funM; apply/measurable_funTS.
-      exact/EFin_measurable_fun.
+      exact/measurable_EFinP.
     exact: measurable_int (f_integrable _).
   - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0.
   - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0.
@@ -1970,7 +1970,7 @@ rewrite ge0_integralZl//.
   rewrite (eq_integral (g \_ (h n @^-1` [set r]))); last first.
     by move=> x xE; rewrite epatch_indic.
   by rewrite -integral_mkcondr -f_integral// integral_indic// setIC.
-- apply: emeasurable_funM; first exact/EFin_measurable_fun.
+- apply: emeasurable_funM; first exact/measurable_EFinP.
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
 - by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0.
 - by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin.

diff --git a/theories/ftc.v b/theories/ftc.v
@@ -286,7 +286,7 @@ move=> xu fi F ax fx; suff lfx : lebesgue_pt f x.
   have /(_ ax lfx)[dfx f'xE] := @FTC1_lebesgue_pt _ a _ _ xu fi.
   by split; [exact: dfx|rewrite f'xE].
 apply: itv_continuous_lebesgue_pt xu _ ax fx.
-by move/integrableP : fi => -[/EFin_measurable_fun].
+by move/integrableP : fi => -[/measurable_EFinP].
 Qed.
 
 Corollary continuous_FTC1_closed f (a x : R) (u : R) : (x < u)%R ->

diff --git a/theories/hoelder.v b/theories/hoelder.v
@@ -387,24 +387,24 @@ pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E.
 apply: (@le_lt_trans _ _ x).
   rewrite ge0_le_integral//=.
   - by move=> t _; rewrite lee_fin// powR_ge0.
-  - apply/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp => //.
+  - apply/measurable_EFinP/measurableT_comp_powR/measurableT_comp => //.
     exact: measurable_funD.
   - by move=> t _; rewrite lee_fin mulr_ge0 ?addr_ge0 ?powR_ge0.
-  - by apply/EFin_measurable_fun/measurable_funM/measurable_funD => //;
+  - by apply/measurable_EFinP/measurable_funM/measurable_funD => //;
       exact/measurableT_comp_powR/measurableT_comp.
   - by move=> ? _; rewrite lee_fin.
 rewrite {}/x; under eq_integral do rewrite EFinM.
 rewrite ge0_integralZl_EFin ?powR_ge0//; last 2 first.
   - by move=> x _; rewrite lee_fin addr_ge0// powR_ge0.
-  - by apply/EFin_measurable_fun/measurable_funD => //;
+  - by apply/measurable_EFinP/measurable_funD => //;
       exact/measurableT_comp_powR/measurableT_comp.
 rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//.
 under eq_integral do rewrite EFinD.
 rewrite ge0_integralD//; last 4 first.
   - by move=> x _; rewrite lee_fin powR_ge0.
-  - exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp.
+  - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
   - by move=> x _; rewrite lee_fin powR_ge0.
-  - exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp.
+  - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
 by rewrite lte_add_pinfty// -powR_Lnorm ?(gt_eqF (lt_trans _ p1))// poweR_lty.
 Qed.
 

diff --git a/theories/kernel.v b/theories/kernel.v
@@ -456,7 +456,7 @@ have CXY : C `<=` XY.
   move=> _ [A mA [B mB <-]]; split; first exact: measurableX.
   rewrite phiM.
   apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI.
-  by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA).
+  by apply/measurable_EFinP; rewrite (_ : \1_ _ = mindic R mA).
 suff lsystemB : lambda_system setT XY by exact: lambda_system_subset.
 split => //; [exact: CXY| |exact: xsection_ndseq_closed].
 move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD.
@@ -522,13 +522,13 @@ rewrite (_ : (fun x => _) =
     apply: ereal_nondecreasing_is_cvgn => m n mn.
     apply: ge0_le_integral => //.
     - by move=> y _; rewrite lee_fin.
-    - exact/EFin_measurable_fun/measurableT_comp.
+    - exact/measurable_EFinP/measurableT_comp.
     - by move=> y _; rewrite lee_fin.
-    - exact/EFin_measurable_fun/measurableT_comp.
+    - exact/measurable_EFinP/measurableT_comp.
     - by move=> y _; rewrite lee_fin; exact/lefP/ndk_.
   rewrite -monotone_convergence//.
   - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k.
-  - by move=> n; exact/EFin_measurable_fun/measurableT_comp.
+  - by move=> n; exact/measurable_EFinP/measurableT_comp.
   - by move=> n y _; rewrite lee_fin.
   - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_.
 apply: measurable_fun_limn_esup => n.
@@ -541,7 +541,7 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n))
   apply/funext => x; rewrite -ge0_integral_fsum//.
   - by apply: eq_integral => y _; rewrite -fsumEFin.
   - move=> r.
-    apply/EFin_measurable_fun/measurableT_comp => [//|].
+    apply/measurable_EFinP/measurableT_comp => [//|].
     exact/measurableT_comp.
   - by move=> m y _; rewrite nnfun_muleindic_ge0.
 apply: emeasurable_fun_fsum => // r.
@@ -550,7 +550,7 @@ rewrite [X in measurable_fun _ X](_ : _ = fun x => r%:E *
   apply/funext => x; under eq_integral do rewrite EFinM.
   have [r0|r0] := leP 0%R r.
     rewrite ge0_integralZl//; last by move=> *; rewrite lee_fin.
-    exact/EFin_measurable_fun/measurableT_comp.
+    exact/measurable_EFinP/measurableT_comp.
   rewrite integral0_eq; last first.
     by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
   by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0.
@@ -607,7 +607,7 @@ Hypothesis mf : measurable_fun [set: X] f.
 Let measurable_fun_kdirac U : measurable U ->
   measurable_fun [set: X] (kdirac mf ^~ U).
 Proof.
-move=> mU; apply/EFin_measurable_fun.
+move=> mU; apply/measurable_EFinP.
 by rewrite (_ : (fun x => _) = mindic R mU \o f)//; exact/measurableT_comp.
 Qed.
 
@@ -742,7 +742,7 @@ apply: measurable_fun_if => //.
   exact: kernel_measurable_fun_eq_cst.
 - apply: emeasurable_funM.
     exact: measurable_funS (measurable_kernel f U mU).
-  apply/EFin_measurable_fun.
+  apply/measurable_EFinP.
   apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //.
   + exact: open_measurable.
   + move=> /= r [t] [] [_ ft0] ftoo ftr; apply/eqP => r0.
@@ -787,7 +787,7 @@ apply: measurable_fun_if => //.
     by apply/seteqP; split=> x /= /orP.
   by rewrite setTI; apply: measurableU; exact: kernel_measurable_eq_cst.
 - apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
-  apply/EFin_measurable_fun; rewrite setTI.
+  apply/measurable_EFinP; rewrite setTI.
   apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
   + exact: open_measurable.
   + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
@@ -1022,7 +1022,7 @@ Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) :
 Proof.
 under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//.
 rewrite ge0_integral_fsum//; last 2 first.
-  - move=> r; apply/EFin_measurable_fun/measurableT_comp => [//|].
+  - move=> r; apply/measurable_EFinP/measurableT_comp => [//|].
     have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
     by rewrite (_ : \1__ = mindic R fr).
   - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
@@ -1031,7 +1031,7 @@ under [in RHS]eq_integral.
   under eq_integral.
     by move=> z _; rewrite fimfunE -fsumEFin//; over.
   rewrite /= ge0_integral_fsum//; last 2 first.
-    - move=> r; apply/EFin_measurable_fun/measurableT_comp => [//|].
+    - move=> r; apply/measurable_EFinP/measurableT_comp => [//|].
       have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
       by rewrite (_ : \1__ = mindic R fr).
     - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
@@ -1070,7 +1070,7 @@ have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z).
 transitivity (\int[kcomp l k x]_z (lim ((f_ n z)%:E @[n --> \oo]))).
   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.
+  by move=> n; exact/measurable_EFinP.
   by move=> n z _; rewrite lee_fin.
   by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin.
 rewrite (_ : (fun _ => _) =
@@ -1081,16 +1081,16 @@ transitivity (\int[l x]_y lim ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])).
   - move=> n; apply: measurable_fun_integral_kernel => //.
     + by move=> U mU; exact: measurableT_comp (measurable_kernel k _ mU) _.
     + by move=> z; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
+    + exact/measurable_EFinP.
   - by move=> n y _; apply: integral_ge0 => // z _; rewrite lee_fin.
   - move=> y _ a b ab; apply: ge0_le_integral => //.
     + by move=> z _; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
+    + exact/measurable_EFinP.
     + by move=> z _; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
+    + exact/measurable_EFinP.
     + 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; exact/measurable_EFinP.
   - 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.