## Stream: math-comp users

### Topic: fold property in a sum using bigop

#### Dubravka Kutlesic (Nov 07 2021 at 16:25):

Hello, I would like to prove that sum of increasing function increases. I proved the following lemmas:
1)

Lemma sum_of_increasing_is_increasing (f g : R -> Rbar) :
increasing f /\ increasing g -> increasing (sum_of_functions f g).


2)

Lemma increasing_plus_0_is_increasing (f : R -> Rbar) (r : R) :
increasing f -> increasing (fun x => Rbar_plus (f x) (Finite 0)).


How to prove something like this or anything like this in more elegant form:

Lemma sum_of_increasing_increases (functions : list (R -> Rbar)):
(forall f, List.In f functions -> increasing f)->
increasing (fun x => \big[Rbar_plus/Finite 0]_(0 <= i < length functions) (List.nth i functions (deltaFunction 0)) x).


Thanks a lot!

#### Ana de Almeida Borges (Nov 07 2021 at 19:54):

Looks like induction on functions should work. I guess you are asking about the Coq/MathComp technicalities. First of all, if you are using bigop it would make sense to use seq as well, and your lemma can be written in this simpler form:

Lemma sum_of_increasing_increases (functions : seq (R -> Rbar)):
{in functions, forall f, increasing f} ->
increasing (fun x => \big[Rbar_plus/Finite 0]_(f <- functions) f x).


The lemmas big_cons and big_nil ought to be helpful.

{in X, forall x, P x} is notation for forall x, x \in X -> P x

Note that I haven't tested my code, or tried to prove the lemma. If you'd like more help please give enough context to compile the file, and possibly show your progress.

#### Christian Doczkal (Nov 08 2021 at 09:47):

Note that x \in _ requires x to have a type with an eqType structure, which is not the case for the function type R -> Rbar unless one adds a bunch of axioms. Indeed, proper support for non-decidable list membership has been on the to-do list for a long time.

#### Dubravka Kutlesic (Nov 08 2021 at 13:41):

Thank you very much for the answers! Will it be easier in this case to do it without mathcomp or to add the axioms for eqType?

#### Karl Palmskog (Nov 08 2021 at 13:44):

don't they already have those axioms for R in MathComp analysis?

#### Pierre Roux (Nov 08 2021 at 14:17):

MathComp canonical instances for stdlib's R should be in Rstruct.v while Rbar can be found in ereal.v (eqType on functions would still require some axioms though (maybe look in boolp.v))

#### Notification Bot (Nov 10 2021 at 17:29):

This topic was moved by Karl Palmskog to #math-comp analysis > ereals and Rbar

Last updated: Jul 25 2024 at 15:02 UTC