equal
deleted
inserted
replaced
93 have difg_eq_0: "\<forall>m<n. difg m 0 = 0" |
93 have difg_eq_0: "\<forall>m<n. difg m 0 = 0" |
94 by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.reindex) |
94 by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.reindex) |
95 have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x" |
95 have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x" |
96 by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp |
96 by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp |
97 have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)" |
97 have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)" |
98 by (rule differentiableI [OF difg_Suc [rule_format]]) simp |
98 using difg_Suc real_differentiable_def by auto |
99 have difg_Suc_eq_0: |
99 have difg_Suc_eq_0: |
100 "\<And>m t. m < n \<Longrightarrow> 0 \<le> t \<Longrightarrow> t \<le> h \<Longrightarrow> DERIV (difg m) t :> 0 \<Longrightarrow> difg (Suc m) t = 0" |
100 "\<And>m t. m < n \<Longrightarrow> 0 \<le> t \<Longrightarrow> t \<le> h \<Longrightarrow> DERIV (difg m) t :> 0 \<Longrightarrow> difg (Suc m) t = 0" |
101 by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp |
101 by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp |
102 |
102 |
103 have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0" |
103 have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0" |
109 show "0 < h" by fact |
109 show "0 < h" by fact |
110 show "difg 0 0 = difg 0 h" |
110 show "difg 0 0 = difg 0 h" |
111 by (simp add: difg_0 g2) |
111 by (simp add: difg_0 g2) |
112 show "continuous_on {0..h} (difg 0)" |
112 show "continuous_on {0..h} (difg 0)" |
113 by (simp add: continuous_at_imp_continuous_on isCont_difg n) |
113 by (simp add: continuous_at_imp_continuous_on isCont_difg n) |
114 show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0::nat) differentiable (at x)" |
114 qed (simp add: differentiable_difg n) |
115 by (simp add: differentiable_difg n) |
|
116 qed |
|
117 next |
115 next |
118 case (Suc m') |
116 case (Suc m') |
119 then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" |
117 then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" |
120 by simp |
118 by simp |
121 then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" |
119 then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" |
127 using t \<open>Suc m' < n\<close> by (simp add: difg_Suc_eq_0 difg_eq_0) |
125 using t \<open>Suc m' < n\<close> by (simp add: difg_Suc_eq_0 difg_eq_0) |
128 have "\<And>x. 0 \<le> x \<and> x \<le> t \<Longrightarrow> isCont (difg (Suc m')) x" |
126 have "\<And>x. 0 \<le> x \<and> x \<le> t \<Longrightarrow> isCont (difg (Suc m')) x" |
129 using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: isCont_difg) |
127 using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: isCont_difg) |
130 then show "continuous_on {0..t} (difg (Suc m'))" |
128 then show "continuous_on {0..t} (difg (Suc m'))" |
131 by (simp add: continuous_at_imp_continuous_on) |
129 by (simp add: continuous_at_imp_continuous_on) |
132 show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)" |
130 qed (use \<open>t < h\<close> \<open>Suc m' < n\<close> in \<open>simp add: differentiable_difg\<close>) |
133 using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: differentiable_difg) |
|
134 qed |
|
135 with \<open>t < h\<close> show ?case |
131 with \<open>t < h\<close> show ?case |
136 by auto |
132 by auto |
137 qed |
133 qed |
138 then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" |
134 then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" |
139 by fast |
135 by fast |