From 9bd8954c5c9e402a4756b62b640eb8ff51d22942 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 9 Oct 2026 14:11:14 +0900 Subject: [PATCH 1/2] measure induced by a measurable function Co-authored-by: Lionel Blatter --- CHANGELOG_UNRELEASED.md | 7 + .../lebesgue_Rintegral.v | 155 +++++++++++++++++- .../lebesgue_integral_monotone_convergence.v | 1 - .../lebesgue_integral_theory/radon_nikodym.v | 13 +- 4 files changed, 157 insertions(+), 19 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e8aa6722ff..7e781e59b2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -135,6 +135,10 @@ `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 `induced_measure` + + lemmas `integral_induced_measure_indic`, `sintegral_induced_measure`, + `integral_induced_measure` ### Changed @@ -206,6 +210,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`: + + lemma `semi_sigma_additive_nng_induced` + ### Renamed - in `sequences.v`: diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index f3b54deff4..3c18a2e352 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -15,17 +15,19 @@ 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)` *) +(* *) +(* `induced_measure mf f0` *) +(* : measure induced by `f : T -> R` *) +(* : `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 +194,145 @@ Qed. End Rintegral. +Section induced_charge. +Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). +Local Open Scope ereal_scope. + +Lemma semi_sigma_additive_nng_induced (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 induced_charge. + +Section induced_measure_def. +Import MeasurableR. +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}). + +Definition induced_measure (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 induced_measure_def. + +(* NB: this does not rely on the Lebesgue measure, just on the Borel sigma-algebra *) +Section induced_measure. +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' := (induced_measure 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_nng_induced => //; exact/measurable_EFinP. +Qed. + +HB.instance Definition _ := isMeasure.Build d T R m' + m'0 m'_ge0 m'_semi_sigma_additive. + +End induced_measure. + +Section integral_induced_measure. +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 _} := induced_measure mu mh h0. + +Lemma integral_induced_measure_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. + +Lemma integral_induced_measureMindic (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_induced_measure_indic. +Qed. + +Import HBNNSimple. + +Lemma sintegral_induced_measure (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_induced_measureMindic. +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_induced_measure (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_induced_measure. +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_induced_measure. + Section Rintegral_lebesgue_measure. Context {R : realType}. Notation mu := (@lebesgue_measure R). diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v index 236aafdd67..6943983650 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v +++ b/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. diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v index be00bf3721..a5fe0b0762 100644 --- a/theories/lebesgue_integral_theory/radon_nikodym.v +++ b/theories/lebesgue_integral_theory/radon_nikodym.v @@ -59,19 +59,10 @@ Definition induced_charge d (T : measurableType d) {R : realType} Notation induced := induced_charge (only parsing). Section induced_charge. -Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). +Context d (T : measurableType d) {R : realType} + (mu : {measure set T -> \bar R}) (f : T -> \bar R). Local Open Scope ereal_scope. -Lemma semi_sigma_additive_nng_induced (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. - -Variable f : T -> \bar R. Hypothesis intf : mu.-integrable setT f. Local Notation nu := (induced_charge intf). From ae5859943b7ecb6ae8c3b81060e60ddee3aa67c3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 16 Oct 2026 23:51:46 +0900 Subject: [PATCH 2/2] addressing comments --- CHANGELOG_UNRELEASED.md | 17 ++- .../lebesgue_Rintegral.v | 49 ++++---- .../lebesgue_integral_theory/radon_nikodym.v | 119 +++++++++--------- theories/lebesgue_stieltjes_measure.v | 4 +- .../bernoulli_distribution.v | 1 - .../probability_theory/beta_distribution.v | 1 - .../exponential_distribution.v | 10 +- .../probability_theory/normal_distribution.v | 46 +++---- .../probability_theory/poisson_distribution.v | 1 - .../probability_theory/uniform_distribution.v | 1 - 10 files changed, 118 insertions(+), 131 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7e781e59b2..5d156684cd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -136,9 +136,10 @@ `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 `induced_measure` - + lemmas `integral_induced_measure_indic`, `sintegral_induced_measure`, - `integral_induced_measure` + + definition `measure_of_density` + + lemmas `integral_measure_of_density_indic`, + `integral_measure_of_densityMindic`, `sintegral_measure_of_density`, + `integral_measure_of_density` ### Changed @@ -210,8 +211,8 @@ + 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`: - + lemma `semi_sigma_additive_nng_induced` +- moved to `lebesgue_Rintegral.v` from `radon_nikodym.v` and renamed: + + `semi_sigma_additive_nng_induced` -> `semi_sigma_additive_measure_of_density` ### Renamed @@ -228,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 @@ -293,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 diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 3c18a2e352..525b3cf35e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -21,8 +21,9 @@ From mathcomp Require Import lebesgue_integral_dominated_convergence. (* `Rintegral mu D f` *) (* : Definition for `fine (\int[mu]_(x in D) f x)` *) (* *) -(* `induced_measure mf f0` *) +(* `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 *) (* *) @@ -194,11 +195,11 @@ Qed. End Rintegral. -Section induced_charge. +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_nng_induced (f : T -> \bar R) : +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. @@ -207,47 +208,47 @@ move=> mf f0 /= F mF tF mUF; rewrite ge0_integral_bigcup//=. by apply: is_cvg_ereal_nneg_natsum_cond => // n _ _; exact: integral_ge0. Qed. -End induced_charge. +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 induced_measure_def. +Section measure_of_density_def. Import MeasurableR. Context {d} {T : measurableType d} {R : realType} (mu : {measure set T -> \bar R}). -Definition induced_measure (f : T -> R) - (mf : measurable_fun [set: T] f) +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 induced_measure_def. +End measure_of_density_def. (* NB: this does not rely on the Lebesgue measure, just on the Borel sigma-algebra *) -Section induced_measure. +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' := (induced_measure mu mf f0). +Local Notation m' := (measure_of_density mu mf f0). -Let m'0 : m' set0 = 0. -Proof. exact: integral_set0. Qed. +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_nng_induced => //; exact/measurable_EFinP. +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 induced_measure. +End measure_of_density. -Section integral_induced_measure. +Section integral_measure_of_density. Import MeasurableR. Local Open Scope ereal_scope. Context {d} {T : measurableType d} {R : realType} @@ -256,9 +257,9 @@ Context {d} {T : measurableType d} {R : realType} Hypothesis mh : measurable_fun [set: T] h. Hypothesis h0 : forall x, (0 <= h x)%R. -Let mu' : {measure set _ -> \bar _} := induced_measure mu mh h0. +Let mu' : {measure set _ -> \bar _} := measure_of_density mu mh h0. -Lemma integral_induced_measure_indic (A : set T) : measurable A -> +#[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 _. @@ -266,7 +267,7 @@ rewrite patchE indicE; case: ifP => _; first by rewrite mul1e. by rewrite mul0e. Qed. -Lemma integral_induced_measureMindic (r : R) (A : set T) : measurable A -> +#[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. @@ -275,18 +276,18 @@ 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_induced_measure_indic. +- by rewrite integral_measure_of_density_indic. Qed. Import HBNNSimple. -Lemma sintegral_induced_measure (g : {nnsfun T >-> R}) : +#[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_induced_measureMindic. + 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//=. @@ -302,7 +303,7 @@ rewrite -ge0_mule_fsuml; first by move=> _ [t _ <-]; rewrite lee_fin mulr_ge0. by rewrite fsumEFin// [in RHS](fimfunE g). Qed. -Lemma integral_induced_measure (f : T -> \bar R) : +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. @@ -318,7 +319,7 @@ transitivity (limn (fun n => \int[mu']_x gE n x)). 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_induced_measure. + 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. @@ -331,7 +332,7 @@ apply: cvg_lim => //; apply: cvgeZr => //. exact: cvg_nnsfun_approx. Qed. -End integral_induced_measure. +End integral_measure_of_density. Section Rintegral_lebesgue_measure. Context {R : realType}. diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v index a5fe0b0762..10c4f2139f 100644 --- a/theories/lebesgue_integral_theory/radon_nikodym.v +++ b/theories/lebesgue_integral_theory/radon_nikodym.v @@ -22,14 +22,14 @@ From mathcomp Require Import lebesgue_integral_definition lebesgue_integrable (* Stieltjes measure in Coq. Computer Software 41(2) 2024 *) (* *) (* ## Theory *) -(* ``` *) -(* induced_charge intf == charge induced by a function f : T -> \bar R *) -(* R has type realType; T is a measurableType. *) -(* intf is a proof that f is integrable over *) -(* [set: T] *) -(* 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu *) -(* (the scope is charge_scope) *) -(* ``` *) +(* *) +(* `charge_of_density intf` *) +(* : charge induced by a function `f : T -> \bar R` *) +(* : `R` has type `realType`; `T` is a `measurableType`. *) +(* : `intf` is a proof that f is integrable over [set: T] *) +(* *) +(* `'d nu '/d mu` *) +(* : Radon-Nikodym derivative of `nu` w.r.t. `mu` (the scope is charge_scope) *) (* *) (******************************************************************************) @@ -38,7 +38,6 @@ Reserved Notation "'d nu '/d mu" (mu at level 0, Declare Scope charge_scope. -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -50,22 +49,22 @@ Local Open Scope ring_scope. Local Open Scope classical_set_scope. Local Open Scope ereal_scope. -Definition induced_charge d (T : measurableType d) {R : realType} +Definition charge_of_density d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}) (f : T -> \bar R) (intf : mu.-integrable [set: T] f) := fun A => (\int[mu]_(t in A) f t)%E. -#[deprecated(since="mathcomp-analysis 1.15.0", note="renamed to `induced_charge`")] -Notation induced := induced_charge (only parsing). +#[deprecated(since="mathcomp-analysis 1.19.0", use=charge_of_density)] +Notation induced_charge := charge_of_density (only parsing). -Section induced_charge. +Section charge_of_density. Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}) (f : T -> \bar R). Local Open Scope ereal_scope. Hypothesis intf : mu.-integrable setT f. -Local Notation nu := (induced_charge intf). +Local Notation nu := (charge_of_density intf). Let nu0 : nu set0 = 0. Proof. by rewrite /nu integral_set0. Qed. @@ -87,30 +86,30 @@ rewrite (_ : SF = fun n => rewrite /nu integralE; apply: cvgeD. - rewrite fin_num_adde_defr// integrable_fin_num//=. by apply: integrable_funepos => //=; exact: integrableS intf. -- apply/semi_sigma_additive_nng_induced => //. +- apply/semi_sigma_additive_measure_of_density => //. by apply: measurable_funepos; exact: (measurable_int mu). -- apply/cvgeN/semi_sigma_additive_nng_induced => //=. +- apply/cvgeN/semi_sigma_additive_measure_of_density => //=. by apply: measurable_funeneg; exact: (measurable_int mu). Qed. HB.instance Definition _ := isCharge.Build _ _ _ nu nu0 finnu snu. -End induced_charge. +End charge_of_density. -Section dominates_induced. -Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}). +Section dominates_charge_of_density. +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}) (f : T -> \bar R). Local Open Scope ereal_scope. -Variable f : T -> \bar R. Hypothesis intf : mu.-integrable setT f. Let intnf : mu.-integrable [set: T] (abse \o f). Proof. exact: integrable_abse. Qed. -Lemma dominates_induced : induced_charge intnf `<< mu. +Lemma dominates_charge_of_density : charge_of_density intnf `<< mu. Proof. apply/null_content_dominatesP => /= A mA muA. -rewrite /induced_charge; apply/eqP; rewrite -abse_eq0 eq_le abse_ge0 andbT. +apply/eqP; rewrite -abse_eq0 eq_le abse_ge0 andbT. rewrite (le_trans (le_abse_integral _ _ _))//=. by case/integrableP : intnf => /= + _; exact: measurable_funTS. rewrite le_eqVlt; apply/orP; left; apply/eqP. @@ -119,12 +118,14 @@ apply: null_set_integral => //=. by apply: measurable_funTS; apply: measurable_int intnf. Qed. -End dominates_induced. +End dominates_charge_of_density. +#[deprecated(since="mathcomp-analysis 1.19.0", use=dominates_charge_of_density)] +Notation dominates_induced := dominates_charge_of_density (only parsing). Section integral_normr_continuous. Local Open Scope ereal_scope. -Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}) - (f : T -> R). +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}) (f : T -> R). Hypothesis intf : mu.-integrable setT (EFin \o f). Let intnf : mu.-integrable setT (abse \o EFin \o f). @@ -136,8 +137,9 @@ Lemma integral_normr_continuous (e : R) : (0 < e)%R -> exists d : R, (0 < d)%R /\ forall A, measurable A -> mu A < d%:E -> (\int[mu]_(x in A) `|f x| < e)%R. Proof. -move=> e0; have [P [N pn]] := Hahn_decomposition (induced_charge intnf). -have [r [r0 re]] := charge_variation_continuous pn (dominates_induced intf) e0. +move=> e0; have [P [N pn]] := Hahn_decomposition (charge_of_density intnf). +have [r [r0 re]] := + charge_variation_continuous pn (dominates_charge_of_density intf) e0. exists r; split => //= A mA Ad. have {re} := re _ mA Ad. rewrite -lte_fin; apply: le_lt_trans. @@ -161,8 +163,8 @@ End integral_normr_continuous. for an overview. *) Module approxRN. Section approxRN. -Context d (T : measurableType d) (R : realType). -Variables mu nu : {measure set T -> \bar R}. +Context d (T : measurableType d) (R : realType) + (mu nu : {measure set T -> \bar R}). Definition approxRN := [set g : T -> \bar R | [/\ forall x, 0 <= g x, mu.-integrable [set: T] g & @@ -190,9 +192,8 @@ End approxRN. Module approxRN_seq. Section approxRN_seq. -Context d (T : measurableType d) (R : realType). -Variable mu : {measure set T -> \bar R}. -Variable nu : {finite_measure set T -> \bar R}. +Context {d} {T : measurableType d} {R : realType} + (mu : {measure set T -> \bar R}) (nu : {finite_measure set T -> \bar R}). Import approxRN. @@ -351,8 +352,8 @@ End approxRN_seq. Module lim_max_approxRN_seq. Section lim_max_approxRN_seq. -Context d (T : measurableType d) (R : realType). -Variables mu nu : {finite_measure set T -> \bar R}. +Context {d} {T : measurableType d} {R : realType} + (mu nu : {finite_measure set T -> \bar R}). Import approxRN. @@ -588,8 +589,8 @@ End lim_max_approxRN_seq. End lim_max_approxRN_seq. Section radon_nikodym_finite. -Context d (T : measurableType d) (R : realType). -Variables mu nu : {finite_measure set T -> \bar R}. +Context {d} {T : measurableType d} {R : realType} + (mu nu : {finite_measure set T -> \bar R}). Import approxRN. @@ -599,8 +600,8 @@ Let M := sup_int_approxRN mu nu. Import lim_max_approxRN_seq. Let f := fRN mu nu. -Let mf := measurable_fun_fRN. -Let f_ge0 := fRN_ge0. +Let mf := measurable_fun_fRN mu nu. +Let f_ge0 := fRN_ge0 mu nu. Lemma radon_nikodym_finite : nu `<< mu -> exists f : T -> \bar R, [/\ forall x, f x >= 0, mu.-integrable [set: T] f & @@ -620,10 +621,10 @@ have muAP_gt0 : 0 < mu AP. move/null_content_dominatesP in nu_mu. apply/eqP/(contra_not (nu_mu _ mAP))/eqP; rewrite gt_eqF//. rewrite (@lt_le_trans _ _ (sigma AP))//. - rewrite (@lt_le_trans _ _ (sigma A))//; last first. - rewrite (charge_partition _ _ mP mN)// geeDl//. - by apply: negN => //; exact: measurableI. - by rewrite sube_gt0// (proj2_sig (epsRN_ex mA abs)). + rewrite (@lt_le_trans _ _ (sigma A))//. + by rewrite sube_gt0// (proj2_sig (epsRN_ex mA abs)). + rewrite (charge_partition _ _ mP mN)// geeDl//. + by apply: negN => //; exact: measurableI. rewrite /sigma/= /sigmaRN lee_subel_addl ?fin_num_measure//. by rewrite lee_paddl// integral_ge0// => x _; rewrite adde_ge0//; exact: f_ge0. pose h x := if x \in AP then f x + (epsRN mA abs)%:num%:E else f x. @@ -667,11 +668,9 @@ have int_h_M : \int[mu]_x h x > M. under [X in _ < _ + X]eq_integral. by move=> x; rewrite inE /= => xE0p; rewrite memNset//; over. rewrite ge0_integralD//. - - by move=> x _; exact: f_ge0. - by apply: measurable_funTS; exact: mf. rewrite integral_cst // addeAC -ge0_integral_setU//. by rewrite setUv//; exact: mf. - by move=> x _; exact: f_ge0. rewrite setUv int_fRNE -lte_subel_addl. rewrite ge0_fin_numE ?sup_int_approxRN_lty. exact: sup_int_approxRN_ge0. @@ -691,9 +690,9 @@ Qed. End radon_nikodym_finite. Section radon_nikodym_sigma_finite. -Context d (T : measurableType d) (R : realType). -Variables (mu : {sigma_finite_measure set T -> \bar R}) - (nu : {finite_measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {finite_measure set T -> \bar R}). Lemma radon_nikodym_sigma_finite : nu `<< mu -> exists f : T -> \bar R, [/\ forall x, f x >= 0, forall x, f x \is a fin_num, @@ -807,9 +806,9 @@ End radon_nikodym_sigma_finite. Module Radon_Nikodym_SigmaFinite. Section radon_nikodym_sigma_finite_def. -Context d (T : measurableType d) (R : realType). -Variables (nu : {finite_measure set T -> \bar R}) - (mu : {sigma_finite_measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (nu : {finite_measure set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). Definition f : T -> \bar R := match pselect (nu `<< mu) with @@ -923,10 +922,10 @@ Qed. End integrableM. Section chain_rule. -Context d (T : measurableType d) (R : realType). -Variables (nu : {finite_measure set T -> \bar R}) - (la : {sigma_finite_measure set T -> \bar R}) - (mu : {finite_measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (nu : {finite_measure set T -> \bar R}) + (la : {sigma_finite_measure set T -> \bar R}) + (mu : {finite_measure set T -> \bar R}). Local Notation "'d nu '/d mu" := (f nu mu). @@ -951,9 +950,9 @@ End chain_rule. End Radon_Nikodym_SigmaFinite. Section radon_nikodym. -Context d (T : measurableType d) (R : realType). -Variables (nu : {charge set T -> \bar R}) - (mu : {sigma_finite_measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (nu : {charge set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). Local Lemma Radon_Nikodym0 : nu `<< mu -> exists f : T -> \bar R, [/\ (forall x, f x \is a fin_num), @@ -1010,9 +1009,9 @@ Local Open Scope charge_scope. solve [apply: measurable_int; exact: Radon_Nikodym_integrable] : core. Section Radon_Nikodym_charge_of_finite_measure. -Context d (T : measurableType d) (R : realType). -Variables (nu : {finite_measure set T -> \bar R}) - (mu : {sigma_finite_measure set T -> \bar R}). +Context {d} {T : measurableType d} {R : realType} + (nu : {finite_measure set T -> \bar R}) + (mu : {sigma_finite_measure set T -> \bar R}). Hypothesis numu : nu `<< mu. Implicit Types f : T -> \bar R. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 1652724365..59b6d673b8 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -989,7 +989,7 @@ HB.instance Definition _ (f : cumulative R R) := End completed_lebesgue_stieltjes_measure. Arguments completed_lebesgue_stieltjes_measure {R}. -Section probability_measure_of_lebesgue_stieltjes_mesure. +Section probability_measure_of_lebesgue_stieltjes_measure. Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. @@ -1019,4 +1019,4 @@ Unshelve. all: end_near. Qed. HB.instance Definition _ := @Measure_isProbability.Build _ _ _ (lebesgue_stieltjes_measure f) lebesgue_stieltjes_setT. -End probability_measure_of_lebesgue_stieltjes_mesure. +End probability_measure_of_lebesgue_stieltjes_measure. diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v index 267d1739a7..b25975d8eb 100644 --- a/theories/probability_theory/bernoulli_distribution.v +++ b/theories/probability_theory/bernoulli_distribution.v @@ -20,7 +20,6 @@ From mathcomp Require Import lebesgue_integral kernel. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v index 7e7fc15dbb..ac0b7b5fae 100644 --- a/theories/probability_theory/beta_distribution.v +++ b/theories/probability_theory/beta_distribution.v @@ -28,7 +28,6 @@ From mathcomp Require Import uniform_distribution bernoulli_distribution. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/probability_theory/exponential_distribution.v b/theories/probability_theory/exponential_distribution.v index 04b76ff3fd..6e113d161d 100644 --- a/theories/probability_theory/exponential_distribution.v +++ b/theories/probability_theory/exponential_distribution.v @@ -10,14 +10,14 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral ftc. (**md**************************************************************************) (* # Exponential distribution *) (* *) -(* ``` *) -(* exponential_pdf r == pdf of the exponential distribution with rate r *) -(* exponential_prob r == exponential probability measure *) -(* ``` *) +(* `exponential_pdf r` *) +(* : pdf of the exponential distribution with rate r *) +(* *) +(* `exponential_prob r` *) +(* : exponential probability measure *) (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index 5940afa83d..b373a0eed2 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -32,7 +32,6 @@ From mathcomp Require Import lebesgue_integral ftc gauss_integral. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -213,13 +212,16 @@ Section normal_prob_def. Import MeasurableR. Context {R : realType}. -Definition normal_prob (m : R) (s : R) : set _ -> \bar R := - fun V => (\int[lebesgue_measure]_(x in V) (normal_pdf m s x)%:E)%E. +Definition normal_prob (m : R) (s : R) := + measure_of_density lebesgue_measure (measurable_normal_pdf m s) + (normal_pdf_ge0 m s). + +HB.instance Definition _ m s := Measure.on (normal_prob m s). End normal_prob_def. Section normal_probability. -Variables (R : realType) (m sigma : R). +Context {R : realType} (m sigma : R). Local Open Scope ring_scope. Notation mu := lebesgue_measure. @@ -305,39 +307,21 @@ apply/abse_integralP => //=; last by rewrite integral_normal_pdf abse1 ltry. by apply/measurable_EFinP; exact: measurable_normal_pdf. Qed. -Local Notation normal_pdf := (normal_pdf m sigma). -Local Notation normal_prob := (normal_prob m sigma). - -Let normal0 : normal_prob set0 = 0%E. -Proof. by rewrite /normal_prob integral_set0. Qed. - -Let normal_ge0 A : (0 <= normal_prob A)%E. -Proof. -rewrite /normal_prob integral_ge0//= => x _. -by rewrite lee_fin normal_pdf_ge0 ?ltW. -Qed. +#[local] Notation normal_pdf := (normal_pdf m sigma). +#[local] Notation normal_prob := (normal_prob m sigma). -Let normal_sigma_additive : semi_sigma_additive normal_prob. +Let normal_setT : normal_prob [set: _] = 1%E. Proof. -move=> /= A mA tA mUA. -rewrite /normal_prob/= integral_bigcup//=. - by apply: (integrableS _ _ (subsetT _)) => //; exact: integrable_normal_pdf. -apply: is_cvg_ereal_nneg_natsum_cond => n _ _. -by apply: integral_ge0 => /= x ?; rewrite lee_fin normal_pdf_ge0 ?ltW. +by rewrite /normal_prob/= /measure_of_density/= integral_normal_pdf. Qed. -HB.instance Definition _ := isMeasure.Build _ _ _ - normal_prob normal0 normal_ge0 normal_sigma_additive. - -Let normal_setT : normal_prob [set: _] = 1%E. -Proof. by rewrite /normal_prob integral_normal_pdf. Qed. - HB.instance Definition _ := @Measure_isProbability.Build _ _ R normal_prob normal_setT. Lemma normal_prob_dominates : normal_prob `<< mu. Proof. -apply/null_content_dominatesP=> A mA muA0; rewrite /normal_prob /normal_pdf. +apply/null_content_dominatesP=> A mA muA0. +rewrite /normal_prob /normal_pdf /measure_of_density. have [s0|s0] := eqVneq sigma 0. apply: null_set_integral => //=; apply: measurable_funTS => /=. exact/measurable_EFinP/measurable_indic. @@ -389,9 +373,8 @@ Section normal_prob_continuous. So the integral of `g` on ]-oo, +oo[ is the integral of `f` on ]-oo, +oo[ added by the integral of `normal_pdf a s x` on ]a - e, a + e[ *) -Context {R : realType}. +Context {R : realType} (s : R). Notation mu := (@lebesgue_measure R). -Variable s : R. Hypothesis s0 : s != 0. Implicit Types a e x : R. @@ -631,7 +614,8 @@ Lemma measurable_normal_prob (s : R) U : measurable U -> measurable_fun setT (fun x => normal_prob x s U). Proof. have [->/=|s0 mU] := eqVneq s 0%R. - by rewrite /normal_prob /normal_pdf eqxx => _; exact: measurable_cst. + rewrite /normal_prob /normal_pdf /measure_of_density eqxx => _. + exact: measurable_cst. under [X in _ _ X]eq_fun. move=> /= x. rewrite -(@fineK _ (_ x _ _)). diff --git a/theories/probability_theory/poisson_distribution.v b/theories/probability_theory/poisson_distribution.v index a8502dc30b..31fce96182 100644 --- a/theories/probability_theory/poisson_distribution.v +++ b/theories/probability_theory/poisson_distribution.v @@ -17,7 +17,6 @@ From mathcomp Require Import lebesgue_integral. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v index 7c8d61abbb..f9eeb6c5d9 100644 --- a/theories/probability_theory/uniform_distribution.v +++ b/theories/probability_theory/uniform_distribution.v @@ -18,7 +18,6 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive.