Prove some admitted lemmas in experimental_reals

[ethanlee515]

Motivation for this change

Prove three admitted lemmas in experimental_reals/realsum.v:

• psumB
• interchange_sup
• interchange_psum

Un-deprecate the following, as they no longer depend on unproven lemmas:

• dlet_dlet
• dmargin_dlet
• dlet_dmargin
• dfst_dswap
• dsnd_dswap
• dsndE
• pr_dlet

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

[affeldt-aist]

Excellent! Note that psumB was also proved in the meantime in https://github.com/math-comp/analysis/pull/1978 (under review). fyi @t6s @strub @lyonel2017

[lyonel2017]

Another way to prove interchange_psum is to use the lemmas esum_psum and exchange_esum. Here is an example:
https://github.com/lyonel2017/analysis/blob/a73e8162a88214015e8f9cd452104ceb15bb2f8c/experimental_reals/realsum.v#L1156. I think this proof could be shorter

[ethanlee515]

I've updated the proof of interchange_psum to use esum_psum and exchange_esum as suggested. I also noticed that my PR earlier changed the statement of interchange_sup by accident; I've changed it back.

[affeldt-aist]

What about the following for interchange_psum?
A bit shorter and more "primitive" (does not rely on esum.v).

Section PSumInterchange.
Context {R : realType} {X Y : choiceType}.

Let summable_pair_from_rows_psum (S : X -> Y -> R) :
    (forall x, summable (S x)) -> summable (PosSum.psum \o S) ->
  summable (fun xy => S xy.1 xy.2).
Proof.
move=> sumS sum_psumS.
exists (PosSum.psum (PosSum.psum \o S)) => J.
rewrite (big_fset_seq (fun xy => `|S xy.1 xy.2|))/=.
rewrite (partition_big_imfset _ fst J (fun xy => `|S xy.1 xy.2|))/=.
pose J1 := [fset xy.1 | xy in J]%fset.
have := gerfin_psum J1 sum_psumS.
rewrite (big_fset_seq (fun x => `|PosSum.psum (S x)|))/=.
apply: le_trans; apply: ler_sum => x _.
rewrite ger0_norm ?ge0_psum//.
pose F := [fset xy in J | xy.1 == x]%fset.
rewrite [leLHS](_ : _ = \sum_(xy <- F) `|S x xy.2|).
  by rewrite /F big_fset /=; apply: eq_bigr => xy /eqP ->.
rewrite -(big_map snd predT (fun y => `|S x y|)).
apply: gerfinseq_psum => //.
rewrite map_inj_in_uniq; last exact: uniq_fset_keys.
move=> [x1 y1] [x2 y2] /[!in_fset] /= /[!inE] /=.
by move=> /andP[_ /eqP ->] /andP[_ /eqP /= ->] ->.
Qed.

Lemma interchange_psum (S : X -> Y -> R) :
    (forall x, summable (S x)) -> summable (PosSum.psum \o S) ->
  PosSum.psum (PosSum.psum \o S) =
  PosSum.psum (fun y => PosSum.psum (S ^~ y)).
Proof.
move=> row_summable rows_summable.
pose P (xy : X * Y) := S xy.1 xy.2.
suff sumP : summable P.
  by rewrite -[LHS](psum_pair sumP)// [LHS](psum_pair_swap sumP).
apply: summable_pair_from_rows_psum.
- exact: row_summable.
- exact: eq_summable rows_summable.
Qed.

End PSumInterchange.

[affeldt-aist]

Though the many small lemmas by @lyonel2017 look worth having... :-/

[affeldt-aist]

In order to merge this PR quickly (because it is a progress and because the release of the next version is near---hopefully next week),
I propose the following:

• tell me whether you prefer the above proof script for interchange_psum
• make an issue for @lyonel2017 to later come up with a new proof using lemmas about esum and psum (the usefulness of which we can then discuss)

[ethanlee515]

ah, my bad, didn't know the changes to interchange_sup (i.e. use of range) was intended.

On the interchange_psum side, I feel I unfortunately know too little to have an informed opinion or strong preference one way or the other. I'm happy with anything that everyone else agrees on :)

[affeldt-aist]

ah, my bad, didn't know the changes to interchange_sup (i.e. use of range) was intended.

it was: we'd better use the existing notations when they exist

PS: closing the PR was unintentional

[ethanlee515]

Replaced the interchange_psum proof with the version above by @affeldt-aist. As for opening a new issue, I don't know if I'm the right person to coordinate this.