Stream: math-comp users

Topic: fold property in a sum using bigop


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Nov 08 2021 at 13:44):

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

view this post on Zulip 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))

view this post on Zulip Notification Bot (Nov 10 2021 at 17:29):

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


Last updated: Feb 08 2023 at 04:04 UTC