Merge pull request #616 from math-comp/dirac_measure

dirac measure

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
+### Misc

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}).

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.

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).