Theory Ordinary_Differential_Equations.Vector_Derivative_On

theory
  Vector_Derivative_On
imports
  "HOL-Analysis.Analysis"
begin

subsection ‹Vector derivative on a set›
  ― ‹TODO: also for the other derivatives?!›
  ― ‹TODO: move to repository and rewrite assumptions of common lemmas?›

definition
  has_vderiv_on :: "(real  'a::real_normed_vector)  (real  'a)  real set  bool"
  (infix "(has'_vderiv'_on)" 50)
where
  "(f has_vderiv_on f') S  (x  S. (f has_vector_derivative f' x) (at x within S))"

lemma has_vderiv_on_empty[intro, simp]: "(f has_vderiv_on f') {}"
  by (auto simp: has_vderiv_on_def)

lemma has_vderiv_on_subset:
  assumes "(f has_vderiv_on f') S"
  assumes "T  S"
  shows "(f has_vderiv_on f') T"
  by (meson assms(1) assms(2) contra_subsetD has_vderiv_on_def has_vector_derivative_within_subset)

lemma has_vderiv_on_compose:
  assumes "(f has_vderiv_on f') (g ` T)"
  assumes "(g has_vderiv_on g') T"
  shows "(f o g has_vderiv_on (λx. g' x *R f' (g x))) T"
  using assms
  unfolding has_vderiv_on_def
  by (auto intro!: vector_diff_chain_within)

lemma has_vderiv_on_open:
  assumes "open T"
  shows "(f has_vderiv_on f') T  (t  T. (f has_vector_derivative f' t) (at t))"
  by (auto simp: has_vderiv_on_def at_within_open[OF _ open T])

