diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 78d0bf711e..22c6c1b140 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -66,6 +66,25 @@ + generalized and renamed: * `measurable_fun_itv_bndo_bndc` -> `measurable_fun_itv_bndo_bndcP` * `measurable_fun_itv_obnd_cbnd` -> `measurable_fun_itv_obnd_cbndP` +- moved from `simple_functions.v` to `measure.v` + + notations `{mfun _ >-> _}`, `[mfun of _]` + + mixin `isMeasurableFun`, structure `MesurableFun`, lemmas `measurable_funP` + + definitions `mfun`, `mfun_key`, canonical `mfun_keyed` + + definitions `mfun_Sub_subproof`, `mfun_Sub` + + lemmas `mfun_rect`, `mfun_valP`, `mfuneqP` + + lemma `measurableT_comp_subproof` + +- moved from `simple_functions.v` to `measure.v` and renamed: + + lemma `measurable_sfunP` -> `measurable_funPTI` + +- moved from `simple_functions.v` to `measurable_realfun.v` + + lemmas `mfun_subring_closed`, `mfun0`, `mfun1`, `mfunN`, + `mfunD`, `mfunB`, `mfunM`, `mfunMn`, `mfun_sum`, `mfun_prod`, `mfunX` + + definitions `mindic`, `indic_mfun`, `scale_mfun`, `max_mfun` + + lemmas `mindicE`, `max_mfun_subproof` + +- moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v` and renamed: + + lemma `measurable_sfun_inP` -> `measurable_funP1` ### Renamed @@ -80,6 +99,12 @@ - in `derive.v`: + `derivemxE` -> `deriveEjacobian` +- `measurable_sfunP` -> `measurable_funPTI` + (and moved from from `simple_functions.v` to `measure.v`) + +- `measurable_sfun_inP` -> `measurable_funP1` + (and moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v`) + ### Generalized - in `functions.v` @@ -91,6 +116,10 @@ - file `forms.v` (superseded by MathComp's `sesquilinear.v`) +- in `simple_functions.v`: + + duplicated hints about `measurable_set1` + + lemma `measurableT_comp_subproof` turned into a `Let` (now in `measure.v`) + ### Infrastructure ### Misc diff --git a/theories/charge.v b/theories/charge.v index 32fd4a16ba..60814b1af8 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat. diff --git a/theories/kernel.v b/theories/kernel.v index 4d16d61f47..957028bcf7 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1189,18 +1189,14 @@ 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/measurable_EFinP/measurableT_comp => [//|]. - have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). + - by move=> r; exact/measurable_EFinP/measurableT_comp. - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under [in RHS]eq_integral. move=> y _. under eq_integral. by move=> z _; rewrite fimfunE -fsumEFin//; over. rewrite /= ge0_integral_fsum//; last 2 first. - - 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; exact/measurable_EFinP/measurableT_comp. - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under eq_fsbigr. move=> r _. @@ -1218,15 +1214,14 @@ rewrite /= ge0_integral_fsum//; last 2 first. apply: eq_fsbigr => r _. rewrite (integralZl_indic _ (fun r => f @^-1` [set r]))//; last first. exact: preimage_nnfun0. -rewrite /= integral_kcomp_indic; last exact/measurable_sfunP. +rewrite /= integral_kcomp_indic//. have [r0|r0] := leP 0%R r. - rewrite ge0_integralZl//; last first. - exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _. - by under eq_integral do rewrite integral_indic// setIT. -rewrite integral0_eq ?mule0; last first. - move=> y _; rewrite integral0_eq// => z _. - by rewrite preimage_nnfun0// indic0. -by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0. + rewrite ge0_integralZl//. + by under eq_integral do rewrite integral_indic// setIT. + exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _. +rewrite integral0_eq ?mule0. + by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0. +by move=> y _; rewrite integral0_eq// => z _; rewrite preimage_nnfun0// indic0. Qed. (* [Lemma 3, Staton 2017 ESOP] (4/4) *) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index ce39a63106..b773c0c998 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -248,7 +248,7 @@ rewrite /fleg [X in _ X](_ : _ = \big[setU/set0]_(y <- fset_set (range f)) \big[setU/set0]_(x <- fset_set (range (g n)) | c * y <= x) (f @^-1` [set y] `&` (g n @^-1` [set x]))). apply: bigsetU_measurable => r _; apply: bigsetU_measurable => r' crr'. - exact/measurableI/measurable_sfunP. + exact/measurableI. rewrite predeqE => t; split => [/= cfgn|]. - rewrite -bigcup_seq; exists (f t); first by rewrite /= in_fset_set//= mem_set. rewrite -bigcup_seq_cond; exists (g n t) => //=. diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 08d726dbaf..4aaae44560 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -29,15 +29,8 @@ From mathcomp Require Import function_spaces. (* *) (* Detailed contents: *) (* ```` *) -(* {mfun aT >-> rT} == type of measurable functions *) -(* aT and rT are sigmaRingType's. *) (* {sfun T >-> R} == type of simple functions *) -(* f \in mfun == holds for f : {mfun _ >-> _} *) (* {nnsfun T >-> R} == type of non-negative simple functions *) -(* mindic mD := \1_D where mD is a proof that D is measurable *) -(* indic_mfun mD := mindic mD *) -(* scale_mfun k f := k \o* f *) -(* max_mfun f g := f \max g *) (* indic_sfun mD := mindic _ mD *) (* cst_sfun r == constant simple function *) (* max_sfun f g := f \max f *) @@ -55,10 +48,6 @@ From mathcomp Require Import function_spaces. (* *) (******************************************************************************) -Reserved Notation "{ 'mfun' aT >-> T }" - (at level 0, format "{ 'mfun' aT >-> T }"). -Reserved Notation "[ 'mfun' 'of' f ]" - (at level 0, format "[ 'mfun' 'of' f ]"). Reserved Notation "{ 'nnfun' aT >-> T }" (at level 0, format "{ 'nnfun' aT >-> T }"). Reserved Notation "[ 'nnfun' 'of' f ]" @@ -81,31 +70,6 @@ Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. - -HB.mixin Record isMeasurableFun d d' (aT : sigmaRingType d) (rT : sigmaRingType d') - (f : aT -> rT) := { - measurable_funPT : measurable_fun [set: aT] f -}. -HB.structure Definition MeasurableFun d d' aT rT := - {f of @isMeasurableFun d d' aT rT f}. -Arguments measurable_funPT {d d' aT rT} s. - -Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ _ aT T) : form_scope. -Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope. -#[global] Hint Extern 0 (measurable_fun [set: _] _) => - solve [apply: measurable_funPT] : core. - -Lemma measurable_funP {d d' : measure_display} - {aT : measurableType d} {rT : sigmaRingType d'} - (D : set aT) (s : {mfun aT >-> rT}) : measurable_fun D s. -Proof. -move=> mD Y mY; apply: measurableI => //. -by rewrite -(setTI (_ @^-1` _)); exact: measurable_funPT. -Qed. -Arguments measurable_funP {d d' aT rT D} s. - Module HBSimple. HB.structure Definition SimpleFun d (aT : sigmaRingType d) (rT : realType) := @@ -116,10 +80,6 @@ End HBSimple. Notation "{ 'sfun' aT >-> T }" := (@HBSimple.SimpleFun.type _ aT T) : form_scope. Notation "[ 'sfun' 'of' f ]" := [the {sfun _ >-> _} of f] : form_scope. -Lemma measurable_sfunP {d d'} {aT : measurableType d} {rT : measurableType d'} - (f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y). -Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. - Module HBNNSimple. Import HBSimple. @@ -132,137 +92,6 @@ End HBNNSimple. Notation "{ 'nnsfun' aT >-> T }" := (@HBNNSimple.NonNegSimpleFun.type _ aT%type T) : form_scope. Notation "[ 'nnsfun' 'of' f ]" := [the {nnsfun _ >-> _} of f] : form_scope. -Section mfun_pred. -Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. -Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f]. -Definition mfun_key : pred_key mfun. Proof. exact. Qed. -Canonical mfun_keyed := KeyedPred mfun_key. -End mfun_pred. - -Section mfun. -Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. -Notation T := {mfun aT >-> rT}. -Notation mfun := (@mfun _ _ aT rT). - -Section Sub. -Context (f : aT -> rT) (fP : f \in mfun). -Definition mfun_Sub_subproof := @isMeasurableFun.Build d _ aT rT f (set_mem fP). -#[local] HB.instance Definition _ := mfun_Sub_subproof. -Definition mfun_Sub := [mfun of f]. -End Sub. - -Lemma mfun_rect (K : T -> Type) : - (forall f (Pf : f \in mfun), K (mfun_Sub Pf)) -> forall u : T, K u. -Proof. -move=> Ksub [f [[Pf]]]/=. -by suff -> : Pf = (set_mem (@mem_set _ [set f | _] f Pf)) by apply: Ksub. -Qed. - -Lemma mfun_valP f (Pf : f \in mfun) : mfun_Sub Pf = f :> (_ -> _). -Proof. by []. Qed. - -HB.instance Definition _ := isSub.Build _ _ T mfun_rect mfun_valP. - -Lemma mfuneqP (f g : {mfun aT >-> rT}) : f = g <-> f =1 g. -Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. - -HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:]. - -HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x) - (@measurable_cst _ _ aT rT setT x). - -End mfun. - -Section mfun_realType. -Context {rT : realType}. - -HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT - (@normr rT rT) (@normr_measurable rT setT). - -HB.instance Definition _ := - isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT). - -End mfun_realType. - -Section mfun_measurableType. -Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2} - {d3} {T3 : measurableType d3}. -Variables (f : {mfun T2 >-> T3}) (g : {mfun T1 >-> T2}). - -Lemma measurableT_comp_subproof : measurable_fun setT (f \o g). -Proof. exact: measurableT_comp. Qed. - -HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (f \o g) - measurableT_comp_subproof. - -End mfun_measurableType. - -Section ring. -Context d (aT : measurableType d) (rT : realType). - -Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT). -Proof. -split=> [|f g|f g]; rewrite !inE/=. -- exact: measurable_cst. -- exact: measurable_funB. -- exact: measurable_funM. -Qed. -HB.instance Definition _ := GRing.isSubringClosed.Build _ - (@mfun d default_measure_display aT rT) mfun_subring_closed. -HB.instance Definition _ := [SubChoice_isSubComRing of {mfun aT >-> rT} by <:]. - -Implicit Types (f g : {mfun aT >-> rT}). - -Lemma mfun0 : (0 : {mfun aT >-> rT}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. -Lemma mfun1 : (1 : {mfun aT >-> rT}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. -Lemma mfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. -Lemma mfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. -Lemma mfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. -Lemma mfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. -Lemma mfunMn f n : (f *+ n) = (fun x => f x *+ n) :> (_ -> _). -Proof. by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed. -Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma mfun_prod I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : - (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. -Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. -Lemma mfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). -Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS mfunM/= IHn. Qed. - -HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). -HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). -HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). -HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). - -Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D. - -Lemma mindicE (D : set aT) (mD : measurable D) : - mindic mD = (fun x => (x \in D)%:R). -Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. - -HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD) - (@measurable_indic _ aT rT setT D mD). - -Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} := - mindic mD. - -HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). -Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f. - -Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). -Proof. by split; apply: measurable_maxr. Qed. - -HB.instance Definition _ f g := max_mfun_subproof f g. - -Definition max_mfun f g : {mfun aT >-> _} := f \max g. - -End ring. -Arguments indic_mfun {d aT rT} _. -(* TODO: move earlier?*) -#[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) => - (exact: measurable_indic ) : core. - Section sfun_pred. Context {d} {aT : sigmaRingType d} {rT : realType}. Definition sfun : {pred _ -> _} := [predI @mfun _ _ aT rT & fimfun]. @@ -311,7 +140,7 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:]. -(* NB: already instantiated in cardinality.v *) +(* NB: already in cardinality.v *) HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x). Definition cst_sfun x : {sfun aT >-> rT} := cst x. @@ -371,16 +200,17 @@ HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). Import HBSimple. -(* NB: already instantiated in lebesgue_integral.v *) + +(* TODO: mv to `measurable_realfun.v`? *) HB.instance Definition _ (D : set aT) (mD : measurable D) : @FImFun aT rT (mindic _ mD) := FImFun.on (mindic _ mD). - Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} := mindic rT mD. HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k). Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f. +(* NB: already in `measurable_realfun.v` *) HB.instance Definition _ f g := max_mfun_subproof f g. Definition max_sfun f g : {sfun aT >-> _} := f \max g. @@ -441,9 +271,6 @@ Proof. by move=> /=. Qed. HB.instance Definition _ x := @isNonNegFun.Build T R (cst x%:num) (cst_nnfun_subproof x). -(* NB: already instantiated in cardinality.v *) -HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x). - Definition cst_nnsfun (r : {nonneg R}) : {nnsfun T >-> R} := cst r%:num. Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%:nng. @@ -554,18 +381,6 @@ Qed. End nnsfun_cover. -(* FIXME: shouldn't we avoid calling [done] in a hint? *) -#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => - solve [apply: measurable_sfunP; exact: measurable_set1] : core. - -Lemma measurable_sfun_inP {d} {aT : measurableType d} {rT : realType} - (f : {mfun aT >-> rT}) D (y : rT) : - measurable D -> measurable (D `&` f @^-1` [set y]). -Proof. by move=> Dm; exact: measurableI. Qed. - -#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => - solve [apply: measurable_sfun_inP; assumption] : core. - Section measure_fsbig. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 9c927b2021..9a372846e7 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -600,6 +600,20 @@ Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. #[global] Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. +#[global] Hint Extern 0 (measurable (_ @^-1` [set _])) => + solve [apply: measurable_funPTI; exact: measurable_set1] : core. + +Lemma measurable_funP1 {d} {aT : measurableType d} {rT : realType} + (f : {mfun aT >-> rT}) D (y : rT) : + measurable D -> measurable (D `&` f @^-1` [set y]). +Proof. move=> mD; exact: measurable_funP. Qed. + +#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `measurable_funP1`")] +Notation measurable_sfun_inP := measurable_funP1 (only parsing). + +#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) => + solve [apply: measurable_funP1; assumption] : core. + HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) := { cumulativeNy : f @ -oo --> l ; cumulativey : f @ +oo --> r }. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 6f454af1f2..f820cedcf9 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -41,6 +41,12 @@ From mathcomp Require Export lebesgue_stieltjes_measure. (* of equivalence between emeasurable and the sigma-algebras generated by *) (* open rays and closed rays. *) (* *) +(* ``` *) +(* mindic mD := \1_D where mD is a proof that D is measurable *) +(* indic_mfun mD := mindic mD *) +(* scale_mfun k f := k \o* f *) +(* max_mfun f g := f \max g *) +(* ``` *) (******************************************************************************) Set Implicit Arguments. @@ -1087,6 +1093,83 @@ Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. #[global] Hint Extern 0 (measurable_fun _ expR) => solve [apply: measurable_expR] : core. +Section mfun_realType. +Context {rT : realType}. + +HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT + (@normr rT rT) (@normr_measurable rT setT). + +HB.instance Definition _ := + isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT). + +End mfun_realType. + +Section ring. +Context d (aT : measurableType d) (rT : realType). + +Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT). +Proof. +split=> [|f g|f g]; rewrite !inE/=. +- exact: measurable_cst. +- exact: measurable_funB. +- exact: measurable_funM. +Qed. +HB.instance Definition _ := GRing.isSubringClosed.Build _ + (@mfun d default_measure_display aT rT) mfun_subring_closed. +HB.instance Definition _ := [SubChoice_isSubComRing of {mfun aT >-> rT} by <:]. + +Implicit Types (f g : {mfun aT >-> rT}). + +Lemma mfun0 : (0 : {mfun aT >-> rT}) =1 cst 0 :> (_ -> _). Proof. by []. Qed. +Lemma mfun1 : (1 : {mfun aT >-> rT}) =1 cst 1 :> (_ -> _). Proof. by []. Qed. +Lemma mfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. +Lemma mfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. +Lemma mfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. +Lemma mfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. +Lemma mfunMn f n : (f *+ n) = (fun x => f x *+ n) :> (_ -> _). +Proof. by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed. +Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma mfun_prod I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : + (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. +Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma mfunX f n : f ^+ n = (fun x => f x ^+ n) :> (_ -> _). +Proof. by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS mfunM/= IHn. Qed. + +HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). +HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). +HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). +HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). + +Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D. + +Lemma mindicE (D : set aT) (mD : measurable D) : + mindic mD = (fun x => (x \in D)%:R). +Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. + +HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD) + (@measurable_indic _ aT rT setT D mD). + +Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} := + mindic mD. + +HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). +Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f. + +Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). +Proof. by split; apply: measurable_maxr. Qed. + +HB.instance Definition _ f g := max_mfun_subproof f g. + +Definition max_mfun f g : {mfun aT >-> _} := f \max g. + +End ring. +Arguments indic_mfun {d aT rT} _. +(* TODO: move earlier?*) +#[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) => + (exact: measurable_indic ) : core. + Lemma natmul_measurable {R : realType} D n : measurable_fun D (fun x : R => x *+ n). Proof. diff --git a/theories/measure.v b/theories/measure.v index 2536331e4b..4fc78ffcc9 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -211,6 +211,9 @@ From mathcomp Require Import sequences esum numfun. (* *) (* ``` *) (* measurable_fun D f == the function f with domain D is measurable *) +(* {mfun aT >-> rT} == type of measurable functions *) +(* aT and rT are sigmaRingType's. *) +(* f \in mfun == holds for f : {mfun _ >-> _} *) (* preimage_set_system D f G == set system of the preimages by f of sets in G *) (* image_set_system D f G == set system of the sets with a preimage by f *) (* in G *) @@ -359,6 +362,10 @@ Reserved Notation "f = g %[ae mu ]" (at level 70, g at next level, format "f = g '%[ae' mu ]"). Reserved Notation "{ 'outer_measure' 'set' T '->' '\bar' R }" (T at level 37, format "{ 'outer_measure' 'set' T '->' '\bar' R }"). +Reserved Notation "{ 'mfun' aT >-> T }" + (at level 0, format "{ 'mfun' aT >-> T }"). +Reserved Notation "[ 'mfun' 'of' f ]" + (at level 0, format "[ 'mfun' 'of' f ]"). Inductive measure_display := default_measure_display. Declare Scope measure_display_scope. @@ -1513,6 +1520,42 @@ Definition measurable_fun d d' (T : sigmaRingType d) (U : sigmaRingType d') (D : set T) (f : T -> U) := measurable D -> forall Y, measurable Y -> measurable (D `&` f @^-1` Y). +HB.mixin Record isMeasurableFun d d' (aT : sigmaRingType d) (rT : sigmaRingType d') + (f : aT -> rT) := { + measurable_funPT : measurable_fun [set: aT] f +}. +HB.structure Definition MeasurableFun d d' aT rT := + {f of @isMeasurableFun d d' aT rT f}. +Arguments measurable_funPT {d d' aT rT} s. + +Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type _ _ aT T) : form_scope. +Notation "[ 'mfun' 'of' f ]" := [the {mfun _ >-> _} of f] : form_scope. +#[global] Hint Extern 0 (measurable_fun [set: _] _) => + solve [apply: measurable_funPT] : core. + +Lemma measurable_funP {d d' : measure_display} + {aT : measurableType d} {rT : sigmaRingType d'} + (D : set aT) (s : {mfun aT >-> rT}) : measurable_fun D s. +Proof. +move=> mD Y mY; apply: measurableI => //. +by rewrite -(setTI (_ @^-1` _)); exact: measurable_funPT. +Qed. +Arguments measurable_funP {d d' aT rT D} s. + +Lemma measurable_funPTI {d d'} {aT : measurableType d} {rT : measurableType d'} + (f : {mfun aT >-> rT}) (Y : set rT) : measurable Y -> measurable (f @^-1` Y). +Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. + +#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `measurable_funPTI`")] +Notation measurable_sfunP := measurable_funPTI (only parsing). + +Section mfun_pred. +Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. +Definition mfun : {pred aT -> rT} := mem [set f | measurable_fun setT f]. +Definition mfun_key : pred_key mfun. Proof. exact. Qed. +Canonical mfun_keyed := KeyedPred mfun_key. +End mfun_pred. + Section measurable_fun. Context d1 d2 d3 (T1 : sigmaRingType d1) (T2 : sigmaRingType d2) (T3 : sigmaRingType d3). @@ -1614,6 +1657,41 @@ End measurable_fun. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}. + +Section mfun. +Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. +Notation T := {mfun aT >-> rT}. +Notation mfun := (@mfun _ _ aT rT). + +Section Sub. +Context (f : aT -> rT) (fP : f \in mfun). +Definition mfun_Sub_subproof := @isMeasurableFun.Build d _ aT rT f (set_mem fP). +#[local] HB.instance Definition _ := mfun_Sub_subproof. +Definition mfun_Sub := [mfun of f]. +End Sub. + +Lemma mfun_rect (K : T -> Type) : + (forall f (Pf : f \in mfun), K (mfun_Sub Pf)) -> forall u : T, K u. +Proof. +move=> Ksub [f [[Pf]]]/=. +by suff -> : Pf = (set_mem (@mem_set _ [set f | _] f Pf)) by apply: Ksub. +Qed. + +Lemma mfun_valP f (Pf : f \in mfun) : mfun_Sub Pf = f :> (_ -> _). +Proof. by []. Qed. + +HB.instance Definition _ := isSub.Build _ _ T mfun_rect mfun_valP. + +Lemma mfuneqP (f g : {mfun aT >-> rT}) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. + +HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:]. + +HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x) + (@measurable_cst _ _ aT rT setT x). + +End mfun. + Section measurable_fun_measurableType. Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3). @@ -1725,6 +1803,19 @@ End measurable_fun_measurableType. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_bool {d1 T1 D f} b. +Section mfun_measurableType. +Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2} + {d3} {T3 : measurableType d3}. +Variables (f : {mfun T2 >-> T3}) (g : {mfun T1 >-> T2}). + +Let measurableT_comp_subproof : measurable_fun setT (f \o g). +Proof. exact: measurableT_comp. Qed. + +HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (f \o g) + measurableT_comp_subproof. + +End mfun_measurableType. + Section measurability. Definition preimage_set_system {aT rT : Type} (D : set aT) (f : aT -> rT) diff --git a/theories/probability.v b/theories/probability.v index 5d49431e35..8ae703d381 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -237,9 +237,9 @@ have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a. suff : P (F n) @[n --> \oo] --> P (\bigcap_n F n). by rewrite [in X in _ --> X -> _]/F -preimage_bigcap -itvNycEbigcap. apply: nonincreasing_cvg_mu => [| | |m n mn]. - - by rewrite -ge0_fin_numE// fin_num_measure//; exact: measurable_sfunP. - - by move=> ?; exact: measurable_sfunP. - - by apply: bigcap_measurable => // ? _; exact: measurable_sfunP. + - by rewrite -ge0_fin_numE// fin_num_measure//; exact: measurable_funPTI. + - by move=> ?; exact: measurable_funPTI. + - by apply: bigcap_measurable => // ? _; exact: measurable_funPTI. - apply/subsetPset; apply: preimage_subset; apply: subset_itvl. by rewrite bnd_simp lerD2l lef_pV2 ?posrE// ler_nat. by rewrite -(cvg_unique _ cdf_ns cdf_na).