Files

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 dSource code (TSource code : sigmaRingType d) (aSource code : T) (RSource code : realFieldType).

Definition dirac
Used by
  • mathcomp.analysis.measure_theory.probability_measure
  • mathcomp.analysis.kernel
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.giry
Source code (ASource code : set T) : \bar R := (\1_A a)%:E.

Let dirac0Source code : dirac set0 = 0
Proof.
by rewrite /dirac indic0. Qed.

Let dirac_ge0Source code BSource code : 0 <= dirac B
Proof.
by rewrite /dirac indicE. Qed.

Let dirac_sigma_additiveSource code : 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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isMeasureSource code.Build _ _ _
  dirac dirac0 dirac_ge0 dirac_sigma_additive.

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

Notation "\d_ a"Source code := (dirac a) : ring_scope.

Section dirac_lemmas_realFieldType.
Local Open Scope ereal_scope.
Context dSource code (TSource code : sigmaRingType d) (RSource code : realFieldType).

Lemma diracEUsed by
  • mathcomp.analysis.probability_theory.random_variable
  • mathcomp.analysis.probability_theory.binomial_distribution
  • mathcomp.analysis.probability_theory.bernoulli_distribution
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
Source code aSource code (ASource code : set T) : \d_a A = (a \in A)%:R%:E :> \bar R.
Proof.
by rewrite /dirac indicE. Qed.

Lemma dirac0Source code (aSource code : T) : \d_a set0 = 0 :> \bar R.
Proof.
by rewrite diracE in_set0. Qed.

Lemma diracTUsed by
  • mathcomp.analysis.probability_theory.random_variable
  • mathcomp.analysis.probability_theory.binomial_distribution
  • mathcomp.analysis.probability_theory.bernoulli_distribution
  • mathcomp.analysis.measure_theory.probability_measure
  • mathcomp.analysis.kernel
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.giry
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable
Source code (aSource code : 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 dSource code (TSource code : sigmaRingType d) (RSource code : realType).

Lemma finite_card_sumUsed by
  • mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation
Source code (ASource code : set T) : finite_set A ->
  \esum_(iSource code 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 finite_card_diracUsed by
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
Source code (ASource code : set T) : finite_set A ->
  \esum_(iSource code 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 infinite_card_diracUsed by
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
Source code (ASource code : set T) : infinite_set A ->
  \esum_(iSource code 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.
Generated by rocqnavi
Source
Uses
Used By