Theory FrechetDeriv

(*  Title       : FrechetDeriv.thy
    ID          : $Id$
    Author      : Brian Huffman, Portland State University
*)

header {* Frechet Derivative *}

theory FrechetDeriv
imports BoundedLinear
begin

definition
  fderiv ::
  "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'a => 'b] => bool"
    -- {* Frechet derivative: D is derivative of function f at x *}
          ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
  "FDERIV f x :> D = (bounded_linear D ∧
    (λh. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"

lemma FDERIV_I:
  "[|bounded_linear D; (λh. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0|]
   ==> FDERIV f x :> D"
by (simp add: fderiv_def)

lemma FDERIV_D:
  "FDERIV f x :> D ==> (λh. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0"
by (simp add: fderiv_def)

lemma FDERIV_bounded_linear: "FDERIV f x :> D ==> bounded_linear D"
by (simp add: fderiv_def)

lemma FDERIV_const: "FDERIV (λx. k) x :> (λh. 0)"
by (simp add: fderiv_def bounded_linear_zero)

lemma FDERIV_ident: "FDERIV (λx. x) x :> (λh. h)"
by (simp add: fderiv_def bounded_linear_ident)

subsection {* Addition *}

lemma norm_ratio_ineq:
  fixes x y :: "'a::real_normed_vector"
  fixes h :: "'b::real_normed_vector"
  shows "norm (x + y) / norm h ≤ norm x / norm h + norm y / norm h"
apply (rule ord_le_eq_trans)
apply (rule divide_right_mono)
apply (rule norm_triangle_ineq)
apply (rule norm_ge_zero)
apply (rule add_divide_distrib)
done

lemma FDERIV_add:
  assumes f: "FDERIV f x :> F"
  assumes g: "FDERIV g x :> G"
  shows "FDERIV (λx. f x + g x) x :> (λh. F h + G h)"
proof (rule FDERIV_I)
  show "bounded_linear (λh. F h + G h)"
    using f g by (intro bounded_linear_add FDERIV_bounded_linear)
next
  have f': "(λh. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
    using f by (rule FDERIV_D)
  have g': "(λh. norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
    using g by (rule FDERIV_D)
  have "(λh. norm (f (x + h) - f x - F h) / norm h
           + norm (g (x + h) - g x - G h) / norm h) -- 0 --> 0"
    using f' g' by (rule LIM_add_zero)
  thus "(λh. norm (f (x + h) + g (x + h) - (f x + g x) - (F h + G h))
           / norm h) -- 0 --> 0"
    apply (rule real_LIM_sandwich_zero)
     apply (simp add: divide_nonneg_pos)
    apply (simp only: add_diff_add)
    apply (rule norm_ratio_ineq)
    done
qed

subsection {* Subtraction *}

lemma FDERIV_minus:
  "FDERIV f x :> F ==> FDERIV (λx. - f x) x :> (λh. - F h)"
apply (rule FDERIV_I)
apply (rule bounded_linear_minus)
apply (erule FDERIV_bounded_linear)
apply (simp only: fderiv_def minus_diff_minus norm_minus_cancel)
done

lemma FDERIV_diff:
  "[|FDERIV f x :> F; FDERIV g x :> G|]
   ==> FDERIV (λx. f x - g x) x :> (λh. F h - G h)"
by (simp only: diff_minus FDERIV_add FDERIV_minus)

subsection {* Continuity *}

lemma FDERIV_isCont:
  assumes f: "FDERIV f x :> F"
  shows "isCont f x"
proof -
  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
  have "(λh. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
    using f by (rule FDERIV_D)
  hence "(λh. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
    by (intro LIM_mult_zero LIM_norm_zero LIM_ident)
  hence "(λh. norm (f (x + h) - f x - F h)) -- 0 --> 0"
    by (simp cong: LIM_cong)
  hence "(λh. f (x + h) - f x - F h) -- 0 --> 0"
    by (rule LIM_norm_zero_cancel)
  hence "(λh. f (x + h) - f x - F h + F h) -- 0 --> 0"
    by (intro LIM_add_zero F.LIM_zero LIM_ident)
  hence "(λh. f (x + h) - f x) -- 0 --> 0"
    by simp
  thus "isCont f x"
    unfolding isCont_iff by (rule LIM_zero_cancel)
