Add lemma `pmf_measurable` #1827

Yosuke-Ito-345 · 2026-01-20T12:47:36Z

Motivation for this change

Prove that the function pmf is measurable.

Checklist

added corresponding entries in CHANGELOG_UNRELEASED.md
added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

PRs with several commits that make sense individually and that
all compile are preferentially merged into master.
PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

Read this Checklist
Put a milestone if possible
Check labels

Yosuke-Ito-345 · 2026-01-20T12:55:04Z

@affeldt-aist @t6s
I kindly ask for your review of this pull request.
Please note that I moved the definition of pmf outside of the Section discrete_distribution, because the random variable here need not be discrete and I'm planning to use the lemma pmf_measurable for a general random variable.

t6s

The statements and the code look good modulo some cleaning as I commented.
I think in_set1_eq can replace in_set1, but not necessarily by this PR.

t6s · 2026-01-26T05:33:51Z

theories/probability.v

+Context d (T : measurableType d) (R : realType)
+  (P : probability T R) (X : {RV P >-> R}).
+
+Lemma pmf_positive_countable : countable [set r | (0 < pmf X r)%R].


pmf_gt0_countable will be more conformant with other names

t6s · 2026-01-26T05:38:51Z

theories/probability.v

+Proof.
+have ->: [set r | 0 < (pmf X r)%:E] =
+  \bigcup_n [set r | (n.+1%:R^-1 < pmf X r)%R].
+  rewrite seteqP; split => [r /ltr_add_invr [l] | r [k] _]; last exact: lt_trans.


Suggested change

rewrite seteqP; split => [r /ltr_add_invr [l] | r [k] _]; last exact: lt_trans.

apply/seteqP; split => [r /ltr_add_invr [l] | r [k] _]; last exact: lt_trans.

to make this line fit within 80 chars.

t6s · 2026-01-26T05:53:37Z

theories/probability.v

+  apply/esym/measure_bigcup => //=.
+  move: (trivIset_comp (fun r => X @^-1` [set r]) q_inj); rewrite /comp => ->.


Suggested change

apply/esym/measure_bigcup => //=.

move: (trivIset_comp (fun r => X @^-1` [set r]) q_inj); rewrite /comp => ->.

rewrite measure_bigcup// (trivIset_comp (fun r => X @^-1` [set r]))//.

t6s · 2026-01-26T05:59:53Z

theories/probability.v

+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: (pselect ([set h k | k in S] r)) => [rS | nrS].


I would use asboolP instead of pselect to avoid an extra of parentheses:

case/asboolP: ([set h k | k in S] r) => [rS | nrS].

But honestly I'm not sure which is more idiomatic.

t6s · 2026-01-26T06:16:06Z

theories/probability.v

+apply: (eq_measurable_fun sfun) => [r _|].
+  case: (pselect ([set h k | k in S] r)) => [rS | nrS].
+  - pose kr := (pinv S h r).
+    have neqh k : in_set S k && (k != kr) -> r != h k.


Suggested change

have neqh k : in_set S k && (k != kr) -> r != h k.

have neqh k : (k \in S) && (k != kr) -> r != h k.

t6s · 2026-01-26T06:28:23Z

theories/probability.v

+    have ->: (r == h k) = false; rewrite ?mulr0// -eq_opE eqbF_neg; apply/negP.
+    apply/contra_not/nrS; rewrite eq_opE => ->.


Suggested change

have ->: (r == h k) = false; rewrite ?mulr0// -eq_opE eqbF_neg; apply/negP.

apply/contra_not/nrS; rewrite eq_opE => ->.

suff ->: (r == h k) = false by rewrite mulr0.

apply/negbTE/eqP/contra_not/nrS => ->.

t6s · 2026-01-26T06:29:10Z

theories/probability.v

+    rewrite indicE in_set1_eq.
+    have ->: (r == h k) = false; rewrite ?mulr0// -eq_opE eqbF_neg; apply/negP.
+    apply/contra_not/nrS; rewrite eq_opE => ->.
+    by exists k; rewrite -?(in_setE S k).


Suggested change

by exists k; rewrite -?(in_setE S k).

by exists k => //; rewrite -(in_setE S k).

t6s · 2026-01-26T06:36:42Z

classical/classical_sets.v


 #[global] Hint Resolve nat_nonempty : core.

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


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

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$

Yosuke-Ito-345 · 2026-01-27T12:02:30Z

@t6s
Thank you for the review.
I incorporated your feedback into the proof.
I'm going to replace the lemma in_set1 with in_set1_eq in another pull request.

Yosuke-Ito-345 · 2026-01-27T12:11:05Z

This is an unexpected failure.
The stable version of mathcomp appears to be unchanged since the last pull request.
Do I need to install the development version of mathcomp?
(In my experience, mathcomp-devel is fragile and often fails to compile.)

t6s · 2026-01-28T00:42:43Z

The CI failure looks strange and irrelevant to this PR.

t6s · 2026-01-28T03:30:18Z

I set up a local env with coq 8.20 and mathcomp 2.4.0, but could not reproduce the error.

Yosuke-Ito-345 · 2026-01-28T08:21:32Z

@t6s
Thank you for looking into this error.
For now, I leave the pull request as it is.

pmf measurable

7b7f690

affeldt-aist mentioned this pull request Jan 22, 2026

Split probability.v into a directory probability_theory #1808

Open

t6s approved these changes Jan 26, 2026

View reviewed changes

Yosuke-Ito-345 added 2 commits January 27, 2026 20:47

fix proof

a958a9d

modify changelog

a004013

	rewrite seteqP; split => [r /ltr_add_invr [l] \| r [k] _]; last exact: lt_trans.
	apply/seteqP; split => [r /ltr_add_invr [l] \| r [k] _]; last exact: lt_trans.

		apply/esym/measure_bigcup => //=.
		move: (trivIset_comp (fun r => X @^-1` [set r]) q_inj); rewrite /comp => ->.

	apply/esym/measure_bigcup => //=.
	move: (trivIset_comp (fun r => X @^-1` [set r]) q_inj); rewrite /comp => ->.
	rewrite measure_bigcup// (trivIset_comp (fun r => X @^-1` [set r]))//.

	have neqh k : in_set S k && (k != kr) -> r != h k.
	have neqh k : (k \in S) && (k != kr) -> r != h k.

		have ->: (r == h k) = false; rewrite ?mulr0// -eq_opE eqbF_neg; apply/negP.
		apply/contra_not/nrS; rewrite eq_opE => ->.

	by exists k; rewrite -?(in_setE S k).
	by exists k => //; rewrite -(in_setE S k).


		#[global] Hint Resolve nat_nonempty : core.

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

Add lemma pmf_measurable #1827

Are you sure you want to change the base?

Add lemma pmf_measurable #1827

Uh oh!

Conversation

Yosuke-Ito-345 commented Jan 20, 2026

Motivation for this change

Checklist

Merge policy

Reminder to reviewers

Uh oh!

Yosuke-Ito-345 commented Jan 20, 2026

Uh oh!

t6s left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Yosuke-Ito-345 commented Jan 27, 2026

Uh oh!

Yosuke-Ito-345 commented Jan 27, 2026

Uh oh!

t6s commented Jan 28, 2026

Uh oh!

t6s commented Jan 28, 2026

Uh oh!

Yosuke-Ito-345 commented Jan 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Add lemma `pmf_measurable` #1827

Add lemma `pmf_measurable` #1827