Email Gateway (Aug 22 2022 at 13:56): Email Gateway (Aug 22 2022 at 13:56):From: "A.L. Hicks" <alh70@cam.ac.uk>
Hi,
Sorry in advance if this is some trivial error on my part.
I'd like to use the lemma has_vector_derivative_mult in the HOL library
which reads:
"lemma has_vector_derivative_mult[derivative_intros]:
"(f has_vector_derivative f') (at x within s) ⟹ (g
has_vector_derivative g') (at x within s) ⟹
((λx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a ::
real_normed_algebra)) (at x within s)"
by (rule bounded_bilinear.has_vector_derivative[OF
bounded_bilinear_mult])"
However it seems that using a statement such as
have "((λx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a
:: real_normed_algebra)) (at x within {a .. b})"
leads to a standard type unification error:
Type unification failed: Clash of types "_ ⇒ _" and "real"
Type error in application: incompatible operand type
Operator: op * (f x) :: real ⇒ real
Operand: g' :: real ⇒ real
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "real"
Am I missing something or is the lemma itself flawed?
As an aside, there is a similar lemma for the has_derivative operator:
has_derivative_mult
which works for statements like
have "((%x. f x * g x) has_derivative (%y. f x * g' y + f' y * g x))
(at x within {a .. b})"
Say I have h=(%x. f x * g x), I can obtain h' such that h has_derivative
h but can't seem to define h' explicitly.
Thanks,
Alex Hicks
Email Gateway (Aug 22 2022 at 13:56):From: Mark Wassell <mpwassell@gmail.com>
Hi,
Something before your line
have "((λx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a ::
real_normed_algebra)) (at x within {a .. b})"
has "given" g' the type real ⇒ real
Have you perhaps said
(g has_derivative g') rather than (g has_vector_derivative g') ?
Mark
Last updated: Apr 19 2024 at 08:19 UTC