qed

subsection {* Composition *}

lemma real_divide_cancel_lemma:
  fixes a b c :: "'a::{field,division_by_zero}"
  shows "(b = 0 ==> a = 0) ==> (a / b) * (b / c) = a / c"
  by simp

lemma FDERIV_compose:
  fixes f :: "'a::real_normed_vector => 'b::real_normed_vector"
  fixes g :: "'b::real_normed_vector => 'c::real_normed_vector"
  assumes f: "FDERIV f x :> F"
  assumes g: "FDERIV g (f x) :> G"
  shows "FDERIV (λx. g (f x)) x :> (λh. G (F h))"
proof (rule FDERIV_I)
  from FDERIV_bounded_linear [OF g] FDERIV_bounded_linear [OF f]
  show "bounded_linear (λh. G (F h))"
    by (rule bounded_linear_compose)
next
  let ?Rf = "λh. f (x + h) - f x - F h"
  let ?Rg = "λk. g (f x + k) - g (f x) - G k"
  let ?k = "λh. f (x + h) - f x"
  let ?Nf = "λh. norm (?Rf h) / norm h"
  let ?Ng = "λh. norm (?Rg (?k h)) / norm (?k h)"
  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
  from g interpret G: bounded_linear ["G"] by (rule FDERIV_bounded_linear)
  from F.bounded obtain kF where kF: "!!x. norm (F x) ≤ norm x * kF" by fast
  from G.bounded obtain kG where kG: "!!x. norm (G x) ≤ norm x * kG" by fast

  let ?fun2 = "λh. ?Nf h * kG + ?Ng h * (?Nf h + kF)"

  show "(λh. norm (g (f (x + h)) - g (f x) - G (F h)) / norm h) -- 0 --> 0"
  proof (rule real_LIM_sandwich_zero)
    have Nf: "?Nf -- 0 --> 0"
      using FDERIV_D [OF f] .

    have Ng1: "isCont (λk. norm (?Rg k) / norm k) 0"
      by (simp add: isCont_def FDERIV_D [OF g])
    have Ng2: "?k -- 0 --> 0"
      apply (rule LIM_zero)
      apply (fold isCont_iff)
      apply (rule FDERIV_isCont [OF f])
      done
    have Ng: "?Ng -- 0 --> 0"
      using isCont_LIM_compose [OF Ng1 Ng2] by simp

    have "(λh. ?Nf h * kG + ?Ng h * (?Nf h + kF))
           -- 0 --> 0 * kG + 0 * (0 + kF)"
      by (intro LIM_add LIM_mult LIM_const Nf Ng)
    thus "(λh. ?Nf h * kG + ?Ng h * (?Nf h + kF)) -- 0 --> 0"
      by simp
  next
    fix h::'a assume h: "h ≠ 0"
    thus "0 ≤ norm (g (f (x + h)) - g (f x) - G (F h)) / norm h"
      by (simp add: divide_nonneg_pos)
  next
    fix h::'a assume h: "h ≠ 0"
    have "g (f (x + h)) - g (f x) - G (F h) = G (?Rf h) + ?Rg (?k h)"
      by (simp add: G.diff)
    hence "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
           = norm (G (?Rf h) + ?Rg (?k h)) / norm h"
      by (rule arg_cong)
    also have "… ≤ norm (G (?Rf h)) / norm h + norm (?Rg (?k h)) / norm h"
      by (rule norm_ratio_ineq)
    also have "… ≤ ?Nf h * kG + ?Ng h * (?Nf h + kF)"
    proof (rule add_mono)
      show "norm (G (?Rf h)) / norm h ≤ ?Nf h * kG"
        apply (rule ord_le_eq_trans)
        apply (rule divide_right_mono [OF kG norm_ge_zero])
        apply simp
        done
    next
      have "norm (?Rg (?k h)) / norm h = ?Ng h * (norm (?k h) / norm h)"
        apply (rule real_divide_cancel_lemma [symmetric])
        apply (simp add: G.zero)
        done
      also have "… ≤ ?Ng h * (?Nf h + kF)"
      proof (rule mult_left_mono)
        have "norm (?k h) / norm h = norm (?Rf h + F h) / norm h"
          by simp
        also have "… ≤ ?Nf h + norm (F h) / norm h"
          by (rule norm_ratio_ineq)
        also have "… ≤ ?Nf h + kF"
          apply (rule add_left_mono)
          apply (subst pos_divide_le_eq, simp add: h)
          apply (subst mult_commute)
          apply (rule kF)
          done
        finally show "norm (?k h) / norm h ≤ ?Nf h + kF" .
      next
        show "0 ≤ ?Ng h"
        apply (case_tac "f (x + h) - f x = 0", simp)
        apply (rule divide_nonneg_pos [OF norm_ge_zero])
        apply simp
        done
      qed
      finally show "norm (?Rg (?k h)) / norm h ≤ ?Ng h * (?Nf h + kF)" .
    qed
    finally show "norm (g (f (x + h)) - g (f x) - G (F h)) / norm h
        ≤ ?Nf h * kG + ?Ng h * (?Nf h + kF)" .
  qed
