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: Mar 29 2024 at 07:01 UTC