83 |
83 |
84 obtain B where f_h: "f h = |
84 obtain B where f_h: "f h = |
85 (\<Sum>m<n. diff m (0::real) / (fact m) * h ^ m) + B * (h ^ n / (fact n))" |
85 (\<Sum>m<n. diff m (0::real) / (fact m) * h ^ m) + B * (h ^ n / (fact n))" |
86 using Maclaurin_lemma [OF h] .. |
86 using Maclaurin_lemma [OF h] .. |
87 |
87 |
88 def g \<equiv> "(\<lambda>t. f t - |
88 define g where [abs_def]: "g t = |
89 (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n)))))" |
89 f t - (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n))))" for t |
90 |
90 |
91 have g2: "g 0 = 0 & g h = 0" |
91 have g2: "g 0 = 0 & g h = 0" |
92 by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex) |
92 by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex) |
93 |
93 |
94 def difg \<equiv> "(%m t. diff m t - |
94 define difg where [abs_def]: "difg m t = |
95 (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m} |
95 diff m t - (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m} |
96 + (B * ((t ^ (n - m)) / (fact (n - m))))))" |
96 + (B * ((t ^ (n - m)) / (fact (n - m)))))" for m t |
97 |
97 |
98 have difg_0: "difg 0 = g" |
98 have difg_0: "difg 0 = g" |
99 unfolding difg_def g_def by (simp add: diff_0) |
99 unfolding difg_def g_def by (simp add: diff_0) |
100 |
100 |
101 have difg_Suc: "\<forall>(m::nat) t::real. |
101 have difg_Suc: "\<forall>(m::nat) t::real. |
102 m < n \<and> (0::real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t" |
102 m < n \<and> (0::real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t" |
103 using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2) |
103 using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2) |
104 |
104 |
105 have difg_eq_0: "\<forall>m<n. difg m 0 = 0" |
105 have difg_eq_0: "\<forall>m<n. difg m 0 = 0" |
106 by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum.reindex) |
106 by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum.reindex) |
107 |
107 |
108 have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x" |
108 have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x" |