Add lemma le0_expectation_cdf

[Yosuke-Ito-345]

Motivation for this change

Add lemma le0_expectation_cdf, which is the counterpart of lemma ge0_expectation_ccdf.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
  N.B. I created CHANGELOG_UNRELEASED_new.md because the current CHANGELOG_UNRELEASED.md appeared to be old.

• 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]

@affeldt-aist @t6s
I would appreciate your review. m(. .)m

[t6s]

I quickly checked the changes and added a few comments. I will further look into the proofs of two main additions.

[t6s]

I have further added a few minor suggestions, but the code now generally looks good.

[t6s]

Reviewing the proofs, I experimented generalizing cdf to

Definition gen_cdf d (T : measurableType d) (R : realType) (P : probability T R)
  (X : {RV P >-> R}) b (r : R) := distribution P X [set` Interval -oo%O (BSide b r)].

The current proofs seem to work without changes at many steps.

[Yosuke-Ito-345]

@t6s
Thank you for the review. Let me clarify your suggestion.
Is your idea to replace the definition of cdf to gen_cdf? If so, I will try to replace proofs in the sections cumulative_distribution_function, cdf_of_lebesgue_stieltjes_measure, lebesgue_stieltjes_measure_of_cdf and tail_expectation_formula. Maybe I should try to generalize ccdf in accordance with gen_cdf.

[t6s]

@Yosuke-Ito-345 My last comment was not meant to be a clear suggestion, but a naive report on my experiment.
I am not convinced enough because my proof attempt is not completed (you can see a broken wip at t6s@21868b3 ).

This attempt may simplify the proofs and save lines of code, and then ccdf should also be generalized.
The cdf and ccdf would be defined by specializing gen_cdf, gen_ccdf.

[affeldt-aist]

I made a first pass, I will take a look at naming later

here are a few comments:

• as a general rule, we avoid named hypotheses that are not explicitly used
  in the statement; it is often better to help reading and to detect more easily
  for example when they become useless (that does not really apply here, though)
• use a type contraint instead of the T2 argument of pushforward
  because the name of T2 can change in the future
• ge0_integral_pushforwardN is not shorter but makes appear a
  potentially useful lemma that is maybe lacking in MathComp
• the suffix _subproof usually indicates proofs that are not meant
  to be exported to the user (max_mfun_subproof should not have been a Lemma
  but it was because it was used in simple_functions.v to circumvent
  an HB limitation that has been lifted since---apparently...)
• when setT appears in statements, it is often better to use the notation [set: _]
  becomes the type provides information
• proofs inside le0_expectation_cdf are a bit shorter if one uses
  preimage's instead of set's defined by comprehension
• it looks like a lemma akin to opp_preimage_itvbndy were called for

[affeldt-aist]

PS: There are maybe more symmetries/simplifications to discover with a better user of preimage or generalizations to generic intervals but this is not requirement to merge the PR imo

[affeldt-aist]

(oops, I haven't figured out yet the CI errors...)

[Yosuke-Ito-345]

According to the contribution guide, shouldn't we add - in the first two subgoals?

- by rewrite pmf0NP; exact: measurableC.
- by move=> x _; rewrite lee_fin pmf_ge0.

[affeldt-aist]

This is indeed what is written but we rarely apply this rule in MathComp-Analysis.
For example, when there are two technical subgoals that are generated and that these subgoals are so simple that they can be proved with one line and that morally they should be automatically discharged, we often write:

rewrite tactic1; last 2 first.
  by tactic2.
  by tactic3
rest_of_the_proof.

I guess that this is because the last 2 first and the leading by tactical and/or the coloring are enough indications to tell the reader "this is not fundamental, skip on a cursory reading", and also because that kind of situations appears less often in MathComp than in MathComp-Analysis (where we are quickly bothered by measurability/derivability/continuity/etc. subgoals).

Of course, it is fine to apply the "official" rule. Maybe we should propose an amendment to the contribution guide. What do you think? (@CohenCyril ?)

PS: Loosely connected topic: it is very likely that in a near future the default order of generation of subgoals will change when rewriting, and that measurability/derivability/continuity/etc. subgoals will be handled more automatically (in a bit more distant future). That could impact style.

[Yosuke-Ito-345]

Thank you for the detail explanation. Now I understand the policy, I do not require to add - in this proof.
Personally, I think this policy should be written down somewhere. I support proposing an amendment to the contribution guide.

[affeldt-aist]

I think I figured out the CI problem. This was specific to the dev version of Rocq, the behavior of simpl has slightly changed so that measurability of R disappeared and caused a type mismatch.
I have also made some small generalizations so that the proof of le0_expectation_cdf becomes less unnatural.
I am afraid you suffered a bit because of not general enough lemmas.

[affeldt-aist]

Since the (large) inequality that was on the right-hand side has disappears in favor of preimage maybe ge0_expectation_preimage is a bit more appropriate now.

[Yosuke-Ito-345]

Yes, I agree with you on changing ge0_expectation_prob_ge to ge0_expectation_preimage.

[affeldt-aist]

(CI should be fixed now, with the last commit)

[affeldt-aist]

pushforward does not appear in the statement so maybe it'd better not appear in the name.
By the way, this is a variant of ge0_integration_by_substitutionNy in ftc.v (fyi: @IshiguroYoshihiro) (maybe even a strict generalization provided the constant bound is generalized).
I'd like to give a bit more thought to naming, generalization, and potentially trying to use the general version when possible to see what can be gained in other files.

[affeldt-aist]

No obvious generalization, I propose to go with the name ge0_integration_by_substitution0 which is a bit long but more uniform with the similar lemmas in ftc.v: by choosing this name, when somebody searches for lemmas with the substring "substitution", they might find this along the others and maybe benefit from the weaker assumption.

[Yosuke-Ito-345]

I agree with your proposal.
By the way, I am considering formalizing the substitution formula for the Lebesgue integral in which the continuity of the integrand is not assumed. In fact, the integrand only needs to be measurable.
I think it is not easy and takes time, so I will send another pull request.

[affeldt-aist]

That would be great. By the way, @IshiguroYoshihiro knows best about these lemmas.

[affeldt-aist]

Thank you very much for the contribution and for your patience during the conversation!

[affeldt-aist]

We ll merge after fixing the changelog