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!

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.

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.

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?

don't they already have those axioms for `R`

in MathComp analysis?

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))

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

Last updated: Feb 08 2023 at 04:04 UTC