Module mathcomp.analysis.measure_theory.probability_measure

From HB Require Import structures.
From mathcomp Require Import boot order algebra.
From mathcomp Require Import boolp classical_sets functions cardinality reals.
From mathcomp Require Import interval_inference ereal topology normedtype.
From mathcomp Require Import measurable_structure measure_function dirac_measure.

# Probability Measures ``` isSubProbability == interface for functions that satisfy the property of subprobability The HB class is SubProbability. subprobability T R == subprobability measure over the measurableType T with values in \bar R with R : realType The HB class is SubProbability. Measure_isSubProbability == interface that extends measures to subprobability measures isProbability == interface for functions that satisfy the property of probability measures The HB class is Probability. probability T R == type of probability measure over the measurableType T with values in \bar R with R : realType Measure_isProbability == interface that extends measures to probability measures mnormalize mu == normalization of a measure to a probability ``` ``` mset U r == the set of probability measures mu such that mu U < r pset == the sets mset U r with U measurable and r \in [0,1] pprobability == the measurable type generated by pset ```

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.

. ( d) (R : realType)
  (P : set T -> \bar R) := { sprobability_setT : (P setT <= 1)%E }.

()
. ( d) (R : realType)
  := { of @FiniteMeasure d T R mu & isSubProbability d T R mu }.

. ( d)
    (R : realType) (P : set T -> \bar R) & isMeasure _ _ _ P :=
  { sprobability_setT : (P setT <= 1)%E }.

. ( d) (R : realType)
  P & Measure_isSubProbability d T R P.

Let : @Measure_isFinite d T R P.

Proof.

split; apply: lty_fin_num_fun.
by rewrite (le_lt_trans (@sprobability_setT))// ltey.
Qed.

..

..Build _ _ _ P sprobability_setT.

..

Section mzero_subprobability.
Context ( : measurableType d) ( : realType).

Let : (@mzero d T R setT <= 1)%E.

Proof.

by rewrite /mzero/=. Qed.

.
  Measure_isSubProbability.Build _ _ _ (@mzero d T R) mzero_setT.

End mzero_subprobability.

. ( d) (R : realType)
  (P : set T -> \bar R) := { probability_setT : P setT = 1%E }.

()
. ( d) (R : realType) :=
  { of @SubProbability d T R P & isProbability d T R P }.

Arguments probability_setT {d T R} s.

. ( d) (R : realType) :=
  gen_eqMixin (probability T R).
. ( d) (R : realType) :=
  gen_choiceMixin (probability T R).

Section probability_lemmas.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType) ( : probability T R).

Lemma ( : set T) : measurable A -> P A <= 1.

Proof.

by move=> mA; rewrite -(probability_setT P) ?le_measure ?in_setE. Qed.

Lemma ( : set T) : measurable A -> P (~` A) = 1 - P A.

Proof.

move=> mA; rewrite -(probability_setT P) -(setvU A) measureU ?addeK ?setICl//.
exact: measurableC.
by rewrite fin_num_measure.
Qed.

End probability_lemmas.

. ( d)
    (R : realType) (P : set T -> \bar R) & isMeasure _ _ _ P :=
  { probability_setT : P setT = 1%E }.

. ( d) (R : realType)
  P & Measure_isProbability d T R P.

Let : @Measure_isSubProbability d T R P.

Proof.

by split; rewrite probability_setT. Qed.

..

..Build _ _ _ P probability_setT.

..

Section pdirac.
Context ( : measurableType d) ( : realType).

.
  Measure_isProbability.Build _ _ _ (@dirac _ T x R) (diracT R x).

End pdirac.

Section mnormalize.
Local Open Scope ereal_scope.
Context ( : measurableType d) ( : realType).
Variables ( : {measure set T -> \bar R}) ( : probability T R).

Definition :=
  let := mu [set: T] in
  if (evidence == 0) || (evidence == +oo) then fun => P U
  else fun => mu U * (fine evidence)^-1%:E.

Let : mnormalize set0 = 0.

Proof.

by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e.
Qed.

Let : 0 <= mnormalize U.

Proof.

by rewrite /mnormalize; case: ifPn. Qed.

Let : semi_sigma_additive mnormalize.

Proof.

move=> F mF tF mUF; rewrite /mnormalize/=.
case: ifPn => [_|_]; first exact: measure_semi_sigma_additive.
rewrite [X in X @ _ --> _](_ : _ = (fun => \sum_(0 <= < n) mu (F i)) \*
cst (fine (mu setT))^-1%:E).
by apply/funext => n; rewrite -ge0_sume_distrl.
by apply: cvgeZr => //; exact: measure_semi_sigma_additive.
Qed.

..Build _ _ _ mnormalize
mnormalize0 mnormalize_ge0 mnormalize_sigma_additive.

Let : mnormalize [set: T] = 1.

Proof.

rewrite /mnormalize; case: ifPn; first by rewrite probability_setT.
rewrite negb_or => /andP[ft0 ftoo].
have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// ltey.
by rewrite -{1}(@fineK _ (mu setT))// -EFinM divff// fine_eq0.
Qed.

.
Measure_isProbability.Build _ _ _ mnormalize mnormalize1.

End mnormalize.

Lemma ( : measurableType d) ( : realType)
( : probability T R) : mnormalize P P' = P.

Proof.

apply/funext => x; rewrite /mnormalize/= probability_setT.
by rewrite onee_eq0/= invr1 mule1.
Qed.

. ( d) (R : realType) :=
isPointed.Build (probability T R) (dirac point).

Section dist_sigma_algebra_instance.
Context ( : measurableType d) ( : realType).

Definition ( : set T) ( : R) :=
[set : probability T R | mu U < r%:E]%E.

Lemma ( : set T) ( : R) : (r < 0)%R -> mset U r = set0.

Proof.

move=> r0; apply/seteqP; split => // x/=.
by apply/negP; rewrite -leNgt (@le_trans _ _ 0%E)// lee_fin ltW.
Qed.

Lemma ( : set T) ( : R) :
measurable U -> (1 < r)%R -> mset U r = [set: probability T R].

Proof.

move=> mU r1; apply/seteqP; split => // x/= _.
by rewrite /mset/= (le_lt_trans (probability_le1 _ _)).
Qed.

Definition : set_system (probability T R) :=
[set mset U r | in `[0%R,1%R] & in measurable].

Definition : measurableType pset.-sigma :=
g_sigma_algebraType pset.

End dist_sigma_algebra_instance.

Files

Module mathcomp.analysis.measure_theory.probability_measure