66 using contour_integrable_on_def by blast |
66 using contour_integrable_on_def by blast |
67 |
67 |
68 text\<open>Show that we can forget about the localized derivative.\<close> |
68 text\<open>Show that we can forget about the localized derivative.\<close> |
69 |
69 |
70 lemma has_integral_localized_vector_derivative: |
70 lemma has_integral_localized_vector_derivative: |
71 "((\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow> |
71 "((\<lambda>x. f (g x) * vector_derivative p (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow> |
72 ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}" |
72 ((\<lambda>x. f (g x) * vector_derivative p (at x)) has_integral i) {a..b}" |
73 proof - |
73 proof - |
74 have *: "{a..b} - {a,b} = interior {a..b}" |
74 have *: "{a..b} - {a,b} = interior {a..b}" |
75 by (simp add: atLeastAtMost_diff_ends) |
75 by (simp add: atLeastAtMost_diff_ends) |
76 show ?thesis |
76 show ?thesis |
77 by (rule has_integral_spike_eq [of "{a,b}"]) (auto simp: at_within_interior [of _ "{a..b}"]) |
77 by (rule has_integral_spike_eq [of "{a,b}"]) (auto simp: at_within_interior [of _ "{a..b}"]) |
78 qed |
78 qed |
79 |
79 |
80 lemma integrable_on_localized_vector_derivative: |
80 lemma integrable_on_localized_vector_derivative: |
81 "(\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow> |
81 "(\<lambda>x. f (g x) * vector_derivative p (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow> |
82 (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}" |
82 (\<lambda>x. f (g x) * vector_derivative p (at x)) integrable_on {a..b}" |
83 by (simp add: integrable_on_def has_integral_localized_vector_derivative) |
83 by (simp add: integrable_on_def has_integral_localized_vector_derivative) |
84 |
84 |
85 lemma has_contour_integral: |
85 lemma has_contour_integral: |
86 "(f has_contour_integral i) g \<longleftrightarrow> |
86 "(f has_contour_integral i) g \<longleftrightarrow> |
87 ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" |
87 ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" |