Quelle  deriv_dot_prod.pvs   Sprache: PVS

deriv_dot_prod[T: TYPE FROM real, n: posnat ] : THEORY
BEGIN


  ASSUMING

    IMPORTING analysis@deriv_domain_def

    deriv_domain     : ASSUMPTION deriv_domain?[T]

    not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING


  IMPORTING analysis@derivatives[T],
            vectors@vectors[n], 
            deriv_real_vect_def[T,n],
            deriv_sigma[T]

  f, f1, f2, fp : VAR [T -> Vector[n]]
  x : VAR T
  u : VAR nzreal
  a,b : VAR real

  dot_prod_derivable  : LEMMA derivable?(f1, x) AND derivable?(f2, x)
                               IMPLIES derivable?(f1 * f2, x)


  deriv_dot_prod      : LEMMA derivable?(f1, x) AND derivable?(f2, x) IMPLIES
                         deriv(f1 * f2, x) = deriv(f1, x) * f2(x) 
                                             + deriv(f2, x) * f1(x)


END deriv_dot_prod