lemma has_vderiv_on_eq_rhs:― ‹TODO: integrate intro derivative_eq_intros›
  "(f has_vderiv_on g') T  (x. x  T  g' x = f' x)  (f has_vderiv_on f') T"
  by (auto simp: has_vderiv_on_def)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
  shows has_vderiv_on_id: "((λx. x) has_vderiv_on (λx. 1)) T"
    and has_vderiv_on_const: "((λx. c) has_vderiv_on (λx. 0)) T"
  by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
  fixes f::"real  'a::real_normed_vector"
  assumes "(f has_vderiv_on f') T"
  shows has_vderiv_on_uminus: "((λx. - f x) has_vderiv_on (λx. - f' x)) T"
  using assms
  by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
  fixes f g::"real  'a::real_normed_vector"
  assumes "(f has_vderiv_on f') T"
  assumes "(g has_vderiv_on g') T"
  shows has_vderiv_on_add: "((λx. f x + g x) has_vderiv_on (λx. f' x + g' x)) T"
   and has_vderiv_on_diff: "((λx. f x - g x) has_vderiv_on (λx. f' x - g' x)) T"
  using assms
  by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
  fixes f::"real  real" and g::"real  'a::real_normed_vector"
  assumes "(f has_vderiv_on f') T"
  assumes "(g has_vderiv_on g') T"
  shows has_vderiv_on_scaleR: "((λx. f x *R g x) has_vderiv_on (λx. f x *R g' x + f' x *R g x)) T"
  using assms
  by (auto simp: has_vderiv_on_def has_real_derivative_iff_has_vector_derivative
    intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
  fixes f g::"real  'a::real_normed_algebra"
  assumes "(f has_vderiv_on f') T"
  assumes "(g has_vderiv_on g') T"
  shows has_vderiv_on_mult: "((λx. f x * g x) has_vderiv_on (λx. f x * g' x + f' x * g x)) T"
  using assms
  by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma has_vderiv_on_ln[THEN has_vderiv_on_eq_rhs, derivative_intros]:
  fixes g::"real  real"
  assumes "x. x  s  0 < g x"
  assumes "(g has_vderiv_on g') s"
  shows "((λx. ln (g x)) has_vderiv_on (λx. g' x / g x)) s"
  using assms
  unfolding has_vderiv_on_def
  by (auto simp: has_vderiv_on_def has_real_derivative_iff_has_vector_derivative[symmetric]
    intro!: derivative_eq_intros)


lemma fundamental_theorem_of_calculus':
  fixes f :: "real  'a::banach"
  shows "a  b  (f has_vderiv_on f') {a .. b}  (f' has_integral (f b - f a)) {a .. b}"
  by (auto intro!: fundamental_theorem_of_calculus simp: has_vderiv_on_def)

lemma has_vderiv_on_If:
  assumes "U = S  T"
  assumes "(f has_vderiv_on f') (S  (closure T  closure S))"
  assumes "(g has_vderiv_on g') (T  (closure T  closure S))"
  assumes "x. x  closure T  x  closure S  f x = g x"
  assumes "x. x  closure T  x  closure S  f' x = g' x"
  shows "((λt. if t  S then f t else g t) has_vderiv_on (λt. if t  S then f' t else g' t)) U"
  using assms
  by (auto simp: has_vderiv_on_def ac_simps
      intro!: has_vector_derivative_If_within_closures
      split del: if_split)

lemma mvt_very_simple_closed_segmentE:
  fixes f::"realreal"
  assumes "(f has_vderiv_on f') (closed_segment a b)"
  obtains y where "y  closed_segment a b"  "f b - f a = (b - a) * f' y"
proof cases
  assume "a  b"
  with mvt_very_simple[of a b f "λx i. i *R f' x"] assms
  obtain y where "y  closed_segment a b"  "f b - f a = (b - a) * f' y"
    by (auto simp: has_vector_derivative_def closed_segment_eq_real_ivl has_vderiv_on_def)
  thus ?thesis ..
next
  assume "¬ a  b"
  with mvt_very_simple[of b a f "λx i. i *R f' x"] assms
  obtain y where "y  closed_segment a b"  "f b - f a = (b - a) * f' y"
    by (force simp: has_vector_derivative_def has_vderiv_on_def closed_segment_eq_real_ivl algebra_simps)
  thus ?thesis ..
qed

lemma mvt_simple_closed_segmentE:
  fixes f::"realreal"
  assumes "(f has_vderiv_on f') (closed_segment a b)"
  assumes "a  b"
  obtains y where "y  open_segment a b"  "f b - f a = (b - a) * f' y"
proof cases
  assume "a  b"
  with assms have "a < b" by simp
  with mvt_simple[of a b f "λx i. i *R f' x"] assms
  obtain y where "y  open_segment a b"  "f b - f a = (b - a) * f' y"
    by (auto simp: has_vector_derivative_def closed_segment_eq_real_ivl has_vderiv_on_def
        open_segment_eq_real_ivl)
  thus ?thesis ..
next
  assume "¬ a  b"
  then have "b < a" by simp
  with mvt_simple[of b a f "λx i. i *R f' x"] assms
  obtain y where "y  open_segment a b"  "f b - f a = (b - a) * f' y"
    by (force simp: has_vector_derivative_def has_vderiv_on_def closed_segment_eq_real_ivl algebra_simps
      open_segment_eq_real_ivl)
  thus ?thesis ..
qed

lemma differentiable_bound_general_open_segment:
  fixes a :: "real"
    and b :: "real"
    and f :: "real  'a::real_normed_vector"
    and f' :: "real  'a"
  assumes "continuous_on (closed_segment a b) f"
  assumes "continuous_on (closed_segment a b) g"
    and "(f has_vderiv_on f') (open_segment a b)"
    and "(g has_vderiv_on g') (open_segment a b)"
    and "x. x  open_segment a b  norm (f' x)  g' x"
  shows "norm (f b - f a)  abs (g b - g a)"
proof -
  {
    assume "a = b"
    hence ?thesis by simp
  } moreover {
    assume "a < b"
    with assms
    have "continuous_on {a .. b} f"
      and "continuous_on {a .. b} g"
      and "x. x{a<..<b}  (f has_vector_derivative f' x) (at x)"
      and "x. x{a<..<b}  (g has_vector_derivative g' x) (at x)"
      and "x. x{a<..<b}  norm (f' x)  g' x"
      by (auto simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl has_vderiv_on_def
        at_within_open[where S="{a<..<b}"])
    from differentiable_bound_general[OF a < b this]
    have ?thesis by auto
  } moreover {
    assume "b < a"
    with assms
    have "continuous_on {b .. a} f"
      and "continuous_on {b .. a} g"
      and "x. x{b<..<a}  (f has_vector_derivative f' x) (at x)"
      and "x. x{b<..<a}  (g has_vector_derivative g' x) (at x)"
      and "x. x{b<..<a}  norm (f' x)  g' x"
      by (auto simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl has_vderiv_on_def
        at_within_open[where S="{b<..<a}"])
    from differentiable_bound_general[OF b < a this]
    have "norm (f a - f b)  g a - g b" by simp
    also have "  abs (g b - g a)" by simp
    finally have ?thesis by (simp add: norm_minus_commute)
  } ultimately show ?thesis by arith
qed

lemma has_vderiv_on_union:
  assumes "(f has_vderiv_on g) (s  closure s  closure t)"
  assumes "(f has_vderiv_on g) (t  closure s  closure t)"
  shows "(f has_vderiv_on g) (s  t)"
  unfolding has_vderiv_on_def
proof
  fix x assume "x  s  t"
  with has_vector_derivative_If_within_closures[of x s t "s  t" f g f g] assms
  show "(f has_vector_derivative g x) (at x within s  t)"
    by (auto simp: has_vderiv_on_def)
qed

lemma has_vderiv_on_union_closed:
  assumes "(f has_vderiv_on g) s"
  assumes "(f has_vderiv_on g) t"
  assumes "closed s" "closed t"
  shows "(f has_vderiv_on g) (s  t)"
  using has_vderiv_on_If[OF refl, of f g s t f g] assms
  by (auto simp: has_vderiv_on_subset)

lemma vderiv_on_continuous_on: "(f has_vderiv_on f') S  continuous_on S f"
  by (auto intro!: continuous_on_vector_derivative simp: has_vderiv_on_def)

lemma has_vderiv_on_cong[cong]:
  assumes "x. x  S  f x = g x"
  assumes "x. x  S  f' x = g' x"
  assumes "S = T"
  shows "(f has_vderiv_on f') S = (g has_vderiv_on g') T"
  using assms
  by (metis has_vector_derivative_transform has_vderiv_on_def)

lemma has_vderiv_eq:
  assumes "(f has_vderiv_on f') S"
  assumes "x. x  S  f x = g x"
  assumes "x. x  S  f' x = g' x"
  assumes "S = T"
  shows "(g has_vderiv_on g') T"
  using assms by simp

lemma has_vderiv_on_compose':
  assumes "(f has_vderiv_on f') (g ` T)"
  assumes "(g has_vderiv_on g') T"
  shows "((λx. f (g x)) has_vderiv_on (λx. g' x *R f' (g x))) T"
  using has_vderiv_on_compose[OF assms]
  by simp

lemma has_vderiv_on_compose2:
  assumes "(f has_vderiv_on f') S"
  assumes "(g has_vderiv_on g') T"
  assumes "t. t  T  g t  S"
  shows "((λx. f (g x)) has_vderiv_on (λx. g' x *R f' (g x))) T"
  using has_vderiv_on_compose[OF has_vderiv_on_subset[OF assms(1)] assms(2)] assms(3)
  by force

lemma has_vderiv_on_singleton: "(y has_vderiv_on y') {t0}"
  by (auto simp: has_vderiv_on_def has_vector_derivative_def has_derivative_within_singleton_iff
      bounded_linear_scaleR_left)

lemma
  has_vderiv_on_zero_constant:
  assumes "convex s"
  assumes "(f has_vderiv_on (λh. 0)) s"
  obtains c where "x. x  s  f x = c"
  using has_vector_derivative_zero_constant[of s f] assms
  by (auto simp: has_vderiv_on_def)

lemma bounded_vderiv_on_imp_lipschitz:
  assumes "(f has_vderiv_on f') X"
  assumes convex: "convex X"
  assumes "x. x  X  norm (f' x)  C" "0  C"
  shows "C-lipschitz_on X f"
  using assms
  by (auto simp: has_vderiv_on_def has_vector_derivative_def onorm_scaleR_left onorm_id
    intro!: bounded_derivative_imp_lipschitz[where f' = "λx d. d *R f' x"])

end