theory Scratch
imports Bounded_Linear_Function
begin

subsection {* Library Additions *}

lemma has_vector_derivative_at:
  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
    and D :: "'a"
    and x :: "real"
  shows
    "(f has_vector_derivative D) (at x) =
      (\<lambda>h. (f (x + h) - f x) /\<^sub>R h) -- 0 --> D"
  apply (simp add: bounded_linear_scaleR_left has_vector_derivative_def has_derivative_at)
  apply (subst (1) LIM_offset_zero_iff)
  apply (subst (2) Lim_null)
  apply simp
  apply (subst tendsto_norm_zero_iff[symmetric])
  apply (subst (2) tendsto_norm_zero_iff[symmetric])
  apply (rule LIM_equal)
  apply (simp add: inverse_eq_divide scaleR_diff_right)
  apply (auto simp: algebra_simps norm_minus_commute abs_real_def)
  done

text {*
  TODO: compare/replace
    in @{thm uniformly_cauchy_imp_uniformly_convergent}, @{thm uniformly_convergent_eq_cauchy}
*}

definition
  converges_uniformly_on
where
  "converges_uniformly_on S f F l \<longleftrightarrow> (\<forall>e > 0. eventually (\<lambda>n. \<forall>x \<in> S. dist (f n x) (l x) < e) F)"

lemma
  converges_uniformly_onE:
  assumes "converges_uniformly_on S f l"
  assumes "e > 0"
  obtains N where "\<And>x n. x \<in> S \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f n x) (l x) < e"
  using assms
  by (force simp: converges_uniformly_on_def)

lemma swap_uniform_limit:
  fixes f::"nat\<Rightarrow>'a::metric_space\<Rightarrow>'b::metric_space"
  assumes fz: "\<And>n. (f n ---> g n) (at x within S)"
  assumes fx: "g ----> l"
  assumes uc: "converges_uniformly_on S (\<lambda>n x. f n x) h"
  shows "(h ---> l) (at x within S)"
