12 |
12 |
13 subsection\<^marker>\<open>tag unimportant\<close>\<open>General lemmas\<close> |
13 subsection\<^marker>\<open>tag unimportant\<close>\<open>General lemmas\<close> |
14 |
14 |
15 lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z" |
15 lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z" |
16 by (simp add: complex_nonneg_Reals_iff cmod_eq_Re) |
16 by (simp add: complex_nonneg_Reals_iff cmod_eq_Re) |
17 |
|
18 lemma has_derivative_mult_right: |
|
19 fixes c:: "'a :: real_normed_algebra" |
|
20 shows "(((*) c) has_derivative ((*) c)) F" |
|
21 by (rule has_derivative_mult_right [OF has_derivative_ident]) |
|
22 |
|
23 lemma has_derivative_of_real[derivative_intros, simp]: |
|
24 "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F" |
|
25 using bounded_linear.has_derivative[OF bounded_linear_of_real] . |
|
26 |
|
27 lemma has_vector_derivative_real_field: |
|
28 "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)" |
|
29 using has_derivative_compose[of of_real of_real a _ f "(*) f'"] |
|
30 by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def) |
|
31 lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field |
|
32 |
17 |
33 lemma fact_cancel: |
18 lemma fact_cancel: |
34 fixes c :: "'a::real_field" |
19 fixes c :: "'a::real_field" |
35 shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)" |
20 shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)" |
36 using of_nat_neq_0 by force |
21 using of_nat_neq_0 by force |
37 |
|
38 lemma bilinear_times: |
|
39 fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)" |
|
40 by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) |
|
41 |
|
42 lemma linear_cnj: "linear cnj" |
|
43 using bounded_linear.linear[OF bounded_linear_cnj] . |
|
44 |
22 |
45 lemma vector_derivative_cnj_within: |
23 lemma vector_derivative_cnj_within: |
46 assumes "at x within A \<noteq> bot" and "f differentiable at x within A" |
24 assumes "at x within A \<noteq> bot" and "f differentiable at x within A" |
47 shows "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) = |
25 shows "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) = |
48 cnj (vector_derivative f (at x within A))" (is "_ = cnj ?D") |
26 cnj (vector_derivative f (at x within A))" (is "_ = cnj ?D") |
80 lemma continuous_within_norm_id [continuous_intros]: "continuous (at x within S) norm" |
58 lemma continuous_within_norm_id [continuous_intros]: "continuous (at x within S) norm" |
81 by (rule continuous_norm [OF continuous_ident]) |
59 by (rule continuous_norm [OF continuous_ident]) |
82 |
60 |
83 lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm" |
61 lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm" |
84 by (intro continuous_on_id continuous_on_norm) |
62 by (intro continuous_on_id continuous_on_norm) |
85 |
|
86 lemmas DERIV_zero_constant = has_field_derivative_zero_constant |
|
87 |
63 |
88 lemma DERIV_zero_unique: |
64 lemma DERIV_zero_unique: |
89 assumes "convex S" |
65 assumes "convex S" |
90 and d0: "\<And>x. x\<in>S \<Longrightarrow> (f has_field_derivative 0) (at x within S)" |
66 and d0: "\<And>x. x\<in>S \<Longrightarrow> (f has_field_derivative 0) (at x within S)" |
91 and "a \<in> S" |
67 and "a \<in> S" |