Add lemma le0_expectation_cdf#1847
Conversation
|
@affeldt-aist @t6s |
t6s
left a comment
t6s
left a comment
There was a problem hiding this comment.
I quickly checked the changes and added a few comments. I will further look into the proofs of two main additions.
|
|
||
| HB.instance Definition _ f g := min_mfun_subproof f g. | ||
|
|
||
| Definition min_mfun f g : {mfun aT >-> _} := f \min g. |
There was a problem hiding this comment.
min_mfun should be added to the header doc.
|
|
||
| Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. | ||
|
|
||
| Lemma lebesgue_measure_oppr A (mA : measurable A) : |
There was a problem hiding this comment.
I suggest renaming this to lebesgue_measureN.
| - by rewrite set_itv_ge ?wlength0// bnd_simp -leNgt. | ||
| Qed. | ||
|
|
||
| Lemma ge0_integral_oppr (f : R -> \bar R) |
There was a problem hiding this comment.
I suggest ge0_integral_pushforwardN.
| by apply: eq_set => r; rewrite in_itv/= s_ge0. | ||
| Qed. | ||
|
|
||
| Lemma ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> |
There was a problem hiding this comment.
What about giving a name to this integrand?
It should be equal to the "closed version" of ccdf.
Definition ccdf P X r := distribution P X `]r, +oo[.
Definition this_integrand P X r := distribution P X `[r, +oo[.
(However I myself do not come up with a good name.)
There was a problem hiding this comment.
This is only an auxiliary lemma for the subsequent lemma le0_expectation_cdf.
If I should not take this as an independent lemma, I would incorporate this into the proof of the lemma le0_expectation_cdf.
There was a problem hiding this comment.
Keeping this proof independent would contribute to the readability.
You can do Local Lemma ge0_expectation_prob_ge or Let ge0_expecation_prob_ge, so that
this will not be exported.
There was a problem hiding this comment.
All right. I changed this Lemma to Let.
Thank you for the suggestion.
t6s
left a comment
t6s
left a comment
There was a problem hiding this comment.
I have further added a few minor suggestions, but the code now generally looks good.
| Context {d} {T : measurableType d} {R : realType}. | ||
| Variables (P : probability T R). |
There was a problem hiding this comment.
| Context {d} {T : measurableType d} {R : realType}. | |
| Variables (P : probability T R). | |
| Context {d} {T : measurableType d} {R : realType} (P : probability T R). |
| + definition `min_mfun` | ||
|
|
||
| - in random_variable.v | ||
| + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, `ge0_expectation_prob_ge`, `le0_expectation_cdf` |
There was a problem hiding this comment.
| + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, `ge0_expectation_prob_ge`, `le0_expectation_cdf` | |
| + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, | |
| `ge0_expectation_prob_ge`, `le0_expectation_cdf` |
|
Reviewing the proofs, I experimented generalizing The current proofs seem to work without changes at many steps. |
|
@t6s |
|
@Yosuke-Ito-345 My last comment was not meant to be a clear suggestion, but a naive report on my experiment. This attempt may simplify the proofs and save lines of code, and then |
2 participants
Motivation for this change
Add lemma
le0_expectation_cdf, which is the counterpart of lemmage0_expectation_ccdf.Checklist
added corresponding entries in
CHANGELOG_UNRELEASED.mdN.B. I created
CHANGELOG_UNRELEASED_new.mdbecause the currentCHANGELOG_UNRELEASED.mdappeared to be old.added corresponding documentation in the headers
Reference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers