Re: [isabelle] Mean value theorem for has_vector_derivative



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


Am Montag, den 04.07.2016, 14:56 +0100 schrieb A.L. Hicks:
> 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
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.