A.L. Hicks

2016-08-05 14:29:49 UTC

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

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