qed

subsection {* Product Rule *}

lemma (in bounded_bilinear) FDERIV_lemma:
  "a' ** b' - a ** b - (a ** B + A ** b)
   = a ** (b' - b - B) + (a' - a - A) ** b' + A ** (b' - b)"
by (simp add: diff_left diff_right)

lemma (in bounded_bilinear) FDERIV:
  fixes x :: "'d::real_normed_vector"
  assumes f: "FDERIV f x :> F"
  assumes g: "FDERIV g x :> G"
  shows "FDERIV (λx. f x ** g x) x :> (λh. f x ** G h + F h ** g x)"
proof (rule FDERIV_I)
  show "bounded_linear (λh. f x ** G h + F h ** g x)"
    apply (rule bounded_linear_add)
    apply (rule bounded_linear_compose [OF bounded_linear_right])
    apply (rule FDERIV_bounded_linear [OF g])
    apply (rule bounded_linear_compose [OF bounded_linear_left])
    apply (rule FDERIV_bounded_linear [OF f])
    done
next
  from bounded_linear.bounded [OF FDERIV_bounded_linear [OF f]]
  obtain KF where norm_F: "!!x. norm (F x) ≤ norm x * KF" by fast

  from pos_bounded obtain K where K: "0 < K" and norm_prod:
    "!!a b. norm (a ** b) ≤ norm a * norm b * K" by fast

  let ?Rf = "λh. f (x + h) - f x - F h"
  let ?Rg = "λh. g (x + h) - g x - G h"

  let ?fun1 = "λh.
        norm (f x ** ?Rg h + ?Rf h ** g (x + h) + F h ** (g (x + h) - g x)) /
        norm h"

  let ?fun2 = "λh.
        norm (f x) * (norm (?Rg h) / norm h) * K +
        norm (?Rf h) / norm h * norm (g (x + h)) * K +
        KF * norm (g (x + h) - g x) * K"

  have "?fun1 -- 0 --> 0"
  proof (rule real_LIM_sandwich_zero)
    from f g isCont_iff [THEN iffD1, OF FDERIV_isCont [OF g]]
    have "?fun2 -- 0 -->
          norm (f x) * 0 * K + 0 * norm (g x) * K + KF * norm (0::'b) * K"
      by (intro LIM_add LIM_mult LIM_const LIM_norm LIM_zero FDERIV_D)
    thus "?fun2 -- 0 --> 0"
      by simp
  next
    fix h::'d assume "h ≠ 0"
    thus "0 ≤ ?fun1 h"
      by (simp add: divide_nonneg_pos)
  next
    fix h::'d assume "h ≠ 0"
    have "?fun1 h ≤ (norm (f x) * norm (?Rg h) * K +
         norm (?Rf h) * norm (g (x + h)) * K +
         norm h * KF * norm (g (x + h) - g x) * K) / norm h"
      by (intro
        divide_right_mono mult_mono'
        order_trans [OF norm_triangle_ineq add_mono]
        order_trans [OF norm_prod mult_right_mono]
        mult_nonneg_nonneg order_refl norm_ge_zero norm_F
        K [THEN order_less_imp_le]
      )
    also have "… = ?fun2 h"
      by (simp add: add_divide_distrib)
    finally show "?fun1 h ≤ ?fun2 h" .
  qed
  thus "(λh.
    norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x))
    / norm h) -- 0 --> 0"
    by (simp only: FDERIV_lemma)
