Skip to content

Commit

Permalink
sampling_lemma
Browse files Browse the repository at this point in the history
bernoulli probability measure
wise_inde_weak
complete pairwise_independentM
mutually_independent_weak
bayes
binomial_mmt_gen_fun
generalizing discrete random variables
bernoulli RVs are discrete
bernoulli_mmt_gen_fun

Co-authored-by: @affeldt-aist
Co-authored-by: @t6s
  • Loading branch information
hoheinzollern committed Nov 24, 2024
1 parent 4b26927 commit d5cb0f9
Show file tree
Hide file tree
Showing 5 changed files with 1,706 additions and 103 deletions.
8 changes: 8 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,14 @@
`independent_RVs2_funrpospos`
+ lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
` expectation_prod`
- in `lebesgue_integral.v`:
+ lemma `abse_integralP`
- in `signed.v`:
+ definition `onem_NngNum`
- in `measure.v`:
+ definition `bernoulli`, declared as a probability measure instance
- in `itv.v`:
+ canonical `onem_itv01`

### Changed

Expand Down
5 changes: 3 additions & 2 deletions reals/itv.v
Original file line number Diff line number Diff line change
Expand Up @@ -850,6 +850,9 @@ Lemma inum_lt : {mono inum : x y / (x < y)%O}. Proof. by []. Qed.

End Morph.

Canonical onem_itv01 {R : realDomainType} (p : {i01 R}) : {i01 R} :=
@Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].

Section Test1.

Variable R : numDomainType.
Expand Down Expand Up @@ -893,8 +896,6 @@ apply/val_inj => /=.
by rewrite subr0 mulr1 opprB addrCA subrr addr0.
Qed.

Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
@Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].

Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
(`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01.
Expand Down
1 change: 1 addition & 0 deletions reals/signed.v
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,7 @@ From mathcomp Require Import mathcomp_extra.
(* Canonical instances are also provided according to types, as a *)
(* fallback when no known operator appears in the expression. Look to *)
(* nat_snum below for an example on how to add your favorite type. *)
(* *)
(******************************************************************************)

Reserved Notation "{ 'compare' x0 & nz & cond }"
Expand Down
12 changes: 4 additions & 8 deletions theories/lebesgue_integral.v
Original file line number Diff line number Diff line change
Expand Up @@ -4958,19 +4958,16 @@ Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
Implicit Types A : set (T1 * T2).

Let pm10 : (m1 \x m2) set0 = 0.
Proof. by rewrite [LHS]integral0_eq// => x/= _; rewrite xsection0 measure0. Qed.
Proof. by rewrite [LHS]integral0_eq// => x/= _; rewrite xsection0. Qed.

Let pm1_ge0 A : 0 <= (m1 \x m2) A.
Proof.
by apply: integral_ge0 => // *; exact/measure_ge0/measurable_xsection.
Qed.
Proof. by apply: integral_ge0 => // *. Qed.

Let pm1_sigma_additive : semi_sigma_additive (m1 \x m2).
Proof.
move=> F mF tF mUF.
rewrite [X in _ --> X](_ : _ = \sum_(n <oo) (m1 \x m2) (F n)).
apply/cvg_closeP; split; last by rewrite closeE.
by apply: is_cvg_nneseries => *; exact: integral_ge0.
by apply/cvg_closeP; split; [exact: is_cvg_nneseries|rewrite closeE].
rewrite -integral_nneseries//; last by move=> n; exact: measurable_fun_xsection.
apply: eq_integral => x _; apply/esym/cvg_lim => //=; rewrite xsection_bigcup.
apply: (measure_sigma_additive _ (trivIset_xsection tF)) => ?.
Expand Down Expand Up @@ -5029,8 +5026,7 @@ HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)

Lemma product_measure_unique
(m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) :
(forall A1 A2, measurable A1 -> measurable A2 ->
m' (A1 `*` A2) = m1 A1 * m2 A2) ->
(forall A B, measurable A -> measurable B -> m' (A `*` B) = m1 A * m2 B) ->
forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.
Proof.
move=> m'E.
Expand Down
Loading

0 comments on commit d5cb0f9

Please sign in to comment.