measure induced by a measurable function

CHANGELOG_UNRELEASED.md

@@ -135,6 +135,11 @@
     `lhopital_Ninfty`, `lhopital_pinfty`, `lhopital_ninfty`,
     `lhopital_Ninfty_at_pinfty`, `lhopital_pinfty_at_pinfty`, `lhopital_ninfty_at_pinfty`,
     `lhopital_Ninfty_at_ninfty`, `lhopital_pinfty_at_ninfty`, `lhopital_ninfty_at_ninfty`
+- in `lebesgue_Rintegral.v`:
+  + definition `measure_of_density`
+  + lemmas `integral_measure_of_density_indic`,
+    `integral_measure_of_densityMindic`, `sintegral_measure_of_density`,
+    `integral_measure_of_density`
 
 ### Changed
 
@@ -206,6 +211,9 @@
   + lemmas `cvg_at_right_filter`,
     `cvg_at_left_filter`, `cvg_at_right_within`, `cvg_at_left_within`
 
+- moved to `lebesgue_Rintegral.v` from `radon_nikodym.v` and renamed:
+  + `semi_sigma_additive_nng_induced` -> `semi_sigma_additive_measure_of_density`
+
 ### Renamed
 
 - in `sequences.v`:
@@ -221,6 +229,9 @@
 
 - in `pseudometric_normed_Zmodule.v`:
   + `continuous_within_itvP` -> `continuous_within_itvccP`
+- in `radon_nikodym.v`:
+  + `induced_charge` -> `charge_of_density`
+  + `dominates_induced` -> `dominates_charge_of_density`
 
 ### Generalized
 
@@ -286,6 +297,9 @@
 - in `pseudometric_normred_Zmodule.v`:
   + lemma `pseudoMetricNormedZModType_hausdorff` (deprecated since 1.10.0)
 
+- in `radon_nikodym.v`:
+  + notation `induced` (deprecated since 1.15.0)
+
 ### Infrastructure
 
 ### Misc

theories/lebesgue_integral_theory/lebesgue_Rintegral.v

