Measurable realfun 20250430

CHANGELOG_UNRELEASED.md

@@ -23,8 +23,15 @@
   + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
   + lemmas `inr_in_set_inl`, `inl_in_set_inl`
 
-- in `lebesgue_integral_approximation.v`:
+- in `lebesgue_integral_approximation.v` (now `measurable_fun_approximation.v`):
   + lemma `measurable_prod`
+  + lemma `measurable_fun_lte`
+  + lemma `measurable_fun_lee`
+  + lemma `measurable_fun_eqe`
+  + lemma `measurable_poweR`
+
+- in `exp.v`:
+  + lemma `poweRE`
 
 ### Changed
 
@@ -36,6 +43,14 @@
 - in `kernel.v`:
   + `isFiniteTransition` -> `isFiniteTransitionKernel`
 
+- in `lebesgue_integral_approximation.v`:
+  + `emeasurable_fun_lt` -> `measurable_lte`
+  + `emeasurable_fun_le` -> `measurable_lee`
+  + `emeasurable_fun_eq` -> `measurable_lee`
+  + `emeasurable_fun_neq` -> `measurable_neqe`
+
+- file `lebesgue_integral_approximation.v` -> `measurable_fun_approximation.v`
+
 ### Generalized
 
 ### Deprecated

_CoqProject

@@ -99,7 +99,7 @@ theories/numfun.v
 
 theories/lebesgue_integral_theory/simple_functions.v
 theories/lebesgue_integral_theory/lebesgue_integral_definition.v
-theories/lebesgue_integral_theory/lebesgue_integral_approximation.v
+theories/lebesgue_integral_theory/measurable_fun_approximation.v
 theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
 theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
 theories/lebesgue_integral_theory/lebesgue_integrable.v

theories/Make

@@ -63,7 +63,7 @@ numfun.v
 
 lebesgue_integral_theory/simple_functions.v
 lebesgue_integral_theory/lebesgue_integral_definition.v
-lebesgue_integral_theory/lebesgue_integral_approximation.v
+lebesgue_integral_theory/measurable_fun_approximation.v
 lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
 lebesgue_integral_theory/lebesgue_integral_nonneg.v
 lebesgue_integral_theory/lebesgue_integrable.v

theories/charge.v

@@ -1405,12 +1405,12 @@ Lemma measurable_is_max_approxRN m j : measurable (E m j).
 Proof.
 rewrite is_max_approxRNE; apply: measurableI => /=.
   rewrite -[X in measurable X]setTI.
