From 87efa7adf6456a13d6661c93020e4088d9533f3f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 28 Mar 2022 19:11:17 +0900 Subject: [PATCH] Dirac measure --- CHANGELOG_UNRELEASED.md | 8 +++- theories/lebesgue_integral.v | 82 +++++++++++++++++++++++++++++++++++- theories/mathcomp_extra.v | 2 +- theories/measure.v | 67 +++++++++++++++++++++++++++++ 4 files changed, 156 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b993fc897..c0581e353 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -73,6 +73,10 @@ + lemma `emeasurable_funN` - in file `measure.v`: + definition `pushforward` and canonical `pushforward_measure` + + definition `dirac` with notation `\d_` and canonical `dirac_measure` + + lemmas `finite_card_dirac`, `infinite_card_dirac` +- in file `lebesgue_integral.v`: + + lemmas `integralM_indic`, `integralM_indic_nnsfun`, `integral_dirac` ### Changed @@ -82,6 +86,8 @@ + hint `measurable_set1`/`emeasurable_set1` - in `sequences.v`: + generalize `eq_nneseries`, `nneseries0` +- in `mathcomp_extra.v`: + + generalize `card_fset_sum1` ### Renamed @@ -182,4 +188,4 @@ ### Infrastructure -### Misc \ No newline at end of file +### Misc diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index cb7d9b8bc..117a04365 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. Require Import mathcomp_extra boolp classical_sets signed functions cardinality. -Require Import reals ereal topology normedtype sequences measure. +Require Import reals ereal topology normedtype sequences esum measure. Require Import lebesgue_measure fsbigop numfun. (******************************************************************************) @@ -64,6 +64,9 @@ Reserved Notation "'\int_' D f ''d' mu [ x ]" (at level 36, D at level 0, Reserved Notation "'\int' f ''d' mu [ x ]" (at level 36, f at level 36, mu at level 0, x at level 3, format "'\int' f ''d' mu [ x ]"). Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable"). +Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a"). +#[global] +Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. HB.mixin Record IsMeasurableFun (aT : measurableType) (rT : realType) (f : aT -> rT) := { measurable_funP : measurable_fun setT f @@ -2242,6 +2245,83 @@ Qed. End integral_ind. +Section integralM_indic. +Local Open Scope ereal_scope. +Variables (T : measurableType) (R : realType) (m : {measure set T -> \bar R}). +Variables (D : set T) (mD : measurable D). + +Lemma integralM_indic (f : R -> set T) (k : R) : + ((k < 0)%R -> f k = set0) -> measurable (f k) -> + \int_ D (k * \1_(f k) x)%:E 'd m[x] = k%:E * \int_ D (\1_(f k) x)%:E 'd m[x]. +Proof. +move=> fk0 mfk; have [k0|k0] := ltP k 0%R. + rewrite (eq_integral (cst 0%E)) ?integral0 ?mule0; last first. + by move=> x _; rewrite fk0// indic0 mulr0. + rewrite (eq_integral (cst 0%E)) ?integral0 ?mule0// => x _. + by rewrite fk0// indic0. +under eq_integral do rewrite EFinM. +rewrite ge0_integralM//. +- apply/EFin_measurable_fun/(@measurable_funS _ _ setT) => //. + by rewrite (_ : \1_(f k) = mindic R mfk). +- by move=> y _; rewrite lee_fin. +Qed. + +Lemma integralM_indic_nnsfun (f : {nnsfun T >-> R}) (k : R) : + \int_ D (k * \1_(f @^-1` [set k]) x)%:E 'd m[x] = + k%:E * \int_ D (\1_(f @^-1` [set k]) x)%:E 'd m[x]. +Proof. +rewrite (@integralM_indic (fun k => f @^-1` [set k]))// => k0. +by rewrite preimage_nnfun0. +Qed. + +End integralM_indic. + +Section integral_dirac. +Local Open Scope ereal_scope. +Variables (T : measurableType) (a : T) (R : realType). +Variables (D : set T) (mD : measurable D). + +Let ge0_integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) + (f0 : forall x, D x -> 0 <= f x) : + D a -> \int_ D (f x) 'd (\d_ a)[x] = f a. +Proof. +move=> Da; have [f_ [ndf_ f_f]] := approximation mD mf f0. +transitivity (lim (fun n => \int_ D (f_ n x)%:E 'd (\d_ a)[x])). + rewrite -monotone_convergence//. + - apply: eq_integral => x Dx; apply/esym/cvg_lim => //; apply: f_f. + by rewrite inE in Dx. + - by move=> n; apply/EFin_measurable_fun; exact/(@measurable_funS _ _ setT). + - by move=> *; rewrite lee_fin. + - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. +rewrite (_ : (fun _ => _) = (fun n => (f_ n a)%:E)). + by apply/cvg_lim => //; exact: f_f. +apply/funext => n; under eq_integral do rewrite fimfunE -sumEFin. +rewrite ge0_integral_sum//. +- under eq_bigr; first by move=> r _; rewrite integralM_indic_nnsfun//; over. + rewrite /= (big_fsetD1 (f_ n a))/=; last first. + by rewrite in_fset_set// in_setE; exists a. + rewrite integral_indic//= /dirac indicE mem_set// mule1. + rewrite big1_fset ?adde0// => r; rewrite !inE => /andP[rfna _] _. + rewrite integral_indic//= /dirac indicE memNset ?mule0//. + by apply/not_andP; left; exact/nesym/eqP. +- move=> r; apply/EFin_measurable_fun. + apply: measurable_funM => //; first exact: measurable_fun_cst. + apply: (@measurable_funS _ _ setT) => //. + by rewrite (_ : \1_ _ = mindic R (measurable_sfunP (f_ n) r)). +- by move=> r x _; rewrite muleindic_ge0. +Qed. + +Lemma integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) : + D a -> \int_ D (f x) 'd (\d_ a)[x] = f a. +Proof. +move=> Da. +rewrite integralE ge0_integral_dirac//; last exact/emeasurable_fun_funepos. +rewrite ge0_integral_dirac//; last exact/emeasurable_fun_funeneg. +by rewrite [in RHS](funeposneg f). +Qed. + +End integral_dirac. + Section subset_integral. Local Open Scope ereal_scope. Variables (T : measurableType) (R : realType) (mu : {measure set T -> \bar R}). diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v index 76c9cb629..7bb462a36 100644 --- a/theories/mathcomp_extra.v +++ b/theories/mathcomp_extra.v @@ -160,7 +160,7 @@ have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT. by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn). Qed. -Lemma card_fset_sum1 (A : {fset nat}) : #|` A| = \sum_(i <- A) 1. +Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) : #|` A| = \sum_(i <- A) 1. Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed. Arguments big_rmcond {R idx op I r} P. diff --git a/theories/measure.v b/theories/measure.v index 406fa0ab8..1db42cf16 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2,6 +2,7 @@ From mathcomp Require Import all_ssreflect all_algebra finmap. Require Import boolp classical_sets mathcomp_extra reals ereal signed. Require Import functions topology normedtype sequences cardinality esum fsbigop. +Require Import numfun. From HB Require Import structures. (******************************************************************************) @@ -61,6 +62,7 @@ From HB Require Import structures. (* that this function maps set0 to 0, is non-negative over *) (* measurable sets and is semi-sigma-additive *) (* pushforward f m == pushforward/image measure of m by f *) +(* \d_a == Dirac measure *) (* sigma_finite A f == the measure f is sigma-finite on A : set T with *) (* T : ringOfSetsType. *) (* mu.-negligible A == A is mu negligible *) @@ -1379,6 +1381,71 @@ Canonical pushforward_measure : {measure set T2 -> \bar R} := End pushforward_measure. +Section dirac_measure. +Local Open Scope ereal_scope. +Variables (T : measurableType) (a : T) (R : realFieldType). + +Definition dirac (A : set T) : \bar R := (\1_A a)%:E. + +Let dirac0 : dirac set0 = 0. Proof. by rewrite /dirac indic0. Qed. + +Let dirac_ge0 B : 0 <= dirac B. Proof. by rewrite /dirac indicE. Qed. + +Let dirac_sigma_additive : semi_sigma_additive dirac. +Proof. +move=> F mF tF mUF; rewrite /dirac indicE; have [|aFn] /= := boolP (a \in _). + rewrite inE => -[n _ Fna]. + have naF m : m != n -> a \notin F m. + move=> mn; rewrite notin_set => Fma. + move/trivIsetP : tF => /(_ _ _ Logic.I Logic.I mn). + by rewrite predeqE => /(_ a)[+ _]; exact. + apply/cvg_ballP => _/posnumP[e]; rewrite near_map; near=> m. + have mn : (n < m)%N by near: m; exists n.+1. + rewrite big_mkord (bigID (xpred1 (Ordinal mn)))//= big_pred1_eq/= big1/=. + by rewrite adde0 indicE mem_set//; exact: ballxx. + by move=> j ij; rewrite indicE (negbTE (naF _ _)). +rewrite [X in X --> _](_ : _ = cst 0); first exact: cvg_cst. +apply/funext => n; rewrite big1// => i _; rewrite indicE; apply/eqP. +by rewrite eqe pnatr_eq0 eqb0; apply: contra aFn => /[!inE] aFn; exists i. +Unshelve. all: by end_near. Qed. + +Canonical dirac_measure : {measure set T -> \bar R} := + Measure.Pack _ (Measure.Axioms dirac0 dirac_ge0 dirac_sigma_additive). + +End dirac_measure. +Arguments dirac {T} _ {R}. +Arguments dirac_measure {T} _ {R}. + +Notation "\d_ a" := (dirac_measure a) : ring_scope. + +Section dirac_lemmas. +Local Open Scope ereal_scope. +Variables (T : measurableType) (R : realType). + +Lemma finite_card_dirac (A : set T) : finite_set A -> + \esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R. +Proof. +move=> finA. +rewrite -sum_fset_set// big_seq_cond (eq_bigr (fun=> 1)) -?big_seq_cond. + by rewrite card_fset_sum1// natr_sum -sumEFin. +by move=> i; rewrite andbT in_fset_set//= /dirac indicE => ->. +Qed. + +Lemma infinite_card_dirac (A : set T) : infinite_set A -> + \esum_(i in A) \d_ i A = +oo :> \bar R. +Proof. +move=> infA; apply/eq_pinftyP => r r0. +have [B BA Br] := infinite_set_fset `|ceil r| infA. +apply: esum_ge; exists B => //; apply: (@le_trans _ _ `|ceil r|%:R%:E). + by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0// ceil_ge. +move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply. +rewrite big_seq (eq_bigr (cst 1))/=; last first. + by move=> i Bi; rewrite /dirac indicE mem_set//; exact: BA. +by rewrite -big_seq card_fset_sum1 sumEFin natr_sum. +Qed. + +End dirac_lemmas. + Section measure_restr. Variables (T : measurableType) (R : realType) (mu : {measure set T -> \bar R}). Variables (D : set T) (mD : measurable D).