proof (rule tendstoI)
  fix e :: real assume "0 < e"
  def e' \<equiv> "e/3"
  have "0 < e'" using `0 < e` by (auto simp: e'_def)

  from converges_uniformly_onE[OF uc `0 < e'`]
  obtain N where N: "\<And>x n. x \<in> S \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f n x) (h x) < e'" by metis
  from metric_LIMSEQ_D[OF fx `0 < e'`] obtain M where M: "\<And>n. n \<ge> M \<Longrightarrow> dist (g n) l < e'" by metis
  def L \<equiv> "max N M"
  hence "L \<ge> N" "L \<ge> M"
    by auto

  from `L \<ge> N` N have "eventually (\<lambda>x. dist (h x) (f L x) < e') (at x within S)"
    by (auto simp: eventually_at_filter dist_commute)
  moreover
  from M `L \<ge> M` have "eventually (\<lambda>x. dist l (g L) < e') (at x within S)"
    by (auto simp: eventually_at_filter dist_commute)
  moreover
  from tendstoD[OF fz `0 < e'`, of L] have "eventually (\<lambda>x. dist (g L) (f L x) < e') (at x within S)"
    by (simp add: dist_commute)
  ultimately
  show "eventually (\<lambda>x. dist (h x) l < e) (at x within S)"
  proof eventually_elim
    case elim
    have "dist (h x) l \<le> dist (h x) (g L) + dist l (g L)"
      by (rule dist_triangle2)
    also
    from dist_triangle_lt[OF add_strict_mono, OF elim(1,3)]
    have "dist (h x) (g L) < e' + e'" .
    also note elim(2)
    also have "e' + e' + e' \<le> e" by (simp add: e'_def `0 < e`)
    finally show ?case by simp
  qed
qed


subsection {* Derivative of Exponential *}

term onorm
term exp

thm uniformly_continuous_on_sequentially
term suminf
term "op sums"

lemma "norm (exp (A::(real*real*real) blinfun)) \<le> exp (norm A)"
by (metis norm_exp)

lemma exp_commutes: "exp A * A = A * exp A"
proof -
  have "A * exp A = (\<Sum>n. A * (A ^ n /\<^sub>R real (fact n)))"
    by (simp add: exp_def suminf_mult[symmetric] summable_exp_generic)
  also have "\<dots> = (\<Sum>n. (A ^ n /\<^sub>R real (fact n)) * A)"
    by (simp add: power_commutes)
  also have "\<dots> = exp A * A"
    by (simp add: exp_def suminf_mult2 summable_exp_generic)
  finally show ?thesis ..
qed

lemma exp_general_uniform:
  "\<exists>l. converges_uniformly_on S (\<lambda>n x. \<Sum>i<n. x ^ n /\<^sub>R real (fact n)) l"
  sorry
  --"using Weierstrass M-Test?! (TODO: http://en.wikipedia.org/wiki/Weierstrass_M-test)
    and @{thm norm_exp}"

thm summable_ratio_test
thm tendsto_scaleR
thm tendsto_mult_right_zero
thm tendsto_mult_left
thm tendsto_add
thm bounded_bilinear.tendsto_zero
thm tendsto_intros
thm LIM_def
thm norm_power_ineq
thm norm_mult_ineq
thm power_Suc2

lemma
  scaleR_power:
  fixes x and y::"'a::real_normed_algebra_1"
  shows "scaleR x y ^ n = x ^ n *\<^sub>R y ^ n"
  by (induct n) auto

(* We prove the derivative of exp at zero. From this, we can prove the derivate at all points. *)
lemma exp_diff_at_0: "(\<lambda>x. (exp (x *\<^sub>R A) - 1) /\<^sub>R x) -- 0 --> A"
unfolding exp_def
proof -
  (* Bring the expression into a nicer form so that we can prove its limit. *)
  {
    fix x::real
    assume "x \<noteq> 0"
    have "((\<Sum>n. (x *\<^sub>R A) ^ n /\<^sub>R real (fact n)) - 1) /\<^sub>R x =
          A + (\<Sum>n. (x^(n+1) *\<^sub>R A^(n+2)) /\<^sub>R real (fact (n+2)))"
      apply (subst suminf_split_initial_segment[where k=2])
      apply (simp add: summable_exp_generic)
      unfolding scaleR_add_right scaleR_diff_right
    proof -
      case goal1
      have "(\<Sum>n. (x *\<^sub>R A) ^ (n + 2) /\<^sub>R real (fact (n + 2))) /\<^sub>R x =
        (\<Sum>n. x ^ (n + 1) *\<^sub>R A ^ (n + 2) /\<^sub>R real (fact (n + 2)))"
        apply (subst suminf_scaleR_right)
        apply (rule summable_ignore_initial_segment)
        apply (simp add: summable_exp_generic)
        apply (simp add: field_simps scaleR_power `x \<noteq> 0`)
        done
      moreover have "(\<Sum>i<2. (x *\<^sub>R A) ^ i /\<^sub>R real (fact i)) /\<^sub>R x -
           1 /\<^sub>R x = A"
        using goal1 `x \<noteq> 0`
        by (auto simp: numeral_2_eq_2 algebra_simps)
      ultimately show ?case by simp
    qed
  }
  from _ this have "((\<lambda>x. ((\<Sum>n. (x *\<^sub>R A) ^ n /\<^sub>R real (fact n)) - 1) /\<^sub>R x) -- 0 --> A)
        =
        ((\<lambda>x. A + (\<Sum>n. (x^(n+1) *\<^sub>R A^(n+2)) /\<^sub>R real (fact (n+2)))) -- 0 --> A)"
    by (rule LIM_cong) auto
  moreover
  have "(\<lambda>x. A + (\<Sum>n. (x^(n+1) *\<^sub>R A^(n+2)) /\<^sub>R real (fact (n+2)))) -- 0 --> A + 0"
    proof (rule tendsto_add)
      show "(\<lambda>x. A) -- 0 --> A" by simp
    next
      show "(\<lambda>x. (\<Sum>n. x^(n+1) *\<^sub>R A^(n+2) /\<^sub>R real (fact (n + 2)))) -- 0 --> 0"
        sorry (* TODO: Prove! *)
    qed
  ultimately
  show "(\<lambda>x. ((\<Sum>n. (x *\<^sub>R A) ^ n /\<^sub>R real (fact n)) - 1) /\<^sub>R x) -- 0 --> A" by simp
qed

(* Proof the derivative of "exp(t *\<^sub>R A)" is "exp(t *\<^sub>R A) * A". *)
lemma "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t)"
proof -
  (* Proof via the limit definition. *)
  have "(\<lambda>h. (exp ((t + h) *\<^sub>R A) - exp (t *\<^sub>R A)) /\<^sub>R h) -- 0 --> exp (t *\<^sub>R A) * A =
        (\<lambda>h::real. (exp (t *\<^sub>R A) * ((exp (h *\<^sub>R A) - 1) /\<^sub>R h))) -- 0 --> exp (t *\<^sub>R A) * A"
    proof (rule LIM_equal)
      show "\<forall>x. x \<noteq> 0 \<longrightarrow> (exp ((t + x) *\<^sub>R A) - exp (t *\<^sub>R A)) /\<^sub>R x = exp (t *\<^sub>R A) * ((exp (x *\<^sub>R A) - 1) /\<^sub>R x)"
      proof (rule allI[OF impI])
        fix x :: real
        assume "x \<noteq> 0"
        have "exp ((t + x) *\<^sub>R A) = exp (t *\<^sub>R A) * exp (x *\<^sub>R A)"
          by (simp add: exp_add_commuting scaleR_add_left)
        thus "(exp ((t + x) *\<^sub>R A) - exp (t *\<^sub>R A)) /\<^sub>R x = exp (t *\<^sub>R A) * ((exp (x *\<^sub>R A) - 1) /\<^sub>R x)"
          by (simp add: right_diff_distrib)
      qed
    qed
  moreover
  have "(\<lambda>h::real. (exp (t *\<^sub>R A) * ((exp (h *\<^sub>R A) - 1) /\<^sub>R h))) -- 0 --> exp (t *\<^sub>R A) * A"
    by (rule tendsto_mult_left[OF exp_diff_at_0])
  ultimately
  show ?thesis using has_vector_derivative_at by auto
qed

end