-  by apply: emeasurable_fun_eq => //; [exact: measurable_max_approxRN_seq|
-                                       exact: measurable_approxRN_seq].
+  by apply: measurable_eqe => //; [exact: measurable_max_approxRN_seq|
+                                   exact: measurable_approxRN_seq].
 rewrite [T in measurable T](_ : _ =
   \bigcap_(k in `I_j) [set x | g_ k x < g_ j x])//.
 apply: bigcap_measurableType => k _.
-by rewrite -[X in measurable X]setTI; apply: emeasurable_fun_lt => //;
+by rewrite -[X in measurable X]setTI; apply: measurable_lte => //;
   exact: measurable_approxRN_seq.
 Qed.
 

theories/exp.v

@@ -1093,6 +1093,21 @@ Proof. by case: x => // x xf; rewrite poweR_EFin powRN. Qed.
 Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0.
 Proof. by move=> r0 /=; rewrite (negbTE r0). Qed.
 
+Lemma poweRE x r :
+  poweR x r = if r == 0%R then
+                (if x \is a fin_num then fine x `^ r else 1)%:E
+               else if x == +oo then +oo
+                    else if x == -oo then 0
+                    else (fine x `^ r)%:E.
+Proof.
+case: ifPn => [/eqP r0|r0].
+  case: ifPn => finx; last by rewrite r0 poweRe0.
+  by rewrite -poweR_EFin; case: x finx.
+case: ifPn => [/eqP ->|xy]; first by rewrite poweRyr.
+case: ifPn => [/eqP ->|xNy]; first by rewrite poweRNyr.
+by rewrite -poweR_EFin// fineK// fin_numE xNy.
+Qed.
+
 Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo.
 Proof. by case: x => [x| |] //=; case: ifP. Qed.
 

theories/ftc.v

@@ -70,15 +70,15 @@ Lemma integrable_locally f (A : set R) : measurable A ->
 Proof.
 move=> mA intf; split.
 - move/integrableP : intf => [mf _].
-  by apply/(measurable_restrictT _ _).1 => //; exact/EFin_measurable_fun.
+  by apply/(measurable_restrictT _ _).1 => //; exact/measurable_EFinP.
 - exact: openT.
 - move=> K _ cK.
   move/integrableP : intf => [mf].
   rewrite integral_mkcond/=.
   under eq_integral do rewrite restrict_EFin restrict_normr.
   apply: le_lt_trans.
   apply: ge0_subset_integral => //=; first exact: compact_measurable.
-  apply/EFin_measurable_fun/measurableT_comp/EFin_measurable_fun => //=.
+  apply/measurable_EFinP/measurableT_comp/measurable_EFinP => //=.
   move/(measurable_restrictT _ _).1 : mf => /=.
   by rewrite restrict_EFin; exact.
 Qed.

theories/lebesgue_integral_theory/lebesgue_Rintegral.v

@@ -7,8 +7,8 @@ From mathcomp Require Import cardinality reals fsbigop interval_inference ereal.
 From mathcomp Require Import topology tvs normedtype sequences real_interval.
 From mathcomp Require Import function_spaces esum measure lebesgue_measure.
 From mathcomp Require Import numfun realfun simple_functions.
+From mathcomp Require Import measurable_fun_approximation.
 From mathcomp Require Import lebesgue_integral_definition.
-From mathcomp Require Import lebesgue_integral_approximation.
 From mathcomp Require Import lebesgue_integral_monotone_convergence.
 From mathcomp Require Import lebesgue_integral_nonneg.
 From mathcomp Require Import lebesgue_integrable.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -7,8 +7,8 @@ From mathcomp Require Import functions cardinality reals fsbigop.
 From mathcomp Require Import interval_inference topology ereal tvs normedtype.
 From mathcomp Require Import sequences real_interval function_spaces esum.
 From mathcomp Require Import measure lebesgue_measure numfun realfun.
-From mathcomp Require Import simple_functions lebesgue_integral_definition.
-From mathcomp Require Import lebesgue_integral_approximation.
+From mathcomp Require Import simple_functions measurable_fun_approximation.
+From mathcomp Require Import lebesgue_integral_definition.
 From mathcomp Require Import lebesgue_integral_monotone_convergence.
 From mathcomp Require Import lebesgue_integral_nonneg.
 
@@ -982,7 +982,7 @@ move=> itf itg fg; pose E j := D `&` [set x | f x - g x >= j.+1%:R^-1%:E].
 have msf := measurable_int _ itf.
 have msg := measurable_int _ itg.
 have mE j : measurable (E j).
-  rewrite /E; apply: emeasurable_fun_le => //.
+  rewrite /E; apply: measurable_lee => //.
   by apply/(emeasurable_funD msf)/measurableT_comp => //; case: mg.
 have muE j : mu (E j) = 0.
   apply/eqP; rewrite -measure_le0.
@@ -1031,12 +1031,9 @@ have mufg : mu (D `&` [set x | f x < g x]) = 0.
 have h : ~` [set x | D x -> f x = g x] = D `&` [set x | f x != g x].
   apply/seteqP; split => [x/= /not_implyP[? /eqP]//|x/= [Dx fgx]].
   by apply/not_implyP; split => //; exact/eqP.
-apply/negligibleP.
-  by rewrite h; apply: emeasurable_fun_neq.
-rewrite h set_neq_lt setIUr measureU//.
+apply/negligibleP; first by rewrite h; apply: measurable_neqe.
+rewrite h set_neq_lt setIUr measureU//; [|exact: measurable_lte..|].
 - by rewrite [X in X + _]mufg add0e [LHS]mugf.
-- exact: emeasurable_fun_lt.
-- exact: emeasurable_fun_lt.
 - apply/seteqP; split => [x [[Dx/= + [_]]]|//].
   by move=> /lt_trans => /[apply]; rewrite ltxx.
 Qed.

theories/lebesgue_integral_theory/lebesgue_integral.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Export simple_functions.
+From mathcomp Require Export measurable_fun_approximation.
 From mathcomp Require Export lebesgue_integral_definition.
-From mathcomp Require Export lebesgue_integral_approximation.
 From mathcomp Require Export lebesgue_integral_monotone_convergence.
 From mathcomp Require Export lebesgue_integral_nonneg.
 From mathcomp Require Export lebesgue_integrable.

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -7,8 +7,8 @@ From mathcomp Require Import cardinality reals fsbigop interval_inference ereal.
 From mathcomp Require Import topology tvs normedtype sequences real_interval.
 From mathcomp Require Import esum function_spaces measure lebesgue_measure.
 From mathcomp Require Import numfun realfun simple_functions.
+From mathcomp Require Import measurable_fun_approximation.
 From mathcomp Require Import lebesgue_integral_definition.
-From mathcomp Require Import lebesgue_integral_approximation.
 From mathcomp Require Import lebesgue_integral_monotone_convergence.
 From mathcomp Require Import lebesgue_integral_nonneg.
 From mathcomp Require Import lebesgue_integrable.

theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v

@@ -7,8 +7,8 @@ From mathcomp Require Import cardinality reals fsbigop interval_inference ereal.
 From mathcomp Require Import topology tvs normedtype sequences real_interval.
 From mathcomp Require Import function_spaces esum measure lebesgue_measure.
 From mathcomp Require Import numfun realfun simple_functions.
+From mathcomp Require Import measurable_fun_approximation.
 From mathcomp Require Import lebesgue_integral_definition.
-From mathcomp Require Import lebesgue_integral_approximation.
 From mathcomp Require Import lebesgue_integral_monotone_convergence.
 From mathcomp Require Import lebesgue_integral_nonneg.
 From mathcomp Require Import lebesgue_integrable.

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -7,8 +7,8 @@ From mathcomp Require Import cardinality reals fsbigop interval_inference ereal.
 From mathcomp Require Import topology tvs normedtype sequences real_interval.
 From mathcomp Require Import esum measure lebesgue_measure numfun realfun.
 From mathcomp Require Import function_spaces simple_functions.
+From mathcomp Require Import measurable_fun_approximation.
 From mathcomp Require Import lebesgue_integral_definition.
-From mathcomp Require Import lebesgue_integral_approximation.
 From mathcomp Require Import lebesgue_integral_monotone_convergence.
 From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.
 

theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v

@@ -7,8 +7,8 @@ From mathcomp Require Import functions cardinality reals fsbigop.
 From mathcomp Require Import interval_inference topology ereal tvs normedtype.
 From mathcomp Require Import sequences real_interval function_spaces esum.
 From mathcomp Require Import measure lebesgue_measure numfun realfun.
-From mathcomp Require Import simple_functions lebesgue_integral_definition.
-From mathcomp Require Import lebesgue_integral_approximation.
+From mathcomp Require Import simple_functions measurable_fun_approximation.
+From mathcomp Require Import lebesgue_integral_definition.
 
 (**md**************************************************************************)
 (* # Monotone convergence theorem for the Lebesgue Integral                   *)

theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v

@@ -7,8 +7,8 @@ From mathcomp Require Import functions cardinality reals fsbigop.
 From mathcomp Require Import interval_inference topology ereal tvs normedtype.
 From mathcomp Require Import sequences real_interval function_spaces esum.
 From mathcomp Require Import measure lebesgue_measure numfun realfun.
-From mathcomp Require Import simple_functions lebesgue_integral_definition.
-From mathcomp Require Import lebesgue_integral_approximation.
+From mathcomp Require Import simple_functions measurable_fun_approximation.
+From mathcomp Require Import lebesgue_integral_definition.
 From mathcomp Require Import lebesgue_integral_monotone_convergence.
 
 (**md**************************************************************************)
@@ -138,7 +138,7 @@ rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h1 x) kg).
 - by move=> x m n mn; rewrite /kg ler_pM//; exact/lefP/nd_nnsfun_approx.
 - move=> x.
   rewrite [X in X @ \oo --> _](_ : _ = (fun n => k%:E * (g n x)%:E)) ?funeqE//.
-  exact/cvgeMl/cvg_nnsfun_approx.
+  exact/cvgeZl/cvg_nnsfun_approx.
 Qed.
 
 End ge0_integralZl_EFin.

theories/lebesgue_integral_theory/lebesgue_integral_approximation.v → theories/lebesgue_integral_theory/measurable_fun_approximation.v

@@ -6,11 +6,11 @@ From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
 From mathcomp Require Import functions cardinality reals fsbigop.
 From mathcomp Require Import interval_inference topology ereal tvs normedtype.
 From mathcomp Require Import sequences real_interval function_spaces esum.
-From mathcomp Require Import measure lebesgue_measure numfun realfun.
-From mathcomp Require Import simple_functions lebesgue_integral_definition.
+From mathcomp Require Import measure lebesgue_measure numfun realfun exp.
+From mathcomp Require Import simple_functions.
 
 (**md**************************************************************************)
-(* # Approximation theorem for the Lebesgue integral                          *)
+(* # Approximation theorem for measurable functions                           *)
 (*                                                                            *)
 (* Applications: measurability of arithmetic of functions, Lusin's theorem.   *)
 (*                                                                            *)
@@ -605,35 +605,93 @@ Context d {T : measurableType d} {R : realType}.
 Variables (D : set T) (mD : measurable D).
 Implicit Types f g : T -> \bar R.
 
-Lemma emeasurable_fun_lt f g : measurable_fun D f -> measurable_fun D g ->
+Lemma measurable_lte f g : measurable_fun D f -> measurable_fun D g ->
   measurable (D `&` [set x | f x < g x]).
 Proof.
 move=> mf mg; under eq_set do rewrite -sube_gt0.
 by apply: emeasurable_fun_o_infty => //; exact: emeasurable_funB.
 Qed.
 
-Lemma emeasurable_fun_le f g : measurable_fun D f -> measurable_fun D g ->
+Lemma measurable_lee f g : measurable_fun D f -> measurable_fun D g ->
   measurable (D `&` [set x | f x <= g x]).
 Proof.
 move=> mf mg; under eq_set do rewrite -sube_le0.
 by apply: emeasurable_fun_infty_c => //; exact: emeasurable_funB.
 Qed.
 
-Lemma emeasurable_fun_eq f g : measurable_fun D f -> measurable_fun D g ->
+Lemma measurable_eqe f g : measurable_fun D f -> measurable_fun D g ->
   measurable (D `&` [set x | f x = g x]).
 Proof.
 move=> mf mg; rewrite set_eq_le setIIr.
-by apply: measurableI; apply: emeasurable_fun_le.
+by apply: measurableI; exact: measurable_lee.
 Qed.
 
-Lemma emeasurable_fun_neq f g : measurable_fun D f -> measurable_fun D g ->
+Lemma measurable_neqe f g : measurable_fun D f -> measurable_fun D g ->
   measurable (D `&` [set x | f x != g x]).
 Proof.
 move=> mf mg; rewrite set_neq_lt setIUr.
-by apply: measurableU; exact: emeasurable_fun_lt.
+by apply: measurableU; exact: measurable_lte.
 Qed.
 
 End emeasurable_comparison.
+#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `measurable_lte`")]
+Notation emeasurable_fun_lt := measurable_lte (only parsing).
+#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `measurable_lee`")]
+Notation emeasurable_fun_le := measurable_lee (only parsing).
+#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `measurable_eqe`")]
+Notation emeasurable_fun_eq := measurable_eqe (only parsing).
+#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `measurable_neqe`")]
+Notation emeasurable_fun_neq := measurable_neqe (only parsing).
+
+Section emeasurable_fun_comparison.
+Context d (T : measurableType d) (R : realType).
+Implicit Types (D : set T) (f g : T -> \bar R).
+Local Open Scope ereal_scope.
+
+Lemma measurable_fun_lte D f g : measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x < g x).
+Proof.
+move=> mf mg mD; apply: (measurable_fun_bool true) => //.
+exact: measurable_lte.
+Qed.
+
+Lemma measurable_fun_lee D f g : measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x <= g x).
+Proof.
+move=> mf mg mD; apply: (measurable_fun_bool true) => //.
+exact: measurable_lee.
+Qed.
+
+Lemma measurable_fun_eqe D f g : measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x == g x).
+Proof.
+move=> mf mg.
+rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))).
+  by apply: measurable_and; exact: measurable_fun_lee.
+by under eq_fun do rewrite eq_le.
+Qed.
+
+End emeasurable_fun_comparison.
+
+Lemma measurable_poweR (R : realType) r :
+  measurable_fun [set: \bar R] (poweR ^~ r).
+Proof.
+under eq_fun do rewrite poweRE.
+rewrite -/(measurable_fun _ _).
+apply: measurable_fun_ifT => //=.
+  apply/measurable_EFinP => //=.
+  apply: measurable_fun_ifT => //=.
+    apply: (measurable_fun_bool true).
+    rewrite setTI (_ : _ @^-1` _ = EFin @` setT).
+      by apply: measurable_image_EFin; exact: measurableT.
+    apply/seteqP; split => [x finx|x [s sx <-//]]/=.
+    by exists (fine x) => //; rewrite fineK.
+  exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)).
+apply: measurable_fun_ifT => //=; first exact: measurable_fun_eqe.
+apply: measurable_fun_ifT => //=; first exact: measurable_fun_eqe.
+apply/measurable_EFinP => //=.
+exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)).
+Qed.
 
 Section measurable_comparison.
 Context d (T : measurableType d) (R : realType).
@@ -644,7 +702,7 @@ Lemma measurable_fun_le D f g :
   measurable (D `&` [set x | f x <= g x]).
 Proof.
 move=> mD mf mg; under eq_set => x do rewrite -lee_fin.
-by apply: emeasurable_fun_le => //; exact: measurableT_comp.
+by apply: measurable_lee => //; exact: measurableT_comp.
 Qed.
 
 End measurable_comparison.