equal
deleted
inserted
replaced
6016 qed |
6016 qed |
6017 qed |
6017 qed |
6018 |
6018 |
6019 |
6019 |
6020 subsection \<open>Taylor series expansion\<close> |
6020 subsection \<open>Taylor series expansion\<close> |
6021 |
|
6022 lemma |
|
6023 setsum_telescope: |
|
6024 fixes f::"nat \<Rightarrow> 'a::ab_group_add" |
|
6025 shows "setsum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" |
|
6026 by (induct i) simp_all |
|
6027 |
6021 |
6028 lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative: |
6022 lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative: |
6029 assumes "p>0" |
6023 assumes "p>0" |
6030 and f0: "Df 0 = f" |
6024 and f0: "Df 0 = f" |
6031 and Df: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> |
6025 and Df: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> |