Theory GradientDeriv

header {* Gradient Derivatives *}

theory GradientDeriv
imports InnerProduct FrechetDeriv
begin

subsection {* Gradient Derivative *}

definition
  gderiv ::
  "['a::real_inner => real, 'a, 'a] => bool"
          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
  "GDERIV f x :> D = FDERIV f x :> (λh. inner h D)"

lemma deriv_fderiv: "DERIV f x :> D = FDERIV f x :> (λh. h * D)"
  by (simp only: deriv_def field_fderiv_def)

lemma gderiv_deriv [simp]: "GDERIV f x :> D = DERIV f x :> D"
  by (simp only: gderiv_def deriv_fderiv inner_real_def)

lemma GDERIV_DERIV_compose:
    "[|GDERIV f x :> D; DERIV g (f x) :> E|]
     ==> GDERIV (λx. g (f x)) x :> scaleR E D"
  unfolding gderiv_def deriv_fderiv
  apply (drule (1) FDERIV_compose)
  apply (simp add: inner_scaleR_right mult_ac)
  done

lemma FDERIV_subst: "[|FDERIV f x :> D; D = E|] ==> FDERIV f x :> E"
  by simp

lemma GDERIV_subst: "[|GDERIV f x :> D; D = E|] ==> GDERIV f x :> E"
  by simp

lemma GDERIV_const: "GDERIV (λx. k) x :> 0"
  unfolding gderiv_def inner_right.zero by (rule FDERIV_const)

lemma GDERIV_add:
    "[|GDERIV f x :> D; GDERIV g x :> E|]
     ==> GDERIV (λx. f x + g x) x :> D + E"
  unfolding gderiv_def inner_right.add by (rule FDERIV_add)

lemma GDERIV_minus:
    "GDERIV f x :> D ==> GDERIV (λx. - f x) x :> - D"
  unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)

lemma GDERIV_diff:
    "[|GDERIV f x :> D; GDERIV g x :> E|]
     ==> GDERIV (λx. f x - g x) x :> D - E"
  unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)

lemma GDERIV_scaleR:
    "[|DERIV f x :> D; GDERIV g x :> E|]
     ==> GDERIV (λx. scaleR (f x) (g x)) x
      :> (scaleR (f x) E + scaleR D (g x))"
  unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
  apply (rule FDERIV_subst)
  apply (erule (1) scaleR.FDERIV)
  apply (simp add: mult_ac)
  done

lemma GDERIV_mult:
    "[|GDERIV f x :> D; GDERIV g x :> E|]
     ==> GDERIV (λx. f x * g x) x :> scaleR (f x) E + scaleR (g x) D"
  unfolding gderiv_def
  apply (rule FDERIV_subst)
  apply (erule (1) FDERIV_mult)
  apply (simp add: inner_distrib inner_scaleR mult_ac)
  done

lemma GDERIV_inverse:
    "[|GDERIV f x :> D; f x ≠ 0|]
     ==> GDERIV (λx. inverse (f x)) x :> - (inverse (f x))² *R D"
  apply (erule GDERIV_DERIV_compose)
  apply (erule DERIV_inverse [folded numeral_2_eq_2])
  done

lemma GDERIV_norm: "x ≠ 0 ==> GDERIV (λx. norm x) x :> sgn x"
  apply (rule GDERIV_subst)
  apply (subst norm_eq_sqrt_inner)
  apply (rule GDERIV_DERIV_compose [where g=sqrt and D="scaleR 2 x"])
  apply (subst gderiv_def)
  apply (rule FDERIV_subst)
  apply (rule inner.FDERIV [OF FDERIV_ident FDERIV_ident])
  apply (simp add: expand_fun_eq inner_scaleR inner_commute)
  apply (rule DERIV_real_sqrt)
  apply (simp add: zero_less_inner_iff)
  apply (subst norm_eq_sqrt_inner [symmetric])
  apply (simp add: sgn_div_norm)
  done

lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def]

lemma isCont_sgn: "x ≠ 0 ==> isCont (λx. sgn x) x"
  unfolding sgn_div_norm
  by (simp add: isCont_scaleR isCont_inverse isCont_norm)

end