Feature esum psum esum only

[affeldt-aist]

Motivation for this change

closes #1954

This PR intends to extract the reusable part of PR #1954

• new lemmas about esum
• removal of fpos and fneg (superseded by funrpos and funrneg)

TODO: completed (?)

• some scripts still need to be linted
• some lemmas are wrongly named
• ome lemmas are not in the right files

fyi: @lyonel2017 @strub

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]

@t6s I am pinging you because this PR changes the definition of esum, I thought you may want to know

[affeldt-aist]

@lyonel2017 @strub rebased

[t6s]

It looks like there are several chunks of changes contained in this PR, making it difficult to review it at once. Can you provide a bit more detailed description of intention for each of them? For example, which lemmas do you consider are important?

[affeldt-aist]

It looks like there are several chunks of changes contained in this PR, making it difficult to review it at once.
Can you provide a bit more detailed description of intention for each of them?
For example, which lemmas do you consider are important?

This is maybe for @lyonel2017 and @strub to say because this PR is used to develop another one.

From my viewpoint, the main change is the definition of esum which has become:

Definition esum S f := pos_esum S f^\+ - pos_esum S f^\-.

Before that, it was only the positive part.

[lyonel2017]

This is maybe for @lyonel2017 and @strub to say because this PR is used to develop another one.

I started porting the distr.v file from experimental_real to use esum. The idea is to better integrate the result present in experimental_reals into mathcomp-analysis. The current status is available here counting_distr.v (the branch is not up to date with this PR). For me all the changes present in this PR are required for the porting.

[t6s]

Local Notation fsum f :=
  (fun (J : {fset T}) => \sum_(x : J) `|f (val x)|).

Definition psum (f : T -> R) : R :=
  let S := range (fsum f) in
  if `[<summable f>] then sup S else 0.

I am afraid I did not understand what "ticked" means here, but the above code using image works.
(range f is a notation for (f @` [set: _])%classic)

[t6s]

(oops, this line does not belong to this PR)

[t6s]

Noting that esum has a very similar definition to sum, the following proof strategy is also possible:
discard the negative part of esum, and show PosEsum.pos_esum and psum are equal.

An attempt is as follows, but resulted in a longer proof:

Lemma ge0_funenegET :
  forall [T : Type] [R : realDomainType] [f : T -> \bar R],
  (forall x : T, (0%R <= f x)%E) -> f^\-%E = cst 0.
Proof.
move=> ? ? ? H; apply/funext => ?.
have ->// := @ge0_funenegE _ _ setT.
by rewrite mem_set.
Qed.

Lemma ge0_funrposET :
  forall [T : Type] [R : realDomainType] [f : T -> R],
    (forall x : T, 0 <= f x) -> f^\+ = f.
Proof.
move=> ? ? ? H; apply/funext => ?.
have ->// := @ge0_funrposE _ _ setT.
by rewrite mem_set.
Qed.

Lemma fsetsTE (T : choiceType) : fsets [set: T] = finite_set.
Proof. by apply/funext=> ?; apply/propext; split => // -[]. Qed.

Lemma exists_fsetE (T : choiceType) (P : {fset T} -> Prop) :
  (exists J : {fset T}, P J) = (exists2 J : set T, finite_set J & P (fset_set J)).
Proof.
apply/propext; split.
  by case=> J ?; exists [set` J]%classic => //; rewrite set_fsetK.
by case=> J ? ?; exists (fset_set J).
Qed.

Lemma exists_finite_setE (T : choiceType) (P : set T -> Prop) :
  (exists2 J : set T, finite_set J & P J) = (exists J : {fset T}, P [set` J]%classic).
Proof.
rewrite exists_fsetE; apply/propext; split => -[] J ?.
  by move=> ?; exists J => //; rewrite fset_setK.
by rewrite fset_setK// => ?; exists J.
Qed.

Lemma esymE (T : Type) (x y : T) : (x = y) = (y = x).
Proof. by apply/propext; split => /esym. Qed.

Lemma esum_psum {R : realType} {T : choiceType} (f : T -> R) :
    (forall i, 0 <= f i) -> summable f ->
  \esum_(x in [set: T]) (f x)%:E = (psum f)%:E.
Proof.
move=> f0 h.
rewrite /esum ge0_funenegET// [X in (_ - X)%E]PosEsum.pos_esum1// sube0.
rewrite /PosEsum.pos_esum fsetsTE.
rewrite /psum/=; case:asboolP => // _.
set S := (S in sup S).
have S_has_ubound : has_ubound S.
  by case: h => M HM; exists M => ?/= [] J ->; exact: HM.
  (* summable f -> has_ubound S; (S in the definition of psum) *)
have S_nonempty : (S !=set0)%classic.
  by exists 0, fset0; rewrite big1// => i; have := fsvalP i.
  (* S always has the sum over the emptyset as its elements *)
rewrite -ereal_sup_EFin; [exact: S_has_ubound | exact: S_nonempty |].
congr ereal_sup.
under eq_imagel do rewrite fsbig_finite//= funerpos/= sumEFin.
rewrite -[LHS]image_comp; congr image.
rewrite /S; apply: funext=> x/=.
rewrite exists_finite_setE; congr ex; apply/funext => J.
rewrite [LHS]esymE; congr eq.
rewrite -(big_seq_fsetE _ _ xpredT (Num.norm \o f))/= set_fsetK.
apply: eq_bigr => ? _.
by rewrite ger0_norm// ge0_funrposET.
Qed.

[t6s]

Further refactored; this ge0_psumEpos_esum can also be used to shorten esumEsum.

Lemma ge0_psumEpos_esum {R : realType} {T : choiceType} (f : T -> R) :
  (forall i, 0 <= f i) -> summable f ->
  (psum f)%:E = PosEsum.pos_esum [set: T] (EFin \o f).
Proof.
move=> f0 h.
rewrite /psum/=; case: asboolP => // _.
rewrite /PosEsum.pos_esum fsetsTE.
set S := (S in sup S).
have S_has_ubound : has_ubound S.
  by case: h => M HM; exists M => ?/= [] J ->; exact: HM.
  (* summable f -> has_ubound S; (S in the definition of psum) *)
have S_nonempty : (S !=set0)%classic.
  by exists 0, fset0; rewrite big1// => i; have := fsvalP i.
  (* S always has the sum over the emptyset as its elements *)
rewrite -ereal_sup_EFin; [exact: S_has_ubound | exact: S_nonempty |].
congr ereal_sup.
under [RHS]eq_imagel do rewrite fsbig_finite//= sumEFin.
rewrite -[RHS]image_comp; congr image.
rewrite /S; apply: funext=> x/=.
rewrite exists_finite_setE; congr ex; apply/funext => J.
rewrite [LHS]esymE; congr eq.
rewrite -(big_seq_fsetE _ _ xpredT (Num.norm \o f))/= set_fsetK.
apply: eq_bigr => ? _.
by rewrite ger0_norm.
Qed.

Lemma esum_psum {R : realType} {T : choiceType} (f : T -> R) :
    (forall i, 0 <= f i) -> summable f ->
  \esum_(x in [set: T]) (f x)%:E = (psum f)%:E.
Proof.
move=> f0 h.
rewrite /esum ge0_funenegET// [X in (_ - X)%E]PosEsum.pos_esum1// sube0.
by rewrite psumEpos_esum// funerpos ge0_funrposET.
Qed.