Skip to content

Add lemma pmf_measurable #1827

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Yosuke-Ito-345 wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add lemma pmf_measurable #1827

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7b7f690
pmf measurable
Yosuke-Ito-345 Jan 20, 2026
a958a9d
fix proof
Yosuke-Ito-345 Jan 27, 2026
a004013
modify changelog
Yosuke-Ito-345 Jan 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,15 @@
## [Unreleased]

### Added
- in classical_sets.v
+ lemma `in_set1_eq`

- in set_interval.v
+ definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`

- in probability.v
+ lemmas `pmf_gt0_countable`, `pmf_measurable`

### Changed
- in set_interval.v
+ `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
Expand Down
5 changes: 5 additions & 0 deletions classical/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -422,6 +422,11 @@ Lemma nat_nonempty : [set: nat] !=set0. Proof. by exists 1%N. Qed.

#[global] Hint Resolve nat_nonempty : core.

Lemma in_set1_eq {T : eqType} (a : T) (x : T) : x \in [set a] = (x == a).
Copy link
Member

@t6s t6s Jan 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this lemma deserves the name in_set1, and the current in_set1 can be removed at all
(or the latter should be renamed to something like in_set1_fin or in_finset1).

@CohenCyril

Copy link
Member

@t6s t6s Jan 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

in_set1 is not used at all in mathcomp-analysis master!

master$ find . -name "*.v" -exec grep -Hn "in_set1" {} ';'
./classical/classical_sets.v:2199:Lemma in_set1 [T : finType] (x y : T) : (x \in [set y]) = (x \in [set y]%SET).
master$

Proof.
by apply/(sameP _ idP)/(equivP idP); rewrite inE eq_opE.
Qed.

Lemma itv_sub_in2 d (T : porderType d) (P : T -> T -> Prop) (i j : interval T) :
[set` j] `<=` [set` i] ->
{in i &, forall x y, P x y} -> {in j &, forall x y, P x y}.
Expand Down
79 changes: 75 additions & 4 deletions theories/probability.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1072,6 +1072,78 @@ Qed.

End distribution_dRV.

Definition pmf d (T : measurableType d) (R : realType) (P : probability T R)
(X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])).

Section pmf_measurable.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType)
(P : probability T R) (X : {RV P >-> R}).

Lemma pmf_gt0_countable : countable [set r | (0 < pmf X r)%R].
Proof.
have ->: [set r | 0 < (pmf X r)%:E] =
\bigcup_n [set r | (n.+1%:R^-1 < pmf X r)%R].
apply/seteqP; split => [r /ltr_add_invr [l] | r [k] _]; last exact: lt_trans.
by rewrite add0r => lpmf; exists l.
apply: bigcup_countable => // n _.
apply: finite_set_countable; apply: contrapT => /infiniteP/pcard_leP/injfunPex.
case=> q q_fun q_inj /=.
have pre1 k : measurable (X @^-1` [set q k]).
by apply: measurable_funPTI; exact: measurable_set1.
rewrite -falseE -(ltxx (1:R)%:E).
apply: (@lt_le_trans _ _ (P (\bigcup_k X @^-1` [set q k])));
last by apply/probability_le1/bigcup_measurable => k _.
have <-: \big[+%R/0%R]_(0 <= k <oo | k \in setT) P (X @^-1` [set q k]) =
P (\bigcup_k X @^-1` [set q k]).
rewrite measure_bigcup// (trivIset_comp (fun r => X@^-1` [set r]))//.
exact: trivIset_preimage1.
apply: (@lt_le_trans _ _
(\sum_(0 <= k < n.+1 | k \in setT) P (X @^-1` [set q k])));
last exact: nneseries_lim_ge.
rewrite (eq_bigl xpredT) => [| ?]; last by rewrite in_setT.
under eq_bigr => k _ do
rewrite -(@fineK _ (P _)) ?fin_num_measure// -/(pmf X (q k)).
have ->: 1%R = (\sum_(0 <= k < n.+1) n.+1%:R^-1:R)%R
by rewrite sumr_const_nat subn0 -(mulr_natr _^-1) mulVf.
by rewrite !sumEFin lte_fin; apply: ltr_sum => // k _; exact: q_fun.
Qed.

Lemma pmf_measurable : measurable_fun setT (pmf X).
Proof.
have : countable [set r | (0 < pmf X r)%R] by exact pmf_gt0_countable.
case/countable_bijP => S.
rewrite card_eq_sym; case/pcard_eqP/bijPex => /= h h_bij.
apply/measurable_EFinP.
pose sfun r :=
\big[+%R/0%R]_(0 <= k <oo | in_set S k) (pmf X (h k) * \1_[set h k] r)%:E.
have pmf_ge0 s : 0 <= (pmf X s)%:E by rewrite fineK ?fin_num_measure.
have pmf1_ge0 k s : 0%R <= (pmf X (h k) * \1_[set h k] s)%:E.
by rewrite EFinM; apply: mule_ge0.
apply: (eq_measurable_fun sfun) => [r _|].
case/asboolP: ([set h k | k in S] r) => [rS | nrS].
- pose kr := (pinv S h r).
have neqh k : (k \in S) && (k != kr) -> r != h k.
move/andP=>[Sk]; apply: contra_neq.
by rewrite /kr => ->; rewrite pinvKV//; exact: (set_bij_inj h_bij).
rewrite /sfun (@nneseriesD1 _ _ kr)//; last by rewrite in_setE; apply: invS.
rewrite eseries0 => [| k k_ge0 /(neqh _)/negPf].
by rewrite indicE in_set1_eq pinvK ?in_setE// eq_refl mulr1 addr0.
by rewrite indicE in_set1_eq => ->; rewrite mulr0.
- rewrite /sfun eseries0 => [|k k_ge0 Sk]/=.
apply: le_anti; rewrite pmf_ge0 lee_fin leNgt.
apply/negP/contra_not/nrS.
by rewrite (surj_image_eq _ (set_bij_surj h_bij))//; exact: set_bij_sub.
rewrite indicE in_set1_eq.
suff ->: (r == h k) = false by rewrite mulr0.
by apply/eqP/contra_not/nrS => ->; exists k => //; rewrite -(in_setE S k).
apply: ge0_emeasurable_sum => //= k _.
apply/measurable_EFinP/measurable_funM;
[exact: measurable_cst | exact/measurable_indicP].
Qed.

End pmf_measurable.

Section discrete_distribution.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Expand Down Expand Up @@ -1122,11 +1194,10 @@ apply: eq_eseriesr => k _; case: ifPn => kX.
by rewrite integral_set0 mule0 /enum_prob patchE (negbTE kX) mul0e.
Qed.

Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])).

Lemma expectation_pmf (X : {dRV P >-> R}) :
P.-integrable [set: T] (EFin \o X) -> 'E_P[X] =
\sum_(n <oo | n \in dRV_dom X) (pmf X (dRV_enum X n))%:E * (dRV_enum X n)%:E.
P.-integrable [set: T] (EFin \o X) ->
'E_P[X] = \sum_(n <oo | n \in dRV_dom X)
(pmf(P:=P) X (dRV_enum X n))%:E * (dRV_enum X n)%:E.
Proof.
move=> iX; rewrite dRV_expectation// [in RHS]eseries_mkcond.
apply: eq_eseriesr => k _.
Expand Down
Loading