@@ -15,17 +15,20 @@ From mathcomp Require Import lebesgue_integral_dominated_convergence.
 (**md**************************************************************************)
 (* # The Lebesgue Integral for real-valued functions                          *)
 (*                                                                            *)
-(* Detailed contents:                                                         *)
-(* ```                                                                        *)
-(*       Rintegral mu D f := fine (\int[mu]_(x in D) f x).                    *)
-(* ```                                                                        *)
-(*                                                                            *)
 (* This file recasts lemmas about `integral` to `Rintegral`. It also          *)
-(* established that Continuous functions are dense in $L^1$.                  *)
+(* establishes that continuous functions are dense in $L^1$.                  *)
+(*                                                                            *)
+(* `Rintegral mu D f`                                                         *)
+(* : Definition for `fine (\int[mu]_(x in D) f x)`                            *)
+(*                                                                            *)
+(* `measure_of_density mf f0`                                                 *)
+(* : measure induced by `f : T -> R`                                          *)
+(* : `f` is called the density of the induced measure                         *)
+(* : `mf` is a proof that `f` is measurable and `f0`, a proof that it is      *)
+(* : non-negative                                                             *)
 (*                                                                            *)
 (******************************************************************************)
 
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -192,6 +195,145 @@ Qed.
 
 End Rintegral.
 
+Section semi_sigma_additive_measure_of_density.
+Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}).
+Local Open Scope ereal_scope.
+
+Lemma semi_sigma_additive_measure_of_density (f : T -> \bar R) :
+  measurable_fun setT f -> (forall x, 0 <= f x) ->
+  semi_sigma_additive (fun A => \int[mu]_(t in A) f t).
+Proof.
+move=> mf f0 /= F mF tF mUF; rewrite ge0_integral_bigcup//=.
+  exact: measurable_funTS.
+by apply: is_cvg_ereal_nneg_natsum_cond => // n _ _; exact: integral_ge0.
+Qed.
+
+End semi_sigma_additive_measure_of_density.
+#[deprecated(since="mathcomp-analysis 1.19.0", use=semi_sigma_additive_measure_of_density)]
+Notation semi_sigma_additive_nng_induced := semi_sigma_additive_measure_of_density (only parsing).
+
+Section measure_of_density_def.
+Import MeasurableR.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}).
+
+Definition measure_of_density (f : T -> R) (mf : measurable_fun [set: T] f)
+    (f0 : forall x, 0 <= f x) :=
+  fun A => (\int[mu]_(t in A) (f t)%:E)%E.
+
+End measure_of_density_def.
+
+(* NB: this does not rely on the Lebesgue measure, just on the Borel sigma-algebra *)
+Section measure_of_density.
+Import MeasurableR.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (f : T -> R).
+
+Hypotheses (mf : measurable_fun [set: T] f) (f0 : forall x, (0 <= f x)%R).
+
+Local Notation m' := (measure_of_density mu mf f0).
+
+Let m'0 : m' set0 = 0. Proof. exact: integral_set0. Qed.
+
+Let m'_ge0 A : (0 <= m' A)%E.
+Proof. by apply: integral_ge0 => t At; rewrite lee_fin. Qed.
+
+Let m'_semi_sigma_additive : semi_sigma_additive m'.
+Proof.
+by apply: semi_sigma_additive_measure_of_density => //; exact/measurable_EFinP.
+Qed.
+
+HB.instance Definition _ := isMeasure.Build d T R m'
+  m'0 m'_ge0 m'_semi_sigma_additive.
+
+End measure_of_density.
+
+Section integral_measure_of_density.
+Import MeasurableR.
+Local Open Scope ereal_scope.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (h : T -> R).
+
+Hypothesis mh : measurable_fun [set: T] h.
+Hypothesis h0 : forall x, (0 <= h x)%R.
+
+Let mu' : {measure set _ -> \bar _} := measure_of_density mu mh h0.
+
+#[local] Lemma integral_measure_of_density_indic (A : set T) : measurable A ->
+  \int[mu]_x ((\1_A x)%:E * (h x)%:E) = mu' A.
+Proof.
+move=> mA; rewrite [RHS]integral_mkcond; apply: eq_integral => x _.
+rewrite patchE indicE; case: ifP => _; first by rewrite mul1e.
+by rewrite mul0e.
+Qed.
+
+#[local] Lemma integral_measure_of_densityMindic (r : R) (A : set T) : measurable A ->
+  (0 <= r)%R ->
+  \int[mu]_x (r%:E * (\1_A x)%:E * (h x)%:E) = r%:E * mu' A.
+Proof.
+move=> mA r0.
+under eq_integral do rewrite -muleA.
+rewrite ge0_integralZl//=.
+- apply: emeasurable_funM => //; by apply /measurable_EFinP.
+- by move=> x _; apply: mule_ge0; rewrite ?lee_fin.
+- by rewrite integral_measure_of_density_indic.
+Qed.
+
+Import HBNNSimple.
+
+#[local] Lemma sintegral_measure_of_density (g : {nnsfun T >-> R}) :
+  sintegral mu' g = \int[mu]_x ((g x)%:E * (h x)%:E).
+Proof.
+transitivity (\sum_(r \in range g)
+    \int[mu]_x (r%:E * (\1_(g @^-1` [set r]) x)%:E * (h x)%:E)).
+  rewrite sintegralE; apply: eq_fsbigr => r /set_mem[x0 _ <-].
+  by rewrite integral_measure_of_densityMindic.
+transitivity (\int[mu]_x (\sum_(r \in range g)
+    ((r * (\1_(g @^-1` [set r]) x))%:E * (h x)%:E))).
+  rewrite ge0_integral_fsum//=.
+  - move=> r.
+    under eq_fun do rewrite EFinM -muleA.
+    apply: measurable_funeM.
+    by apply: emeasurable_funM => //; exact/measurable_EFinP.
+  - move=> r x _; have [r0|r0] := leP 0%R r.
+      by rewrite mule_ge0// lee_fin// mulr_ge0.
+    by rewrite preimage_nnfun0// indic0/= mulr0 mul0e.
+apply: eq_integral => x _.
+rewrite -ge0_mule_fsuml; first by move=> _ [t _ <-]; rewrite lee_fin mulr_ge0.
+by rewrite fsumEFin// [in RHS](fimfunE g).
+Qed.
+
+Lemma integral_measure_of_density (f : T -> \bar R) :
+    measurable_fun [set: T] f -> (forall x, 0 <= f x) ->
+  \int[mu']_x f x = \int[mu]_x (f x * (h x)%:E).
+Proof.
+move=> mf f0.
+pose g := nnsfun_approx measurableT mf.
+pose gE := fun n => EFin \o g n.
+have mgE n : measurable_fun [set: T] (EFin \o g n) by exact/measurable_EFinP.
+have gE_ge0 n x : 0 <= gE n x by rewrite lee_fin.
+have nd_gE x : {homo gE ^~ x : n p / (n <= p)%O >-> n <= p}.
+  by move=> *; exact/lefP/nd_nnsfun_approx.
+transitivity (limn (fun n => \int[mu']_x gE n x)).
+  rewrite -monotone_convergence//; apply: eq_integral => t _.
+  by apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
+transitivity (limn (fun n => \int[mu]_x (gE n x * (h x)%:E))).
+  apply: congr_lim; apply/funext => n.
+  by rewrite integralT_nnsfun sintegral_measure_of_density.
+have mgEh n : measurable_fun [set: T] (fun x => gE n x * (h x)%:E).
+  by apply: emeasurable_funM => //; exact/measurable_EFinP.
+have gEh_ge0 n x : 0 <= gE n x * (h x)%:E by rewrite mule_ge0// lee_fin.
+have nd_gEh x :
+    {homo (fun n => gE n x * (h x)%:E) : n p / (n <= p)%O >-> n <= p}.
+  by move=> p q pq; rewrite lee_wpmul2r ?lee_fin//; exact: nd_gE.
+rewrite -monotone_convergence//.
+apply: eq_integral => x _.
+apply: cvg_lim => //; apply: cvgeZr => //.
+exact: cvg_nnsfun_approx.
+Qed.
+
+End integral_measure_of_density.
+
 Section Rintegral_lebesgue_measure.
 Context {R : realType}.
 Notation mu := (@lebesgue_measure R).

theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v

@@ -18,7 +18,6 @@ From mathcomp Require Import lebesgue_integral_definition.
 (*                                                                            *)
 (******************************************************************************)
 
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.