qed

lemmas FDERIV_mult = mult.FDERIV

lemmas FDERIV_scaleR = scaleR.FDERIV

subsection {* Powers *}

lemma FDERIV_power_Suc:
  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
  shows "FDERIV (λx. x ^ Suc n) x :> (λh. (1 + of_nat n) * x ^ n * h)"
  apply (induct n)
  apply (simp add: power_Suc FDERIV_ident)
  apply (drule FDERIV_mult [OF FDERIV_ident])
  apply (simp only: of_nat_Suc left_distrib mult_1_left)
  apply (simp only: power_Suc right_distrib mult_ac add_ac)
  done

lemma FDERIV_power:
  fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
  shows "FDERIV (λx. x ^ n) x :> (λh. of_nat n * x ^ (n - 1) * h)"
  by (cases n, simp add: FDERIV_const, simp add: FDERIV_power_Suc)

subsection {* Inverse *}

lemma FDERIV_inverse:
  fixes x :: "'a::real_normed_div_algebra"
  assumes x: "x ≠ 0"
  shows "FDERIV inverse x :> (λh. - (inverse x * h * inverse x))"
        (is "FDERIV ?inv _ :> _")
proof (rule FDERIV_I)
  show "bounded_linear (λh. - (?inv x * h * ?inv x))"
    apply (rule bounded_linear_minus)
    apply (rule bounded_linear_mult_const)
    apply (rule bounded_linear_const_mult)
    apply (rule bounded_linear_ident)
    done
next
  show "(λh. norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h)
        -- 0 --> 0"
  proof (rule LIM_equal2)
    show "0 < norm x" using x by simp
  next
    fix h::'a
    assume 1: "h ≠ 0"
    assume "norm (h - 0) < norm x"
    hence "h ≠ -x" by clarsimp
    hence 2: "x + h ≠ 0"
      apply (rule contrapos_nn)
      apply (rule sym)
      apply (erule equals_zero_I)
      done
    show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
          = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
      apply (subst inverse_diff_inverse [OF 2 x])
      apply (subst minus_diff_minus)
      apply (subst norm_minus_cancel)
      apply (simp add: left_diff_distrib)
      done
  next
    show "(λh. norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h)
          -- 0 --> 0"
    proof (rule real_LIM_sandwich_zero)
      show "(λh. norm (?inv (x + h) - ?inv x) * norm (?inv x))
            -- 0 --> 0"
        apply (rule LIM_mult_left_zero)
        apply (rule LIM_norm_zero)
        apply (rule LIM_zero)
        apply (rule LIM_offset_zero)
        apply (rule LIM_inverse)
        apply (rule LIM_ident)
        apply (rule x)
        done
    next
      fix h::'a assume h: "h ≠ 0"
      show "0 ≤ norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
        apply (rule divide_nonneg_pos)
        apply (rule norm_ge_zero)
        apply (simp add: h)
        done
    next
      fix h::'a assume h: "h ≠ 0"
      have "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
            ≤ norm (?inv (x + h) - ?inv x) * norm h * norm (?inv x) / norm h"
        apply (rule divide_right_mono [OF _ norm_ge_zero])
        apply (rule order_trans [OF norm_mult_ineq])
        apply (rule mult_right_mono [OF _ norm_ge_zero])
        apply (rule norm_mult_ineq)
        done
      also have "… = norm (?inv (x + h) - ?inv x) * norm (?inv x)"
        by simp
      finally show "norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h
            ≤ norm (?inv (x + h) - ?inv x) * norm (?inv x)" .
    qed
  qed
qed

subsection {* Alternate definition *}

lemma field_fderiv_def:
  fixes x :: "'a::real_normed_field" shows
  "FDERIV f x :> (λh. h * D) = (λh. (f (x + h) - f x) / h) -- 0 --> D"
  unfolding fderiv_def
  apply (simp add: mult.bounded_linear_left)
  apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
  apply (subst diff_divide_distrib)
  apply (subst times_divide_eq_right [symmetric])
  apply (simp cong: LIM_cong add: divide_self)
  apply (simp add: LIM_norm_zero_iff LIM_zero_iff)
  done

end