[isabelle] Mean value theorem for has_vector_derivative


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?

Alex Hicks

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