equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Frechet Derivative *} |
5 header {* Frechet Derivative *} |
6 |
6 |
7 theory FrechetDeriv |
7 theory FrechetDeriv |
8 imports Lim Complex_Main |
8 imports Complex_Main |
9 begin |
9 begin |
10 |
10 |
11 definition |
11 definition |
12 fderiv :: |
12 fderiv :: |
13 "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool" |
13 "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool" |
396 norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x)) |
396 norm (f (x + h) ** g (x + h) - f x ** g x - (f x ** G h + F h ** g x)) |
397 / norm h) -- 0 --> 0" |
397 / norm h) -- 0 --> 0" |
398 by (simp only: FDERIV_lemma) |
398 by (simp only: FDERIV_lemma) |
399 qed |
399 qed |
400 |
400 |
401 lemmas FDERIV_mult = mult.FDERIV |
401 lemmas FDERIV_mult = |
402 |
402 bounded_bilinear.FDERIV [OF bounded_bilinear_mult] |
403 lemmas FDERIV_scaleR = scaleR.FDERIV |
403 |
|
404 lemmas FDERIV_scaleR = |
|
405 bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR] |
404 |
406 |
405 |
407 |
406 subsection {* Powers *} |
408 subsection {* Powers *} |
407 |
409 |
408 lemma FDERIV_power_Suc: |
410 lemma FDERIV_power_Suc: |
425 |
427 |
426 |
428 |
427 subsection {* Inverse *} |
429 subsection {* Inverse *} |
428 |
430 |
429 lemmas bounded_linear_mult_const = |
431 lemmas bounded_linear_mult_const = |
430 mult.bounded_linear_left [THEN bounded_linear_compose] |
432 bounded_linear_mult_left [THEN bounded_linear_compose] |
431 |
433 |
432 lemmas bounded_linear_const_mult = |
434 lemmas bounded_linear_const_mult = |
433 mult.bounded_linear_right [THEN bounded_linear_compose] |
435 bounded_linear_mult_right [THEN bounded_linear_compose] |
434 |
436 |
435 lemma FDERIV_inverse: |
437 lemma FDERIV_inverse: |
436 fixes x :: "'a::real_normed_div_algebra" |
438 fixes x :: "'a::real_normed_div_algebra" |
437 assumes x: "x \<noteq> 0" |
439 assumes x: "x \<noteq> 0" |
438 shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))" |
440 shows "FDERIV inverse x :> (\<lambda>h. - (inverse x * h * inverse x))" |
508 |
510 |
509 lemma field_fderiv_def: |
511 lemma field_fderiv_def: |
510 fixes x :: "'a::real_normed_field" shows |
512 fixes x :: "'a::real_normed_field" shows |
511 "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D" |
513 "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D" |
512 apply (unfold fderiv_def) |
514 apply (unfold fderiv_def) |
513 apply (simp add: mult.bounded_linear_left) |
515 apply (simp add: bounded_linear_mult_left) |
514 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) |
516 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) |
515 apply (subst diff_divide_distrib) |
517 apply (subst diff_divide_distrib) |
516 apply (subst times_divide_eq_left [symmetric]) |
518 apply (subst times_divide_eq_left [symmetric]) |
517 apply (simp cong: LIM_cong) |
519 apply (simp cong: LIM_cong) |
518 apply (simp add: LIM_norm_zero_iff LIM_zero_iff) |
520 apply (simp add: LIM_norm_zero_iff LIM_zero_iff) |