Email Gateway (Aug 22 2022 at 13:40): Email Gateway (Aug 22 2022 at 13:40):From: "A.L. Hicks" <alh70@cam.ac.uk>
Hi,
For a step of a proof I'm working on I'd like to use "∀j∈{a .. b}. ∀l∈{j
.. b}. G j ≤ G l" where G has derivative g ≥ 0. The standard way to
prove this is using the mean value theorem which already exists in the
MVA/Derivative theory.
Unfortunately the mvt is formulated for has_derivative and I have to use
G has_vector_derivative g rather than has_derivative as G is defined to
be (%y. LBINT x=a..y. g x) and using has_derivative leads to a type
error ereal/real_normed_vector.
Should I just go back and prove the MVT for has_vector_derivative or is
there an easier way around this?
Cheers,
Alex Hicks
Email Gateway (Aug 22 2022 at 13:43):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Alex,
The vector derivative is essentially the derivative, only that instead
of a linear function as derivative we only take a vector f' and the
linear function is the scalar multiplication with the vector f':
has_vector_derivative_def:
(f has_vector_derivative f') F <-->
(f has_derivative (λx. x *⇩R f')) F
So you should have no problem with using mvt.
But another problem could be that LBINT x=a..y. g x uses ereal for a
and y. Is there the case that a = -infty or b = +infty in your example?
If not just fix a b to be real. Then Isabelle will add the necessary
coercions to LBINT and you should be able to use has_vector_derivative:
G == (%y::real. LBINT x=a..y. g x)
Does this help?
- Johannes
Last updated: Apr 27 2024 at 04:17 UTC