Module mathcomp.analysis.measure_theory.dirac_measure

From HB Require Import structures.
From mathcomp Require Import boot order algebra interval_inference finmap.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop
reals.
From mathcomp Require Import topology ereal normedtype sequences esum numfun.
From mathcomp Require Import measurable_structure measure_function.

# The Dirac Measure ``` \d_a == Dirac measure ```

Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a").

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section dirac_measure.
Local Open Scope ereal_scope.
Context ( : sigmaRingType d) ( : T) ( : realFieldType).

Definition ( : set T) : \bar R := (\1_A a)%:E.

Let : dirac set0 = 0

Proof.

by rewrite /dirac indic0. Qed.

Let : 0 <= dirac B

Proof.

by rewrite /dirac indicE. Qed.

Let : 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_setE => Fma.
    move/trivIsetP : tF => /(_ _ _ Logic.I Logic.I mn).
    by rewrite predeqE => /(_ a)[+ _]; exact.
  apply/cvg_ballP => _/posnumP[e]; 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 move=> j ij; rewrite indicE (negbTE (naF _ _)).
  by rewrite adde0 indicE mem_set//; exact: ballxx.
rewrite [X in X @ _ --> _](_ : _ = cst 0)//.
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.

..Build _ _ _
dirac dirac0 dirac_ge0 dirac_sigma_additive.

End dirac_measure.
Arguments dirac {d T} _ {R}.

Notation := (dirac a) : ring_scope.

Section dirac_lemmas_realFieldType.
Local Open Scope ereal_scope.
Context ( : sigmaRingType d) ( : realFieldType).

Lemma ( : set T) : \d_a A = (a \in A)%:R%:E :> \bar R.

Proof.

by rewrite /dirac indicE. Qed.

Lemma ( : T) : \d_a set0 = 0 :> \bar R.

Proof.

by rewrite diracE in_set0. Qed.

Lemma ( : T) : \d_a setT = 1 :> \bar R.

Proof.

by rewrite diracE in_setT. Qed.

End dirac_lemmas_realFieldType.

Section dirac_lemmas.
Local Open Scope ereal_scope.
Context ( : sigmaRingType d) ( : realType).

Lemma ( : set T) : finite_set A ->
\esum_( in A) 1 = (#|` fset_set A|%:R)%:E :> \bar R.

Proof.

move=> finA; rewrite esum_fset// (eq_fsbigr (cst 1))//.
by rewrite card_fset_sum1// natr_sum -sumEFin fsbig_finite.
Qed.

Lemma ( : set T) : finite_set A ->
\esum_( in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R.

Proof.

move=> finA; rewrite esum_fset// (eq_fsbigr (cst 1))//.
by move=> i iA; rewrite diracE iA.
by rewrite card_fset_sum1// natr_sum -sumEFin fsbig_finite.
Qed.

Lemma ( : set T) : infinite_set A ->
\esum_( in A) \d_ i A = +oo :> \bar R.

Proof.

move=> infA; apply/eqyP => r r0.
have [B BA Br] := infinite_set_fset (Num.truncn r).+1 infA.
rewrite ge0_esum//; apply: PosEsum.pos_esum_ge; exists [set` B] => //.
apply: (@le_trans _ _ (Num.truncn r).+1%:R%:E).
by rewrite lee_fin ltW// truncnS_gt.
move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply.
rewrite (eq_fsbigr (cst 1))/=; last first.
by rewrite fsbig_finite//= card_fset_sum1 sumEFin natr_sum// set_fsetK.
by move=> i /[!inE] /BA /mem_set iA; rewrite diracE iA.
Qed.

End dirac_lemmas.

Files

Module mathcomp.analysis.measure_theory.dirac_measure