Re: [isabelle] type unification failed using an old lemma?



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


On 5 August 2016 at 15:24, A.L. Hicks <alh70 at cam.ac.uk> wrote:

> 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
>
>



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