src/HOL/MacLaurin.thy
changeset 61944 5d06ecfdb472
parent 61799 4cf66f21b764
child 61954 1d43f86f48be
     1.1 --- a/src/HOL/MacLaurin.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -259,8 +259,8 @@
     1.4  
     1.5  lemma Maclaurin_bi_le:
     1.6     assumes "diff 0 = f"
     1.7 -   and DERIV : "\<forall>m t::real. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
     1.8 -   shows "\<exists>t. abs t \<le> abs x &
     1.9 +   and DERIV : "\<forall>m t::real. m < n & \<bar>t\<bar> \<le> \<bar>x\<bar> --> DERIV (diff m) t :> diff (Suc m) t"
    1.10 +   shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    1.11                f x =
    1.12                (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) +
    1.13       diff n t / (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
    1.14 @@ -294,7 +294,7 @@
    1.15    fixes x::real
    1.16    assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
    1.17    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
    1.18 -  shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
    1.19 +  shows "\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> & f x =
    1.20      (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    1.21                  (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
    1.22  proof (cases rule: linorder_cases)
    1.23 @@ -320,7 +320,7 @@
    1.24       "diff 0 = f &
    1.25        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
    1.26        x ~= 0 & n > 0
    1.27 -      --> (\<exists>t. 0 < abs t & abs t < abs x &
    1.28 +      --> (\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> &
    1.29                 f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    1.30                       (diff n t / (fact n)) * x ^ n)"
    1.31  by (blast intro: Maclaurin_all_lt)
    1.32 @@ -336,7 +336,7 @@
    1.33  lemma Maclaurin_all_le:
    1.34    assumes INIT: "diff 0 = f"
    1.35    and DERIV: "\<forall>m x::real. DERIV (diff m) x :> diff (Suc m) x"
    1.36 -  shows "\<exists>t. abs t \<le> abs x & f x =
    1.37 +  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> & f x =
    1.38      (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    1.39      (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
    1.40  proof cases
    1.41 @@ -363,7 +363,7 @@
    1.42  lemma Maclaurin_all_le_objl:
    1.43    "diff 0 = f &
    1.44        (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
    1.45 -      --> (\<exists>t::real. abs t \<le> abs x &
    1.46 +      --> (\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    1.47                f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    1.48                      (diff n t / (fact n)) * x ^ n)"
    1.49  by (blast intro: Maclaurin_all_le)
    1.50 @@ -375,15 +375,15 @@
    1.51    fixes x::real
    1.52    shows
    1.53    "[| x ~= 0; n > 0 |]
    1.54 -      ==> (\<exists>t. 0 < abs t &
    1.55 -                abs t < abs x &
    1.56 +      ==> (\<exists>t. 0 < \<bar>t\<bar> &
    1.57 +                \<bar>t\<bar> < \<bar>x\<bar> &
    1.58                  exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
    1.59                          (exp t / (fact n)) * x ^ n)"
    1.60  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
    1.61  
    1.62  
    1.63  lemma Maclaurin_exp_le:
    1.64 -     "\<exists>t::real. abs t \<le> abs x &
    1.65 +     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    1.66              exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
    1.67                         (exp t / (fact n)) * x ^ n"
    1.68  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
    1.69 @@ -422,7 +422,7 @@
    1.70  by (simp only: cos_add sin_add of_nat_Suc add_divide_distrib distrib_right, auto)
    1.71  
    1.72  lemma Maclaurin_sin_expansion2:
    1.73 -     "\<exists>t. abs t \<le> abs x &
    1.74 +     "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    1.75         sin x =
    1.76         (\<Sum>m<n. sin_coeff m * x ^ m)
    1.77        + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
    1.78 @@ -495,7 +495,7 @@
    1.79  by (simp only: cos_add sin_add of_nat_Suc distrib_right add_divide_distrib, auto)
    1.80  
    1.81  lemma Maclaurin_cos_expansion:
    1.82 -     "\<exists>t::real. abs t \<le> abs x &
    1.83 +     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    1.84         cos x =
    1.85         (\<Sum>m<n. cos_coeff m * x ^ m)
    1.86        + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
    1.87 @@ -550,12 +550,11 @@
    1.88  (* ------------------------------------------------------------------------- *)
    1.89  
    1.90  lemma sin_bound_lemma:
    1.91 -    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
    1.92 +    "[|x = y; \<bar>u\<bar> \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
    1.93  by auto
    1.94  
    1.95  lemma Maclaurin_sin_bound:
    1.96 -  "abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
    1.97 -  \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
    1.98 +  "\<bar>sin x - (\<Sum>m<n. sin_coeff m * x ^ m)\<bar> \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
    1.99  proof -
   1.100    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
   1.101      by (rule_tac mult_right_mono,simp_all)