src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
 author paulson Tue Jul 28 16:16:13 2015 +0100 (2015-07-28) changeset 60809 457abb82fb9e child 61104 3c2d4636cebc permissions -rw-r--r--
the Cauchy integral theorem and related material
 lp15@60809 ` 1` ```section \Complex path integrals and Cauchy's integral theorem\ ``` lp15@60809 ` 2` lp15@60809 ` 3` ```theory Cauchy_Integral_Thm ``` lp15@60809 ` 4` ```imports Complex_Transcendental Path_Connected ``` lp15@60809 ` 5` ```begin ``` lp15@60809 ` 6` lp15@60809 ` 7` lp15@60809 ` 8` ```definition piecewise_differentiable_on ``` lp15@60809 ` 9` ``` (infixr "piecewise'_differentiable'_on" 50) ``` lp15@60809 ` 10` ``` where "f piecewise_differentiable_on i \ ``` lp15@60809 ` 11` ``` continuous_on i f \ ``` lp15@60809 ` 12` ``` (\s. finite s \ (\x \ i - s. f differentiable (at x)))" ``` lp15@60809 ` 13` lp15@60809 ` 14` ```lemma piecewise_differentiable_on_imp_continuous_on: ``` lp15@60809 ` 15` ``` "f piecewise_differentiable_on s \ continuous_on s f" ``` lp15@60809 ` 16` ```by (simp add: piecewise_differentiable_on_def) ``` lp15@60809 ` 17` lp15@60809 ` 18` ```lemma piecewise_differentiable_on_subset: ``` lp15@60809 ` 19` ``` "f piecewise_differentiable_on s \ t \ s \ f piecewise_differentiable_on t" ``` lp15@60809 ` 20` ``` using continuous_on_subset ``` lp15@60809 ` 21` ``` by (fastforce simp: piecewise_differentiable_on_def) ``` lp15@60809 ` 22` lp15@60809 ` 23` ```lemma differentiable_on_imp_piecewise_differentiable: ``` lp15@60809 ` 24` ``` fixes a:: "'a::{linorder_topology,real_normed_vector}" ``` lp15@60809 ` 25` ``` shows "f differentiable_on {a..b} \ f piecewise_differentiable_on {a..b}" ``` lp15@60809 ` 26` ``` apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on) ``` lp15@60809 ` 27` ``` apply (rule_tac x="{a,b}" in exI, simp) ``` lp15@60809 ` 28` ``` by (metis DiffE atLeastAtMost_diff_ends differentiable_on_subset subsetI ``` lp15@60809 ` 29` ``` differentiable_on_eq_differentiable_at open_greaterThanLessThan) ``` lp15@60809 ` 30` lp15@60809 ` 31` ```lemma differentiable_imp_piecewise_differentiable: ``` lp15@60809 ` 32` ``` "(\x. x \ s \ f differentiable (at x)) ``` lp15@60809 ` 33` ``` \ f piecewise_differentiable_on s" ``` lp15@60809 ` 34` ```by (auto simp: piecewise_differentiable_on_def differentiable_on_eq_differentiable_at ``` lp15@60809 ` 35` ``` differentiable_imp_continuous_within continuous_at_imp_continuous_on) ``` lp15@60809 ` 36` lp15@60809 ` 37` ```lemma piecewise_differentiable_compose: ``` lp15@60809 ` 38` ``` "\f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s); ``` lp15@60809 ` 39` ``` \x. finite (s \ f-`{x})\ ``` lp15@60809 ` 40` ``` \ (g o f) piecewise_differentiable_on s" ``` lp15@60809 ` 41` ``` apply (simp add: piecewise_differentiable_on_def, safe) ``` lp15@60809 ` 42` ``` apply (blast intro: continuous_on_compose2) ``` lp15@60809 ` 43` ``` apply (rename_tac A B) ``` lp15@60809 ` 44` ``` apply (rule_tac x="A \ (\x\B. s \ f-`{x})" in exI) ``` lp15@60809 ` 45` ``` using differentiable_chain_at by blast ``` lp15@60809 ` 46` lp15@60809 ` 47` ```lemma piecewise_differentiable_affine: ``` lp15@60809 ` 48` ``` fixes m::real ``` lp15@60809 ` 49` ``` assumes "f piecewise_differentiable_on ((\x. m *\<^sub>R x + c) ` s)" ``` lp15@60809 ` 50` ``` shows "(f o (\x. m *\<^sub>R x + c)) piecewise_differentiable_on s" ``` lp15@60809 ` 51` ```proof (cases "m = 0") ``` lp15@60809 ` 52` ``` case True ``` lp15@60809 ` 53` ``` then show ?thesis ``` lp15@60809 ` 54` ``` unfolding o_def ``` lp15@60809 ` 55` ``` by (force intro: differentiable_imp_piecewise_differentiable differentiable_const) ``` lp15@60809 ` 56` ```next ``` lp15@60809 ` 57` ``` case False ``` lp15@60809 ` 58` ``` show ?thesis ``` lp15@60809 ` 59` ``` apply (rule piecewise_differentiable_compose [OF differentiable_imp_piecewise_differentiable]) ``` lp15@60809 ` 60` ``` apply (rule assms derivative_intros | simp add: False vimage_def real_vector_affinity_eq)+ ``` lp15@60809 ` 61` ``` done ``` lp15@60809 ` 62` ```qed ``` lp15@60809 ` 63` lp15@60809 ` 64` ```lemma piecewise_differentiable_cases: ``` lp15@60809 ` 65` ``` fixes c::real ``` lp15@60809 ` 66` ``` assumes "f piecewise_differentiable_on {a..c}" ``` lp15@60809 ` 67` ``` "g piecewise_differentiable_on {c..b}" ``` lp15@60809 ` 68` ``` "a \ c" "c \ b" "f c = g c" ``` lp15@60809 ` 69` ``` shows "(\x. if x \ c then f x else g x) piecewise_differentiable_on {a..b}" ``` lp15@60809 ` 70` ```proof - ``` lp15@60809 ` 71` ``` obtain s t where st: "finite s" "finite t" ``` lp15@60809 ` 72` ``` "\x\{a..c} - s. f differentiable at x" ``` lp15@60809 ` 73` ``` "\x\{c..b} - t. g differentiable at x" ``` lp15@60809 ` 74` ``` using assms ``` lp15@60809 ` 75` ``` by (auto simp: piecewise_differentiable_on_def) ``` lp15@60809 ` 76` ``` have "continuous_on {a..c} f" "continuous_on {c..b} g" ``` lp15@60809 ` 77` ``` using assms piecewise_differentiable_on_def by auto ``` lp15@60809 ` 78` ``` then have "continuous_on {a..b} (\x. if x \ c then f x else g x)" ``` lp15@60809 ` 79` ``` using continuous_on_cases [OF closed_real_atLeastAtMost [of a c], ``` lp15@60809 ` 80` ``` OF closed_real_atLeastAtMost [of c b], ``` lp15@60809 ` 81` ``` of f g "\x. x\c"] assms ``` lp15@60809 ` 82` ``` by (force simp: ivl_disj_un_two_touch) ``` lp15@60809 ` 83` ``` moreover ``` lp15@60809 ` 84` ``` { fix x ``` lp15@60809 ` 85` ``` assume x: "x \ {a..b} - insert c (s \ t)" ``` lp15@60809 ` 86` ``` have "(\x. if x \ c then f x else g x) differentiable at x" (is "?diff_fg") ``` lp15@60809 ` 87` ``` proof (cases x c rule: le_cases) ``` lp15@60809 ` 88` ``` case le show ?diff_fg ``` lp15@60809 ` 89` ``` apply (rule differentiable_transform_at [of "dist x c" _ f]) ``` lp15@60809 ` 90` ``` using dist_nz x dist_real_def le st x ``` lp15@60809 ` 91` ``` apply auto ``` lp15@60809 ` 92` ``` done ``` lp15@60809 ` 93` ``` next ``` lp15@60809 ` 94` ``` case ge show ?diff_fg ``` lp15@60809 ` 95` ``` apply (rule differentiable_transform_at [of "dist x c" _ g]) ``` lp15@60809 ` 96` ``` using dist_nz x dist_real_def ge st x ``` lp15@60809 ` 97` ``` apply auto ``` lp15@60809 ` 98` ``` done ``` lp15@60809 ` 99` ``` qed ``` lp15@60809 ` 100` ``` } ``` lp15@60809 ` 101` ``` then have "\s. finite s \ (\x\{a..b} - s. (\x. if x \ c then f x else g x) differentiable at x)" ``` lp15@60809 ` 102` ``` using st ``` lp15@60809 ` 103` ``` by (metis (full_types) finite_Un finite_insert) ``` lp15@60809 ` 104` ``` ultimately show ?thesis ``` lp15@60809 ` 105` ``` by (simp add: piecewise_differentiable_on_def) ``` lp15@60809 ` 106` ```qed ``` lp15@60809 ` 107` lp15@60809 ` 108` ```lemma piecewise_differentiable_neg: ``` lp15@60809 ` 109` ``` "f piecewise_differentiable_on s \ (\x. -(f x)) piecewise_differentiable_on s" ``` lp15@60809 ` 110` ``` by (auto simp: piecewise_differentiable_on_def continuous_on_minus) ``` lp15@60809 ` 111` lp15@60809 ` 112` ```lemma piecewise_differentiable_add: ``` lp15@60809 ` 113` ``` assumes "f piecewise_differentiable_on i" ``` lp15@60809 ` 114` ``` "g piecewise_differentiable_on i" ``` lp15@60809 ` 115` ``` shows "(\x. f x + g x) piecewise_differentiable_on i" ``` lp15@60809 ` 116` ```proof - ``` lp15@60809 ` 117` ``` obtain s t where st: "finite s" "finite t" ``` lp15@60809 ` 118` ``` "\x\i - s. f differentiable at x" ``` lp15@60809 ` 119` ``` "\x\i - t. g differentiable at x" ``` lp15@60809 ` 120` ``` using assms by (auto simp: piecewise_differentiable_on_def) ``` lp15@60809 ` 121` ``` then have "finite (s \ t) \ (\x\i - (s \ t). (\x. f x + g x) differentiable at x)" ``` lp15@60809 ` 122` ``` by auto ``` lp15@60809 ` 123` ``` moreover have "continuous_on i f" "continuous_on i g" ``` lp15@60809 ` 124` ``` using assms piecewise_differentiable_on_def by auto ``` lp15@60809 ` 125` ``` ultimately show ?thesis ``` lp15@60809 ` 126` ``` by (auto simp: piecewise_differentiable_on_def continuous_on_add) ``` lp15@60809 ` 127` ```qed ``` lp15@60809 ` 128` lp15@60809 ` 129` ```lemma piecewise_differentiable_diff: ``` lp15@60809 ` 130` ``` "\f piecewise_differentiable_on s; g piecewise_differentiable_on s\ ``` lp15@60809 ` 131` ``` \ (\x. f x - g x) piecewise_differentiable_on s" ``` lp15@60809 ` 132` ``` unfolding diff_conv_add_uminus ``` lp15@60809 ` 133` ``` by (metis piecewise_differentiable_add piecewise_differentiable_neg) ``` lp15@60809 ` 134` lp15@60809 ` 135` lp15@60809 ` 136` ```subsection \Valid paths, and their start and finish\ ``` lp15@60809 ` 137` lp15@60809 ` 138` ```lemma Diff_Un_eq: "A - (B \ C) = A - B - C" ``` lp15@60809 ` 139` ``` by blast ``` lp15@60809 ` 140` lp15@60809 ` 141` ```definition valid_path :: "(real \ 'a :: real_normed_vector) \ bool" ``` lp15@60809 ` 142` ``` where "valid_path f \ f piecewise_differentiable_on {0..1::real}" ``` lp15@60809 ` 143` lp15@60809 ` 144` ```definition closed_path :: "(real \ 'a :: real_normed_vector) \ bool" ``` lp15@60809 ` 145` ``` where "closed_path g \ g 0 = g 1" ``` lp15@60809 ` 146` lp15@60809 ` 147` ```lemma valid_path_compose: ``` lp15@60809 ` 148` ``` assumes "valid_path g" "f differentiable_on (path_image g)" ``` lp15@60809 ` 149` ``` shows "valid_path (f o g)" ``` lp15@60809 ` 150` ```proof - ``` lp15@60809 ` 151` ``` { fix s :: "real set" ``` lp15@60809 ` 152` ``` assume df: "f differentiable_on g ` {0..1}" ``` lp15@60809 ` 153` ``` and cg: "continuous_on {0..1} g" ``` lp15@60809 ` 154` ``` and s: "finite s" ``` lp15@60809 ` 155` ``` and dg: "\x. x\{0..1} - s \ g differentiable at x" ``` lp15@60809 ` 156` ``` have dfo: "f differentiable_on g ` {0<..<1}" ``` lp15@60809 ` 157` ``` by (auto intro: differentiable_on_subset [OF df]) ``` lp15@60809 ` 158` ``` have *: "\x. x \ {0<..<1} \ x \ s \ (f o g) differentiable (at x within ({0<..<1} - s))" ``` lp15@60809 ` 159` ``` apply (rule differentiable_chain_within) ``` lp15@60809 ` 160` ``` apply (simp_all add: dg differentiable_at_withinI differentiable_chain_within) ``` lp15@60809 ` 161` ``` using df ``` lp15@60809 ` 162` ``` apply (force simp: differentiable_on_def elim: Deriv.differentiable_subset) ``` lp15@60809 ` 163` ``` done ``` lp15@60809 ` 164` ``` have oo: "open ({0<..<1} - s)" ``` lp15@60809 ` 165` ``` by (simp add: finite_imp_closed open_Diff s) ``` lp15@60809 ` 166` ``` have "\s. finite s \ (\x\{0..1} - s. f \ g differentiable at x)" ``` lp15@60809 ` 167` ``` apply (rule_tac x="{0,1} Un s" in exI) ``` lp15@60809 ` 168` ``` apply (simp add: Diff_Un_eq atLeastAtMost_diff_ends s del: Set.Un_insert_left, clarify) ``` lp15@60809 ` 169` ``` apply (rule differentiable_within_open [OF _ oo, THEN iffD1]) ``` lp15@60809 ` 170` ``` apply (auto simp: *) ``` lp15@60809 ` 171` ``` done } ``` lp15@60809 ` 172` ``` with assms show ?thesis ``` lp15@60809 ` 173` ``` by (clarsimp simp: valid_path_def piecewise_differentiable_on_def continuous_on_compose ``` lp15@60809 ` 174` ``` differentiable_imp_continuous_on path_image_def simp del: o_apply) ``` lp15@60809 ` 175` ```qed ``` lp15@60809 ` 176` lp15@60809 ` 177` lp15@60809 ` 178` ```subsubsection\In particular, all results for paths apply\ ``` lp15@60809 ` 179` lp15@60809 ` 180` ```lemma valid_path_imp_path: "valid_path g \ path g" ``` lp15@60809 ` 181` ```by (simp add: path_def piecewise_differentiable_on_def valid_path_def) ``` lp15@60809 ` 182` lp15@60809 ` 183` ```lemma connected_valid_path_image: "valid_path g \ connected(path_image g)" ``` lp15@60809 ` 184` ``` by (metis connected_path_image valid_path_imp_path) ``` lp15@60809 ` 185` lp15@60809 ` 186` ```lemma compact_valid_path_image: "valid_path g \ compact(path_image g)" ``` lp15@60809 ` 187` ``` by (metis compact_path_image valid_path_imp_path) ``` lp15@60809 ` 188` lp15@60809 ` 189` ```lemma bounded_valid_path_image: "valid_path g \ bounded(path_image g)" ``` lp15@60809 ` 190` ``` by (metis bounded_path_image valid_path_imp_path) ``` lp15@60809 ` 191` lp15@60809 ` 192` ```lemma closed_valid_path_image: "valid_path g \ closed(path_image g)" ``` lp15@60809 ` 193` ``` by (metis closed_path_image valid_path_imp_path) ``` lp15@60809 ` 194` lp15@60809 ` 195` lp15@60809 ` 196` ```subsection\Contour Integrals along a path\ ``` lp15@60809 ` 197` lp15@60809 ` 198` ```text\This definition is for complex numbers only, and does not generalise to line integrals in a vector field\ ``` lp15@60809 ` 199` lp15@60809 ` 200` ```text\= piecewise differentiable function on [0,1]\ ``` lp15@60809 ` 201` lp15@60809 ` 202` ```definition has_path_integral :: "(complex \ complex) \ complex \ (real \ complex) \ bool" ``` lp15@60809 ` 203` ``` (infixr "has'_path'_integral" 50) ``` lp15@60809 ` 204` ``` where "(f has_path_integral i) g \ ``` lp15@60809 ` 205` ``` ((\x. f(g x) * vector_derivative g (at x within {0..1})) ``` lp15@60809 ` 206` ``` has_integral i) {0..1}" ``` lp15@60809 ` 207` lp15@60809 ` 208` ```definition path_integrable_on ``` lp15@60809 ` 209` ``` (infixr "path'_integrable'_on" 50) ``` lp15@60809 ` 210` ``` where "f path_integrable_on g \ \i. (f has_path_integral i) g" ``` lp15@60809 ` 211` lp15@60809 ` 212` ```definition path_integral ``` lp15@60809 ` 213` ``` where "path_integral g f \ @i. (f has_path_integral i) g" ``` lp15@60809 ` 214` lp15@60809 ` 215` ```lemma path_integral_unique: "(f has_path_integral i) g \ path_integral g f = i" ``` lp15@60809 ` 216` ``` by (auto simp: path_integral_def has_path_integral_def integral_def [symmetric]) ``` lp15@60809 ` 217` lp15@60809 ` 218` ```lemma has_path_integral_integral: ``` lp15@60809 ` 219` ``` "f path_integrable_on i \ (f has_path_integral (path_integral i f)) i" ``` lp15@60809 ` 220` ``` by (metis path_integral_unique path_integrable_on_def) ``` lp15@60809 ` 221` lp15@60809 ` 222` ```lemma has_path_integral_unique: ``` lp15@60809 ` 223` ``` "(f has_path_integral i) g \ (f has_path_integral j) g \ i = j" ``` lp15@60809 ` 224` ``` using has_integral_unique ``` lp15@60809 ` 225` ``` by (auto simp: has_path_integral_def) ``` lp15@60809 ` 226` lp15@60809 ` 227` ```lemma has_path_integral_integrable: "(f has_path_integral i) g \ f path_integrable_on g" ``` lp15@60809 ` 228` ``` using path_integrable_on_def by blast ``` lp15@60809 ` 229` lp15@60809 ` 230` ```(* Show that we can forget about the localized derivative.*) ``` lp15@60809 ` 231` lp15@60809 ` 232` ```lemma vector_derivative_within_interior: ``` lp15@60809 ` 233` ``` "\x \ interior s; NO_MATCH UNIV s\ ``` lp15@60809 ` 234` ``` \ vector_derivative f (at x within s) = vector_derivative f (at x)" ``` lp15@60809 ` 235` ``` apply (simp add: vector_derivative_def has_vector_derivative_def has_derivative_def netlimit_within_interior) ``` lp15@60809 ` 236` ``` apply (subst lim_within_interior, auto) ``` lp15@60809 ` 237` ``` done ``` lp15@60809 ` 238` lp15@60809 ` 239` ```lemma has_integral_localized_vector_derivative: ``` lp15@60809 ` 240` ``` "((\x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \ ``` lp15@60809 ` 241` ``` ((\x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}" ``` lp15@60809 ` 242` ```proof - ``` lp15@60809 ` 243` ``` have "{a..b} - {a,b} = interior {a..b}" ``` lp15@60809 ` 244` ``` by (simp add: atLeastAtMost_diff_ends) ``` lp15@60809 ` 245` ``` show ?thesis ``` lp15@60809 ` 246` ``` apply (rule has_integral_spike_eq [of "{a,b}"]) ``` lp15@60809 ` 247` ``` apply (auto simp: vector_derivative_within_interior) ``` lp15@60809 ` 248` ``` done ``` lp15@60809 ` 249` ```qed ``` lp15@60809 ` 250` lp15@60809 ` 251` ```lemma integrable_on_localized_vector_derivative: ``` lp15@60809 ` 252` ``` "(\x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \ ``` lp15@60809 ` 253` ``` (\x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}" ``` lp15@60809 ` 254` ``` by (simp add: integrable_on_def has_integral_localized_vector_derivative) ``` lp15@60809 ` 255` lp15@60809 ` 256` ```lemma has_path_integral: ``` lp15@60809 ` 257` ``` "(f has_path_integral i) g \ ``` lp15@60809 ` 258` ``` ((\x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" ``` lp15@60809 ` 259` ``` by (simp add: has_integral_localized_vector_derivative has_path_integral_def) ``` lp15@60809 ` 260` lp15@60809 ` 261` ```lemma path_integrable_on: ``` lp15@60809 ` 262` ``` "f path_integrable_on g \ ``` lp15@60809 ` 263` ``` (\t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}" ``` lp15@60809 ` 264` ``` by (simp add: has_path_integral integrable_on_def path_integrable_on_def) ``` lp15@60809 ` 265` lp15@60809 ` 266` ```subsection\Reversing a path\ ``` lp15@60809 ` 267` lp15@60809 ` 268` ```lemma valid_path_imp_reverse: ``` lp15@60809 ` 269` ``` assumes "valid_path g" ``` lp15@60809 ` 270` ``` shows "valid_path(reversepath g)" ``` lp15@60809 ` 271` ```proof - ``` lp15@60809 ` 272` ``` obtain s where "finite s" "\x\{0..1} - s. g differentiable at x" ``` lp15@60809 ` 273` ``` using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 274` ``` then have "finite (op - 1 ` s)" "(\x\{0..1} - op - 1 ` s. reversepath g differentiable at x)" ``` lp15@60809 ` 275` ``` apply (auto simp: reversepath_def) ``` lp15@60809 ` 276` ``` apply (rule differentiable_chain_at [of "\x::real. 1-x" _ g, unfolded o_def]) ``` lp15@60809 ` 277` ``` using image_iff ``` lp15@60809 ` 278` ``` apply fastforce+ ``` lp15@60809 ` 279` ``` done ``` lp15@60809 ` 280` ``` then show ?thesis using assms ``` lp15@60809 ` 281` ``` by (auto simp: valid_path_def piecewise_differentiable_on_def path_def [symmetric]) ``` lp15@60809 ` 282` ```qed ``` lp15@60809 ` 283` lp15@60809 ` 284` ```lemma valid_path_reversepath: "valid_path(reversepath g) \ valid_path g" ``` lp15@60809 ` 285` ``` using valid_path_imp_reverse by force ``` lp15@60809 ` 286` lp15@60809 ` 287` ```lemma has_path_integral_reversepath: ``` lp15@60809 ` 288` ``` assumes "valid_path g" "(f has_path_integral i) g" ``` lp15@60809 ` 289` ``` shows "(f has_path_integral (-i)) (reversepath g)" ``` lp15@60809 ` 290` ```proof - ``` lp15@60809 ` 291` ``` { fix s x ``` lp15@60809 ` 292` ``` assume xs: "\x\{0..1} - s. g differentiable at x" "x \ op - 1 ` s" "0 \ x" "x \ 1" ``` lp15@60809 ` 293` ``` have "vector_derivative (\x. g (1 - x)) (at x within {0..1}) = ``` lp15@60809 ` 294` ``` - vector_derivative g (at (1 - x) within {0..1})" ``` lp15@60809 ` 295` ``` proof - ``` lp15@60809 ` 296` ``` obtain f' where f': "(g has_vector_derivative f') (at (1 - x))" ``` lp15@60809 ` 297` ``` using xs ``` lp15@60809 ` 298` ``` apply (drule_tac x="1-x" in bspec) ``` lp15@60809 ` 299` ``` apply (simp_all add: has_vector_derivative_def differentiable_def, force) ``` lp15@60809 ` 300` ``` apply (blast elim!: linear_imp_scaleR dest: has_derivative_linear) ``` lp15@60809 ` 301` ``` done ``` lp15@60809 ` 302` ``` have "(g o (\x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)" ``` lp15@60809 ` 303` ``` apply (rule vector_diff_chain_within) ``` lp15@60809 ` 304` ``` apply (intro vector_diff_chain_within derivative_eq_intros | simp)+ ``` lp15@60809 ` 305` ``` apply (rule has_vector_derivative_at_within [OF f']) ``` lp15@60809 ` 306` ``` done ``` lp15@60809 ` 307` ``` then have mf': "((\x. g (1 - x)) has_vector_derivative -f') (at x)" ``` lp15@60809 ` 308` ``` by (simp add: o_def) ``` lp15@60809 ` 309` ``` show ?thesis ``` lp15@60809 ` 310` ``` using xs ``` lp15@60809 ` 311` ``` by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f']) ``` lp15@60809 ` 312` ``` qed ``` lp15@60809 ` 313` ``` } note * = this ``` lp15@60809 ` 314` ``` have 01: "{0..1::real} = cbox 0 1" ``` lp15@60809 ` 315` ``` by simp ``` lp15@60809 ` 316` ``` show ?thesis using assms ``` lp15@60809 ` 317` ``` apply (auto simp: has_path_integral_def) ``` lp15@60809 ` 318` ``` apply (drule has_integral_affinity01 [where m= "-1" and c=1]) ``` lp15@60809 ` 319` ``` apply (auto simp: reversepath_def valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 320` ``` apply (drule has_integral_neg) ``` lp15@60809 ` 321` ``` apply (rule_tac s = "(\x. 1 - x) ` s" in has_integral_spike_finite) ``` lp15@60809 ` 322` ``` apply (auto simp: *) ``` lp15@60809 ` 323` ``` done ``` lp15@60809 ` 324` ```qed ``` lp15@60809 ` 325` lp15@60809 ` 326` ```lemma path_integrable_reversepath: ``` lp15@60809 ` 327` ``` "valid_path g \ f path_integrable_on g \ f path_integrable_on (reversepath g)" ``` lp15@60809 ` 328` ``` using has_path_integral_reversepath path_integrable_on_def by blast ``` lp15@60809 ` 329` lp15@60809 ` 330` ```lemma path_integrable_reversepath_eq: ``` lp15@60809 ` 331` ``` "valid_path g \ (f path_integrable_on (reversepath g) \ f path_integrable_on g)" ``` lp15@60809 ` 332` ``` using path_integrable_reversepath valid_path_reversepath by fastforce ``` lp15@60809 ` 333` lp15@60809 ` 334` ```lemma path_integral_reversepath: ``` lp15@60809 ` 335` ``` "\valid_path g; f path_integrable_on g\ \ path_integral (reversepath g) f = -(path_integral g f)" ``` lp15@60809 ` 336` ``` using has_path_integral_reversepath path_integrable_on_def path_integral_unique by blast ``` lp15@60809 ` 337` lp15@60809 ` 338` lp15@60809 ` 339` ```subsection\Joining two paths together\ ``` lp15@60809 ` 340` lp15@60809 ` 341` ```lemma valid_path_join: ``` lp15@60809 ` 342` ``` assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2" ``` lp15@60809 ` 343` ``` shows "valid_path(g1 +++ g2)" ``` lp15@60809 ` 344` ```proof - ``` lp15@60809 ` 345` ``` have "g1 1 = g2 0" ``` lp15@60809 ` 346` ``` using assms by (auto simp: pathfinish_def pathstart_def) ``` lp15@60809 ` 347` ``` moreover have "(g1 o (\x. 2*x)) piecewise_differentiable_on {0..1/2}" ``` lp15@60809 ` 348` ``` apply (rule piecewise_differentiable_compose) ``` lp15@60809 ` 349` ``` using assms ``` lp15@60809 ` 350` ``` apply (auto simp: valid_path_def piecewise_differentiable_on_def continuous_on_joinpaths) ``` lp15@60809 ` 351` ``` apply (rule continuous_intros | simp)+ ``` lp15@60809 ` 352` ``` apply (force intro: finite_vimageI [where h = "op*2"] inj_onI) ``` lp15@60809 ` 353` ``` done ``` lp15@60809 ` 354` ``` moreover have "(g2 o (\x. 2*x-1)) piecewise_differentiable_on {1/2..1}" ``` lp15@60809 ` 355` ``` apply (rule piecewise_differentiable_compose) ``` lp15@60809 ` 356` ``` using assms ``` lp15@60809 ` 357` ``` apply (auto simp: valid_path_def piecewise_differentiable_on_def continuous_on_joinpaths) ``` lp15@60809 ` 358` ``` apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff)+ ``` lp15@60809 ` 359` ``` apply (force intro: finite_vimageI [where h = "(\x. 2*x - 1)"] inj_onI) ``` lp15@60809 ` 360` ``` done ``` lp15@60809 ` 361` ``` ultimately show ?thesis ``` lp15@60809 ` 362` ``` apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def) ``` lp15@60809 ` 363` ``` apply (rule piecewise_differentiable_cases) ``` lp15@60809 ` 364` ``` apply (auto simp: o_def) ``` lp15@60809 ` 365` ``` done ``` lp15@60809 ` 366` ```qed ``` lp15@60809 ` 367` lp15@60809 ` 368` ```lemma continuous_on_joinpaths_D1: ``` lp15@60809 ` 369` ``` "continuous_on {0..1} (g1 +++ g2) \ continuous_on {0..1} g1" ``` lp15@60809 ` 370` ``` apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"]) ``` lp15@60809 ` 371` ``` apply (simp add: joinpaths_def) ``` lp15@60809 ` 372` ``` apply (rule continuous_intros | simp)+ ``` lp15@60809 ` 373` ``` apply (auto elim!: continuous_on_subset) ``` lp15@60809 ` 374` ``` done ``` lp15@60809 ` 375` lp15@60809 ` 376` ```lemma continuous_on_joinpaths_D2: ``` lp15@60809 ` 377` ``` "\continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2\ \ continuous_on {0..1} g2" ``` lp15@60809 ` 378` ``` apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (\x. inverse 2*x + 1/2)"]) ``` lp15@60809 ` 379` ``` apply (simp add: joinpaths_def pathfinish_def pathstart_def Ball_def) ``` lp15@60809 ` 380` ``` apply (rule continuous_intros | simp)+ ``` lp15@60809 ` 381` ``` apply (auto elim!: continuous_on_subset) ``` lp15@60809 ` 382` ``` done ``` lp15@60809 ` 383` lp15@60809 ` 384` ```lemma piecewise_differentiable_D1: ``` lp15@60809 ` 385` ``` "(g1 +++ g2) piecewise_differentiable_on {0..1} \ g1 piecewise_differentiable_on {0..1}" ``` lp15@60809 ` 386` ``` apply (clarsimp simp add: piecewise_differentiable_on_def continuous_on_joinpaths_D1) ``` lp15@60809 ` 387` ``` apply (rule_tac x="insert 1 ((op*2)`s)" in exI) ``` lp15@60809 ` 388` ``` apply simp ``` lp15@60809 ` 389` ``` apply (intro ballI) ``` lp15@60809 ` 390` ``` apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at) ``` lp15@60809 ` 391` ``` apply (auto simp: dist_real_def joinpaths_def) ``` lp15@60809 ` 392` ``` apply (rule differentiable_chain_at derivative_intros | force)+ ``` lp15@60809 ` 393` ``` done ``` lp15@60809 ` 394` lp15@60809 ` 395` ```lemma piecewise_differentiable_D2: ``` lp15@60809 ` 396` ``` "\(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\ ``` lp15@60809 ` 397` ``` \ g2 piecewise_differentiable_on {0..1}" ``` lp15@60809 ` 398` ``` apply (clarsimp simp add: piecewise_differentiable_on_def continuous_on_joinpaths_D2) ``` lp15@60809 ` 399` ``` apply (rule_tac x="insert 0 ((\x. 2*x-1)`s)" in exI) ``` lp15@60809 ` 400` ``` apply simp ``` lp15@60809 ` 401` ``` apply (intro ballI) ``` lp15@60809 ` 402` ``` apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\x. (x+1)/2)" in differentiable_transform_at) ``` lp15@60809 ` 403` ``` apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm) ``` lp15@60809 ` 404` ``` apply (rule differentiable_chain_at derivative_intros | force simp: divide_simps)+ ``` lp15@60809 ` 405` ``` done ``` lp15@60809 ` 406` lp15@60809 ` 407` ```lemma valid_path_join_D1: "valid_path (g1 +++ g2) \ valid_path g1" ``` lp15@60809 ` 408` ``` by (simp add: valid_path_def piecewise_differentiable_D1) ``` lp15@60809 ` 409` lp15@60809 ` 410` ```lemma valid_path_join_D2: "\valid_path (g1 +++ g2); pathfinish g1 = pathstart g2\ \ valid_path g2" ``` lp15@60809 ` 411` ``` by (simp add: valid_path_def piecewise_differentiable_D2) ``` lp15@60809 ` 412` lp15@60809 ` 413` ```lemma valid_path_join_eq [simp]: ``` lp15@60809 ` 414` ``` "pathfinish g1 = pathstart g2 \ (valid_path(g1 +++ g2) \ valid_path g1 \ valid_path g2)" ``` lp15@60809 ` 415` ``` using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast ``` lp15@60809 ` 416` lp15@60809 ` 417` ```lemma has_path_integral_join: ``` lp15@60809 ` 418` ``` assumes "(f has_path_integral i1) g1" "(f has_path_integral i2) g2" ``` lp15@60809 ` 419` ``` "valid_path g1" "valid_path g2" ``` lp15@60809 ` 420` ``` shows "(f has_path_integral (i1 + i2)) (g1 +++ g2)" ``` lp15@60809 ` 421` ```proof - ``` lp15@60809 ` 422` ``` obtain s1 s2 ``` lp15@60809 ` 423` ``` where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x" ``` lp15@60809 ` 424` ``` and s2: "finite s2" "\x\{0..1} - s2. g2 differentiable at x" ``` lp15@60809 ` 425` ``` using assms ``` lp15@60809 ` 426` ``` by (auto simp: valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 427` ``` have 1: "((\x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}" ``` lp15@60809 ` 428` ``` and 2: "((\x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}" ``` lp15@60809 ` 429` ``` using assms ``` lp15@60809 ` 430` ``` by (auto simp: has_path_integral) ``` lp15@60809 ` 431` ``` have i1: "((\x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}" ``` lp15@60809 ` 432` ``` and i2: "((\x. (2*f (g2 (2*x - 1))) * vector_derivative g2 (at (2*x - 1))) has_integral i2) {1/2..1}" ``` lp15@60809 ` 433` ``` using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]] ``` lp15@60809 ` 434` ``` has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]] ``` lp15@60809 ` 435` ``` by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac) ``` lp15@60809 ` 436` ``` have g1: "\0 \ z; z*2 < 1; z*2 \ s1\ \ ``` lp15@60809 ` 437` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) = ``` lp15@60809 ` 438` ``` 2 *\<^sub>R vector_derivative g1 (at (z*2))" for z ``` lp15@60809 ` 439` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\z - 1/2\" _ "(\x. g1(2*x))"]]) ``` lp15@60809 ` 440` ``` apply (simp_all add: dist_real_def abs_if split: split_if_asm) ``` lp15@60809 ` 441` ``` apply (rule vector_diff_chain_at [of "\x. 2*x" 2 _ g1, simplified o_def]) ``` lp15@60809 ` 442` ``` apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) ``` lp15@60809 ` 443` ``` using s1 ``` lp15@60809 ` 444` ``` apply (auto simp: algebra_simps vector_derivative_works) ``` lp15@60809 ` 445` ``` done ``` lp15@60809 ` 446` ``` have g2: "\1 < z*2; z \ 1; z*2 - 1 \ s2\ \ ``` lp15@60809 ` 447` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) = ``` lp15@60809 ` 448` ``` 2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z ``` lp15@60809 ` 449` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\z - 1/2\" _ "(\x. g2 (2*x - 1))"]]) ``` lp15@60809 ` 450` ``` apply (simp_all add: dist_real_def abs_if split: split_if_asm) ``` lp15@60809 ` 451` ``` apply (rule vector_diff_chain_at [of "\x. 2*x - 1" 2 _ g2, simplified o_def]) ``` lp15@60809 ` 452` ``` apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) ``` lp15@60809 ` 453` ``` using s2 ``` lp15@60809 ` 454` ``` apply (auto simp: algebra_simps vector_derivative_works) ``` lp15@60809 ` 455` ``` done ``` lp15@60809 ` 456` ``` have "((\x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}" ``` lp15@60809 ` 457` ``` apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (op*2 -` s1)"]) ``` lp15@60809 ` 458` ``` using s1 ``` lp15@60809 ` 459` ``` apply (force intro: finite_vimageI [where h = "op*2"] inj_onI) ``` lp15@60809 ` 460` ``` apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1) ``` lp15@60809 ` 461` ``` done ``` lp15@60809 ` 462` ``` moreover have "((\x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}" ``` lp15@60809 ` 463` ``` apply (rule has_integral_spike_finite [OF _ _ i2, of "insert (1/2) ((\x. 2*x-1) -` s2)"]) ``` lp15@60809 ` 464` ``` using s2 ``` lp15@60809 ` 465` ``` apply (force intro: finite_vimageI [where h = "\x. 2*x-1"] inj_onI) ``` lp15@60809 ` 466` ``` apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g2) ``` lp15@60809 ` 467` ``` done ``` lp15@60809 ` 468` ``` ultimately ``` lp15@60809 ` 469` ``` show ?thesis ``` lp15@60809 ` 470` ``` apply (simp add: has_path_integral) ``` lp15@60809 ` 471` ``` apply (rule has_integral_combine [where c = "1/2"], auto) ``` lp15@60809 ` 472` ``` done ``` lp15@60809 ` 473` ```qed ``` lp15@60809 ` 474` lp15@60809 ` 475` ```lemma path_integrable_joinI: ``` lp15@60809 ` 476` ``` assumes "f path_integrable_on g1" "f path_integrable_on g2" ``` lp15@60809 ` 477` ``` "valid_path g1" "valid_path g2" ``` lp15@60809 ` 478` ``` shows "f path_integrable_on (g1 +++ g2)" ``` lp15@60809 ` 479` ``` using assms ``` lp15@60809 ` 480` ``` by (meson has_path_integral_join path_integrable_on_def) ``` lp15@60809 ` 481` lp15@60809 ` 482` ```lemma path_integrable_joinD1: ``` lp15@60809 ` 483` ``` assumes "f path_integrable_on (g1 +++ g2)" "valid_path g1" ``` lp15@60809 ` 484` ``` shows "f path_integrable_on g1" ``` lp15@60809 ` 485` ```proof - ``` lp15@60809 ` 486` ``` obtain s1 ``` lp15@60809 ` 487` ``` where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x" ``` lp15@60809 ` 488` ``` using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 489` ``` have "(\x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" ``` lp15@60809 ` 490` ``` using assms ``` lp15@60809 ` 491` ``` apply (auto simp: path_integrable_on) ``` lp15@60809 ` 492` ``` apply (drule integrable_on_subcbox [where a=0 and b="1/2"]) ``` lp15@60809 ` 493` ``` apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified]) ``` lp15@60809 ` 494` ``` done ``` lp15@60809 ` 495` ``` then have *: "(\x. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" ``` lp15@60809 ` 496` ``` by (force dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) ``` lp15@60809 ` 497` ``` have g1: "\0 < z; z < 1; z \ s1\ \ ``` lp15@60809 ` 498` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) = ``` lp15@60809 ` 499` ``` 2 *\<^sub>R vector_derivative g1 (at z)" for z ``` lp15@60809 ` 500` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\(z-1)/2\" _ "(\x. g1(2*x))"]]) ``` lp15@60809 ` 501` ``` apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) ``` lp15@60809 ` 502` ``` apply (rule vector_diff_chain_at [of "\x. x*2" 2 _ g1, simplified o_def]) ``` lp15@60809 ` 503` ``` using s1 ``` lp15@60809 ` 504` ``` apply (auto simp: vector_derivative_works has_vector_derivative_def has_derivative_def bounded_linear_mult_left) ``` lp15@60809 ` 505` ``` done ``` lp15@60809 ` 506` ``` show ?thesis ``` lp15@60809 ` 507` ``` using s1 ``` lp15@60809 ` 508` ``` apply (auto simp: path_integrable_on) ``` lp15@60809 ` 509` ``` apply (rule integrable_spike_finite [of "{0,1} \ s1", OF _ _ *]) ``` lp15@60809 ` 510` ``` apply (auto simp: joinpaths_def scaleR_conv_of_real g1) ``` lp15@60809 ` 511` ``` done ``` lp15@60809 ` 512` ```qed ``` lp15@60809 ` 513` lp15@60809 ` 514` ```lemma path_integrable_joinD2: (*FIXME: could combine these proofs*) ``` lp15@60809 ` 515` ``` assumes "f path_integrable_on (g1 +++ g2)" "valid_path g2" ``` lp15@60809 ` 516` ``` shows "f path_integrable_on g2" ``` lp15@60809 ` 517` ```proof - ``` lp15@60809 ` 518` ``` obtain s2 ``` lp15@60809 ` 519` ``` where s2: "finite s2" "\x\{0..1} - s2. g2 differentiable at x" ``` lp15@60809 ` 520` ``` using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 521` ``` have "(\x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}" ``` lp15@60809 ` 522` ``` using assms ``` lp15@60809 ` 523` ``` apply (auto simp: path_integrable_on) ``` lp15@60809 ` 524` ``` apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto) ``` lp15@60809 ` 525` ``` apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified]) ``` lp15@60809 ` 526` ``` apply (simp add: image_affinity_atLeastAtMost_diff) ``` lp15@60809 ` 527` ``` done ``` lp15@60809 ` 528` ``` then have *: "(\x. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) ``` lp15@60809 ` 529` ``` integrable_on {0..1}" ``` lp15@60809 ` 530` ``` by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real) ``` lp15@60809 ` 531` ``` have g2: "\0 < z; z < 1; z \ s2\ \ ``` lp15@60809 ` 532` ``` vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) = ``` lp15@60809 ` 533` ``` 2 *\<^sub>R vector_derivative g2 (at z)" for z ``` lp15@60809 ` 534` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\z/2\" _ "(\x. g2(2*x-1))"]]) ``` lp15@60809 ` 535` ``` apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) ``` lp15@60809 ` 536` ``` apply (rule vector_diff_chain_at [of "\x. x*2-1" 2 _ g2, simplified o_def]) ``` lp15@60809 ` 537` ``` using s2 ``` lp15@60809 ` 538` ``` apply (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left ``` lp15@60809 ` 539` ``` vector_derivative_works add_divide_distrib) ``` lp15@60809 ` 540` ``` done ``` lp15@60809 ` 541` ``` show ?thesis ``` lp15@60809 ` 542` ``` using s2 ``` lp15@60809 ` 543` ``` apply (auto simp: path_integrable_on) ``` lp15@60809 ` 544` ``` apply (rule integrable_spike_finite [of "{0,1} \ s2", OF _ _ *]) ``` lp15@60809 ` 545` ``` apply (auto simp: joinpaths_def scaleR_conv_of_real g2) ``` lp15@60809 ` 546` ``` done ``` lp15@60809 ` 547` ```qed ``` lp15@60809 ` 548` lp15@60809 ` 549` ```lemma path_integrable_join [simp]: ``` lp15@60809 ` 550` ``` shows ``` lp15@60809 ` 551` ``` "\valid_path g1; valid_path g2\ ``` lp15@60809 ` 552` ``` \ f path_integrable_on (g1 +++ g2) \ f path_integrable_on g1 \ f path_integrable_on g2" ``` lp15@60809 ` 553` ```using path_integrable_joinD1 path_integrable_joinD2 path_integrable_joinI by blast ``` lp15@60809 ` 554` lp15@60809 ` 555` ```lemma path_integral_join [simp]: ``` lp15@60809 ` 556` ``` shows ``` lp15@60809 ` 557` ``` "\f path_integrable_on g1; f path_integrable_on g2; valid_path g1; valid_path g2\ ``` lp15@60809 ` 558` ``` \ path_integral (g1 +++ g2) f = path_integral g1 f + path_integral g2 f" ``` lp15@60809 ` 559` ``` by (simp add: has_path_integral_integral has_path_integral_join path_integral_unique) ``` lp15@60809 ` 560` lp15@60809 ` 561` lp15@60809 ` 562` ```subsection\Shifting the starting point of a (closed) path\ ``` lp15@60809 ` 563` lp15@60809 ` 564` ```lemma shiftpath_alt_def: "shiftpath a f = (\x. if x \ 1-a then f (a + x) else f (a + x - 1))" ``` lp15@60809 ` 565` ``` by (auto simp: shiftpath_def) ``` lp15@60809 ` 566` lp15@60809 ` 567` ```lemma valid_path_shiftpath [intro]: ``` lp15@60809 ` 568` ``` assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@60809 ` 569` ``` shows "valid_path(shiftpath a g)" ``` lp15@60809 ` 570` ``` using assms ``` lp15@60809 ` 571` ``` apply (auto simp: valid_path_def shiftpath_alt_def) ``` lp15@60809 ` 572` ``` apply (rule piecewise_differentiable_cases) ``` lp15@60809 ` 573` ``` apply (auto simp: algebra_simps) ``` lp15@60809 ` 574` ``` apply (rule piecewise_differentiable_affine [of g 1 a, simplified o_def scaleR_one]) ``` lp15@60809 ` 575` ``` apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset) ``` lp15@60809 ` 576` ``` apply (rule piecewise_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps]) ``` lp15@60809 ` 577` ``` apply (auto simp: pathfinish_def pathstart_def elim: piecewise_differentiable_on_subset) ``` lp15@60809 ` 578` ``` done ``` lp15@60809 ` 579` lp15@60809 ` 580` ```lemma has_path_integral_shiftpath: ``` lp15@60809 ` 581` ``` assumes f: "(f has_path_integral i) g" "valid_path g" ``` lp15@60809 ` 582` ``` and a: "a \ {0..1}" ``` lp15@60809 ` 583` ``` shows "(f has_path_integral i) (shiftpath a g)" ``` lp15@60809 ` 584` ```proof - ``` lp15@60809 ` 585` ``` obtain s ``` lp15@60809 ` 586` ``` where s: "finite s" and g: "\x\{0..1} - s. g differentiable at x" ``` lp15@60809 ` 587` ``` using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 588` ``` have *: "((\x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" ``` lp15@60809 ` 589` ``` using assms by (auto simp: has_path_integral) ``` lp15@60809 ` 590` ``` then have i: "i = integral {a..1} (\x. f (g x) * vector_derivative g (at x)) + ``` lp15@60809 ` 591` ``` integral {0..a} (\x. f (g x) * vector_derivative g (at x))" ``` lp15@60809 ` 592` ``` apply (rule has_integral_unique) ``` lp15@60809 ` 593` ``` apply (subst add.commute) ``` lp15@60809 ` 594` ``` apply (subst Integration.integral_combine) ``` lp15@60809 ` 595` ``` using assms * integral_unique by auto ``` lp15@60809 ` 596` ``` { fix x ``` lp15@60809 ` 597` ``` have "0 \ x \ x + a < 1 \ x \ (\x. x - a) ` s \ ``` lp15@60809 ` 598` ``` vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))" ``` lp15@60809 ` 599` ``` unfolding shiftpath_def ``` lp15@60809 ` 600` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist(1-a) x" _ "(\x. g(a+x))"]]) ``` lp15@60809 ` 601` ``` apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm) ``` lp15@60809 ` 602` ``` apply (rule vector_diff_chain_at [of "\x. x+a" 1 _ g, simplified o_def scaleR_one]) ``` lp15@60809 ` 603` ``` apply (intro derivative_eq_intros | simp)+ ``` lp15@60809 ` 604` ``` using g ``` lp15@60809 ` 605` ``` apply (drule_tac x="x+a" in bspec) ``` lp15@60809 ` 606` ``` using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) ``` lp15@60809 ` 607` ``` done ``` lp15@60809 ` 608` ``` } note vd1 = this ``` lp15@60809 ` 609` ``` { fix x ``` lp15@60809 ` 610` ``` have "1 < x + a \ x \ 1 \ x \ (\x. x - a + 1) ` s \ ``` lp15@60809 ` 611` ``` vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))" ``` lp15@60809 ` 612` ``` unfolding shiftpath_def ``` lp15@60809 ` 613` ``` apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist (1-a) x" _ "(\x. g(a+x-1))"]]) ``` lp15@60809 ` 614` ``` apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm) ``` lp15@60809 ` 615` ``` apply (rule vector_diff_chain_at [of "\x. x+a-1" 1 _ g, simplified o_def scaleR_one]) ``` lp15@60809 ` 616` ``` apply (intro derivative_eq_intros | simp)+ ``` lp15@60809 ` 617` ``` using g ``` lp15@60809 ` 618` ``` apply (drule_tac x="x+a-1" in bspec) ``` lp15@60809 ` 619` ``` using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute) ``` lp15@60809 ` 620` ``` done ``` lp15@60809 ` 621` ``` } note vd2 = this ``` lp15@60809 ` 622` ``` have va1: "(\x. f (g x) * vector_derivative g (at x)) integrable_on ({a..1})" ``` lp15@60809 ` 623` ``` using * a by (fastforce intro: integrable_subinterval_real) ``` lp15@60809 ` 624` ``` have v0a: "(\x. f (g x) * vector_derivative g (at x)) integrable_on ({0..a})" ``` lp15@60809 ` 625` ``` apply (rule integrable_subinterval_real) ``` lp15@60809 ` 626` ``` using * a by auto ``` lp15@60809 ` 627` ``` have "((\x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x)) ``` lp15@60809 ` 628` ``` has_integral integral {a..1} (\x. f (g x) * vector_derivative g (at x))) {0..1 - a}" ``` lp15@60809 ` 629` ``` apply (rule has_integral_spike_finite ``` lp15@60809 ` 630` ``` [where s = "{1-a} \ (\x. x-a) ` s" and f = "\x. f(g(a+x)) * vector_derivative g (at(a+x))"]) ``` lp15@60809 ` 631` ``` using s apply blast ``` lp15@60809 ` 632` ``` using a apply (auto simp: algebra_simps vd1) ``` lp15@60809 ` 633` ``` apply (force simp: shiftpath_def add.commute) ``` lp15@60809 ` 634` ``` using has_integral_affinity [where m=1 and c=a, simplified, OF integrable_integral [OF va1]] ``` lp15@60809 ` 635` ``` apply (simp add: image_affinity_atLeastAtMost_diff [where m=1 and c=a, simplified] add.commute) ``` lp15@60809 ` 636` ``` done ``` lp15@60809 ` 637` ``` moreover ``` lp15@60809 ` 638` ``` have "((\x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x)) ``` lp15@60809 ` 639` ``` has_integral integral {0..a} (\x. f (g x) * vector_derivative g (at x))) {1 - a..1}" ``` lp15@60809 ` 640` ``` apply (rule has_integral_spike_finite ``` lp15@60809 ` 641` ``` [where s = "{1-a} \ (\x. x-a+1) ` s" and f = "\x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"]) ``` lp15@60809 ` 642` ``` using s apply blast ``` lp15@60809 ` 643` ``` using a apply (auto simp: algebra_simps vd2) ``` lp15@60809 ` 644` ``` apply (force simp: shiftpath_def add.commute) ``` lp15@60809 ` 645` ``` using has_integral_affinity [where m=1 and c="a-1", simplified, OF integrable_integral [OF v0a]] ``` lp15@60809 ` 646` ``` apply (simp add: image_affinity_atLeastAtMost [where m=1 and c="1-a", simplified]) ``` lp15@60809 ` 647` ``` apply (simp add: algebra_simps) ``` lp15@60809 ` 648` ``` done ``` lp15@60809 ` 649` ``` ultimately show ?thesis ``` lp15@60809 ` 650` ``` using a ``` lp15@60809 ` 651` ``` by (auto simp: i has_path_integral intro: has_integral_combine [where c = "1-a"]) ``` lp15@60809 ` 652` ```qed ``` lp15@60809 ` 653` lp15@60809 ` 654` ```lemma has_path_integral_shiftpath_D: ``` lp15@60809 ` 655` ``` assumes "(f has_path_integral i) (shiftpath a g)" ``` lp15@60809 ` 656` ``` "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@60809 ` 657` ``` shows "(f has_path_integral i) g" ``` lp15@60809 ` 658` ```proof - ``` lp15@60809 ` 659` ``` obtain s ``` lp15@60809 ` 660` ``` where s: "finite s" and g: "\x\{0..1} - s. g differentiable at x" ``` lp15@60809 ` 661` ``` using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 662` ``` { fix x ``` lp15@60809 ` 663` ``` assume x: "0 < x" "x < 1" "x \ s" ``` lp15@60809 ` 664` ``` then have gx: "g differentiable at x" ``` lp15@60809 ` 665` ``` using g by auto ``` lp15@60809 ` 666` ``` have "vector_derivative g (at x within {0..1}) = ``` lp15@60809 ` 667` ``` vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})" ``` lp15@60809 ` 668` ``` apply (rule vector_derivative_at_within_ivl ``` lp15@60809 ` 669` ``` [OF has_vector_derivative_transform_within_open ``` lp15@60809 ` 670` ``` [of "{0<..<1}-s" _ "(shiftpath (1 - a) (shiftpath a g))"]]) ``` lp15@60809 ` 671` ``` using s g assms x ``` lp15@60809 ` 672` ``` apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath ``` lp15@60809 ` 673` ``` vector_derivative_within_interior vector_derivative_works [symmetric]) ``` lp15@60809 ` 674` ``` apply (rule Derivative.differentiable_transform_at [of "min x (1-x)", OF _ _ gx]) ``` lp15@60809 ` 675` ``` apply (auto simp: dist_real_def shiftpath_shiftpath abs_if) ``` lp15@60809 ` 676` ``` done ``` lp15@60809 ` 677` ``` } note vd = this ``` lp15@60809 ` 678` ``` have fi: "(f has_path_integral i) (shiftpath (1 - a) (shiftpath a g))" ``` lp15@60809 ` 679` ``` using assms by (auto intro!: has_path_integral_shiftpath) ``` lp15@60809 ` 680` ``` show ?thesis ``` lp15@60809 ` 681` ``` apply (simp add: has_path_integral_def) ``` lp15@60809 ` 682` ``` apply (rule has_integral_spike_finite [of "{0,1} \ s", OF _ _ fi [unfolded has_path_integral_def]]) ``` lp15@60809 ` 683` ``` using s assms vd ``` lp15@60809 ` 684` ``` apply (auto simp: Path_Connected.shiftpath_shiftpath) ``` lp15@60809 ` 685` ``` done ``` lp15@60809 ` 686` ```qed ``` lp15@60809 ` 687` lp15@60809 ` 688` ```lemma has_path_integral_shiftpath_eq: ``` lp15@60809 ` 689` ``` assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@60809 ` 690` ``` shows "(f has_path_integral i) (shiftpath a g) \ (f has_path_integral i) g" ``` lp15@60809 ` 691` ``` using assms has_path_integral_shiftpath has_path_integral_shiftpath_D by blast ``` lp15@60809 ` 692` lp15@60809 ` 693` ```lemma path_integral_shiftpath: ``` lp15@60809 ` 694` ``` assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" ``` lp15@60809 ` 695` ``` shows "path_integral (shiftpath a g) f = path_integral g f" ``` lp15@60809 ` 696` ``` using assms by (simp add: path_integral_def has_path_integral_shiftpath_eq) ``` lp15@60809 ` 697` lp15@60809 ` 698` lp15@60809 ` 699` ```subsection\More about straight-line paths\ ``` lp15@60809 ` 700` lp15@60809 ` 701` ```lemma has_vector_derivative_linepath_within: ``` lp15@60809 ` 702` ``` "(linepath a b has_vector_derivative (b - a)) (at x within s)" ``` lp15@60809 ` 703` ```apply (simp add: linepath_def has_vector_derivative_def algebra_simps) ``` lp15@60809 ` 704` ```apply (rule derivative_eq_intros | simp)+ ``` lp15@60809 ` 705` ```done ``` lp15@60809 ` 706` lp15@60809 ` 707` ```lemma valid_path_linepath [iff]: "valid_path (linepath a b)" ``` lp15@60809 ` 708` ``` apply (simp add: valid_path_def) ``` lp15@60809 ` 709` ``` apply (rule differentiable_on_imp_piecewise_differentiable) ``` lp15@60809 ` 710` ``` apply (simp add: differentiable_on_def differentiable_def) ``` lp15@60809 ` 711` ``` using has_vector_derivative_def has_vector_derivative_linepath_within by blast ``` lp15@60809 ` 712` lp15@60809 ` 713` ```lemma vector_derivative_linepath_within: ``` lp15@60809 ` 714` ``` "x \ {0..1} \ vector_derivative (linepath a b) (at x within {0..1}) = b - a" ``` lp15@60809 ` 715` ``` apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified]) ``` lp15@60809 ` 716` ``` apply (auto simp: has_vector_derivative_linepath_within) ``` lp15@60809 ` 717` ``` done ``` lp15@60809 ` 718` lp15@60809 ` 719` ```lemma vector_derivative_linepath_at: "vector_derivative (linepath a b) (at x) = b - a" ``` lp15@60809 ` 720` ``` by (simp add: has_vector_derivative_linepath_within vector_derivative_at) ``` lp15@60809 ` 721` lp15@60809 ` 722` ```lemma has_path_integral_linepath: ``` lp15@60809 ` 723` ``` shows "(f has_path_integral i) (linepath a b) \ ``` lp15@60809 ` 724` ``` ((\x. f(linepath a b x) * (b - a)) has_integral i) {0..1}" ``` lp15@60809 ` 725` ``` by (simp add: has_path_integral vector_derivative_linepath_at) ``` lp15@60809 ` 726` lp15@60809 ` 727` ```lemma linepath_in_path: ``` lp15@60809 ` 728` ``` shows "x \ {0..1} \ linepath a b x \ closed_segment a b" ``` lp15@60809 ` 729` ``` by (auto simp: segment linepath_def) ``` lp15@60809 ` 730` lp15@60809 ` 731` ```lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b" ``` lp15@60809 ` 732` ``` by (auto simp: segment linepath_def) ``` lp15@60809 ` 733` lp15@60809 ` 734` ```lemma linepath_in_convex_hull: ``` lp15@60809 ` 735` ``` fixes x::real ``` lp15@60809 ` 736` ``` assumes a: "a \ convex hull s" ``` lp15@60809 ` 737` ``` and b: "b \ convex hull s" ``` lp15@60809 ` 738` ``` and x: "0\x" "x\1" ``` lp15@60809 ` 739` ``` shows "linepath a b x \ convex hull s" ``` lp15@60809 ` 740` ``` apply (rule closed_segment_subset_convex_hull [OF a b, THEN subsetD]) ``` lp15@60809 ` 741` ``` using x ``` lp15@60809 ` 742` ``` apply (auto simp: linepath_image_01 [symmetric]) ``` lp15@60809 ` 743` ``` done ``` lp15@60809 ` 744` lp15@60809 ` 745` ```lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b" ``` lp15@60809 ` 746` ``` by (simp add: linepath_def) ``` lp15@60809 ` 747` lp15@60809 ` 748` ```lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0" ``` lp15@60809 ` 749` ``` by (simp add: linepath_def) ``` lp15@60809 ` 750` lp15@60809 ` 751` ```lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1 - x)*a + x*b)" ``` lp15@60809 ` 752` ``` by (simp add: scaleR_conv_of_real linepath_def) ``` lp15@60809 ` 753` lp15@60809 ` 754` ```lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x" ``` lp15@60809 ` 755` ``` by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def) ``` lp15@60809 ` 756` lp15@60809 ` 757` ```lemma has_path_integral_trivial [iff]: "(f has_path_integral 0) (linepath a a)" ``` lp15@60809 ` 758` ``` by (simp add: has_path_integral_linepath) ``` lp15@60809 ` 759` lp15@60809 ` 760` ```lemma path_integral_trivial [simp]: "path_integral (linepath a a) f = 0" ``` lp15@60809 ` 761` ``` using has_path_integral_trivial path_integral_unique by blast ``` lp15@60809 ` 762` lp15@60809 ` 763` lp15@60809 ` 764` ```subsection\Relation to subpath construction\ ``` lp15@60809 ` 765` lp15@60809 ` 766` ```lemma valid_path_subpath: ``` lp15@60809 ` 767` ``` fixes g :: "real \ 'a :: real_normed_vector" ``` lp15@60809 ` 768` ``` assumes "valid_path g" "u \ {0..1}" "v \ {0..1}" ``` lp15@60809 ` 769` ``` shows "valid_path(subpath u v g)" ``` lp15@60809 ` 770` ```proof (cases "v=u") ``` lp15@60809 ` 771` ``` case True ``` lp15@60809 ` 772` ``` then show ?thesis ``` lp15@60809 ` 773` ``` by (simp add: valid_path_def subpath_def differentiable_on_def differentiable_on_imp_piecewise_differentiable) ``` lp15@60809 ` 774` ```next ``` lp15@60809 ` 775` ``` case False ``` lp15@60809 ` 776` ``` have "(g o (\x. ((v-u) * x + u))) piecewise_differentiable_on {0..1}" ``` lp15@60809 ` 777` ``` apply (rule piecewise_differentiable_compose) ``` lp15@60809 ` 778` ``` apply (simp add: differentiable_on_def differentiable_on_imp_piecewise_differentiable) ``` lp15@60809 ` 779` ``` apply (simp add: image_affinity_atLeastAtMost) ``` lp15@60809 ` 780` ``` using assms False ``` lp15@60809 ` 781` ``` apply (auto simp: algebra_simps valid_path_def piecewise_differentiable_on_subset) ``` lp15@60809 ` 782` ``` apply (subst Int_commute) ``` lp15@60809 ` 783` ``` apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI) ``` lp15@60809 ` 784` ``` done ``` lp15@60809 ` 785` ``` then show ?thesis ``` lp15@60809 ` 786` ``` by (auto simp: o_def valid_path_def subpath_def) ``` lp15@60809 ` 787` ```qed ``` lp15@60809 ` 788` lp15@60809 ` 789` ```lemma has_path_integral_subpath_refl [iff]: "(f has_path_integral 0) (subpath u u g)" ``` lp15@60809 ` 790` ``` by (simp add: has_path_integral subpath_def) ``` lp15@60809 ` 791` lp15@60809 ` 792` ```lemma path_integrable_subpath_refl [iff]: "f path_integrable_on (subpath u u g)" ``` lp15@60809 ` 793` ``` using has_path_integral_subpath_refl path_integrable_on_def by blast ``` lp15@60809 ` 794` lp15@60809 ` 795` ```lemma path_integral_subpath_refl [simp]: "path_integral (subpath u u g) f = 0" ``` lp15@60809 ` 796` ``` by (simp add: has_path_integral_subpath_refl path_integral_unique) ``` lp15@60809 ` 797` lp15@60809 ` 798` ```lemma has_path_integral_subpath: ``` lp15@60809 ` 799` ``` assumes f: "f path_integrable_on g" and g: "valid_path g" ``` lp15@60809 ` 800` ``` and uv: "u \ {0..1}" "v \ {0..1}" "u \ v" ``` lp15@60809 ` 801` ``` shows "(f has_path_integral integral {u..v} (\x. f(g x) * vector_derivative g (at x))) ``` lp15@60809 ` 802` ``` (subpath u v g)" ``` lp15@60809 ` 803` ```proof (cases "v=u") ``` lp15@60809 ` 804` ``` case True ``` lp15@60809 ` 805` ``` then show ?thesis ``` lp15@60809 ` 806` ``` using f by (simp add: path_integrable_on_def subpath_def has_path_integral) ``` lp15@60809 ` 807` ```next ``` lp15@60809 ` 808` ``` case False ``` lp15@60809 ` 809` ``` obtain s where s: "\x. x \ {0..1} - s \ g differentiable at x" and fs: "finite s" ``` lp15@60809 ` 810` ``` using g by (auto simp: valid_path_def piecewise_differentiable_on_def) (blast intro: that) ``` lp15@60809 ` 811` ``` have *: "((\x. f (g ((v - u) * x + u)) * vector_derivative g (at ((v - u) * x + u))) ``` lp15@60809 ` 812` ``` has_integral (1 / (v - u)) * integral {u..v} (\t. f (g t) * vector_derivative g (at t))) ``` lp15@60809 ` 813` ``` {0..1}" ``` lp15@60809 ` 814` ``` using f uv ``` lp15@60809 ` 815` ``` apply (simp add: path_integrable_on subpath_def has_path_integral) ``` lp15@60809 ` 816` ``` apply (drule integrable_on_subcbox [where a=u and b=v, simplified]) ``` lp15@60809 ` 817` ``` apply (simp_all add: has_integral_integral) ``` lp15@60809 ` 818` ``` apply (drule has_integral_affinity [where m="v-u" and c=u, simplified]) ``` lp15@60809 ` 819` ``` apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real) ``` lp15@60809 ` 820` ``` apply (simp add: divide_simps False) ``` lp15@60809 ` 821` ``` done ``` lp15@60809 ` 822` ``` { fix x ``` lp15@60809 ` 823` ``` have "x \ {0..1} \ ``` lp15@60809 ` 824` ``` x \ (\t. (v-u) *\<^sub>R t + u) -` s \ ``` lp15@60809 ` 825` ``` vector_derivative (\x. g ((v-u) * x + u)) (at x) = (v-u) *\<^sub>R vector_derivative g (at ((v-u) * x + u))" ``` lp15@60809 ` 826` ``` apply (rule vector_derivative_at [OF vector_diff_chain_at [simplified o_def]]) ``` lp15@60809 ` 827` ``` apply (intro derivative_eq_intros | simp)+ ``` lp15@60809 ` 828` ``` apply (cut_tac s [of "(v - u) * x + u"]) ``` lp15@60809 ` 829` ``` using uv mult_left_le [of x "v-u"] ``` lp15@60809 ` 830` ``` apply (auto simp: vector_derivative_works) ``` lp15@60809 ` 831` ``` done ``` lp15@60809 ` 832` ``` } note vd = this ``` lp15@60809 ` 833` ``` show ?thesis ``` lp15@60809 ` 834` ``` apply (cut_tac has_integral_cmul [OF *, where c = "v-u"]) ``` lp15@60809 ` 835` ``` using fs assms ``` lp15@60809 ` 836` ``` apply (simp add: False subpath_def has_path_integral) ``` lp15@60809 ` 837` ``` apply (rule_tac s = "(\t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite) ``` lp15@60809 ` 838` ``` apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real) ``` lp15@60809 ` 839` ``` done ``` lp15@60809 ` 840` ```qed ``` lp15@60809 ` 841` lp15@60809 ` 842` ```lemma path_integrable_subpath: ``` lp15@60809 ` 843` ``` assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" ``` lp15@60809 ` 844` ``` shows "f path_integrable_on (subpath u v g)" ``` lp15@60809 ` 845` ``` apply (cases u v rule: linorder_class.le_cases) ``` lp15@60809 ` 846` ``` apply (metis path_integrable_on_def has_path_integral_subpath [OF assms]) ``` lp15@60809 ` 847` ``` apply (subst reversepath_subpath [symmetric]) ``` lp15@60809 ` 848` ``` apply (rule path_integrable_reversepath) ``` lp15@60809 ` 849` ``` using assms apply (blast intro: valid_path_subpath) ``` lp15@60809 ` 850` ``` apply (simp add: path_integrable_on_def) ``` lp15@60809 ` 851` ``` using assms apply (blast intro: has_path_integral_subpath) ``` lp15@60809 ` 852` ``` done ``` lp15@60809 ` 853` lp15@60809 ` 854` ```lemma has_integral_integrable_integral: "(f has_integral i) s \ f integrable_on s \ integral s f = i" ``` lp15@60809 ` 855` ``` by blast ``` lp15@60809 ` 856` lp15@60809 ` 857` ```lemma has_integral_path_integral_subpath: ``` lp15@60809 ` 858` ``` assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" ``` lp15@60809 ` 859` ``` shows "(((\x. f(g x) * vector_derivative g (at x))) ``` lp15@60809 ` 860` ``` has_integral path_integral (subpath u v g) f) {u..v}" ``` lp15@60809 ` 861` ``` using assms ``` lp15@60809 ` 862` ``` apply (auto simp: has_integral_integrable_integral) ``` lp15@60809 ` 863` ``` apply (rule integrable_on_subcbox [where a=u and b=v and s = "{0..1}", simplified]) ``` lp15@60809 ` 864` ``` apply (auto simp: path_integral_unique [OF has_path_integral_subpath] path_integrable_on) ``` lp15@60809 ` 865` ``` done ``` lp15@60809 ` 866` lp15@60809 ` 867` ```lemma path_integral_subpath_integral: ``` lp15@60809 ` 868` ``` assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" ``` lp15@60809 ` 869` ``` shows "path_integral (subpath u v g) f = ``` lp15@60809 ` 870` ``` integral {u..v} (\x. f(g x) * vector_derivative g (at x))" ``` lp15@60809 ` 871` ``` using assms has_path_integral_subpath path_integral_unique by blast ``` lp15@60809 ` 872` lp15@60809 ` 873` ```lemma path_integral_subpath_combine_less: ``` lp15@60809 ` 874` ``` assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "w \ {0..1}" ``` lp15@60809 ` 875` ``` "u {0..1}" "v \ {0..1}" "w \ {0..1}" ``` lp15@60809 ` 886` ``` shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f = ``` lp15@60809 ` 887` ``` path_integral (subpath u w g) f" ``` lp15@60809 ` 888` ```proof (cases "u\v \ v\w \ u\w") ``` lp15@60809 ` 889` ``` case True ``` lp15@60809 ` 890` ``` have *: "subpath v u g = reversepath(subpath u v g) \ ``` lp15@60809 ` 891` ``` subpath w u g = reversepath(subpath u w g) \ ``` lp15@60809 ` 892` ``` subpath w v g = reversepath(subpath v w g)" ``` lp15@60809 ` 893` ``` by (auto simp: reversepath_subpath) ``` lp15@60809 ` 894` ``` have "u < v \ v < w \ ``` lp15@60809 ` 895` ``` u < w \ w < v \ ``` lp15@60809 ` 896` ``` v < u \ u < w \ ``` lp15@60809 ` 897` ``` v < w \ w < u \ ``` lp15@60809 ` 898` ``` w < u \ u < v \ ``` lp15@60809 ` 899` ``` w < v \ v < u" ``` lp15@60809 ` 900` ``` using True assms by linarith ``` lp15@60809 ` 901` ``` with assms show ?thesis ``` lp15@60809 ` 902` ``` using path_integral_subpath_combine_less [of f g u v w] ``` lp15@60809 ` 903` ``` path_integral_subpath_combine_less [of f g u w v] ``` lp15@60809 ` 904` ``` path_integral_subpath_combine_less [of f g v u w] ``` lp15@60809 ` 905` ``` path_integral_subpath_combine_less [of f g v w u] ``` lp15@60809 ` 906` ``` path_integral_subpath_combine_less [of f g w u v] ``` lp15@60809 ` 907` ``` path_integral_subpath_combine_less [of f g w v u] ``` lp15@60809 ` 908` ``` apply simp ``` lp15@60809 ` 909` ``` apply (elim disjE) ``` lp15@60809 ` 910` ``` apply (auto simp: * path_integral_reversepath path_integrable_subpath ``` lp15@60809 ` 911` ``` valid_path_reversepath valid_path_subpath algebra_simps) ``` lp15@60809 ` 912` ``` done ``` lp15@60809 ` 913` ```next ``` lp15@60809 ` 914` ``` case False ``` lp15@60809 ` 915` ``` then show ?thesis ``` lp15@60809 ` 916` ``` apply (auto simp: path_integral_subpath_refl) ``` lp15@60809 ` 917` ``` using assms ``` lp15@60809 ` 918` ``` by (metis eq_neg_iff_add_eq_0 path_integrable_subpath path_integral_reversepath reversepath_subpath valid_path_subpath) ``` lp15@60809 ` 919` ```qed ``` lp15@60809 ` 920` lp15@60809 ` 921` ```lemma path_integral_integral: ``` lp15@60809 ` 922` ``` shows "path_integral g f = integral {0..1} (\x. f (g x) * vector_derivative g (at x))" ``` lp15@60809 ` 923` ``` by (simp add: path_integral_def integral_def has_path_integral) ``` lp15@60809 ` 924` lp15@60809 ` 925` lp15@60809 ` 926` ```subsection\Segments via convex hulls\ ``` lp15@60809 ` 927` lp15@60809 ` 928` ```lemma segments_subset_convex_hull: ``` lp15@60809 ` 929` ``` "closed_segment a b \ (convex hull {a,b,c})" ``` lp15@60809 ` 930` ``` "closed_segment a c \ (convex hull {a,b,c})" ``` lp15@60809 ` 931` ``` "closed_segment b c \ (convex hull {a,b,c})" ``` lp15@60809 ` 932` ``` "closed_segment b a \ (convex hull {a,b,c})" ``` lp15@60809 ` 933` ``` "closed_segment c a \ (convex hull {a,b,c})" ``` lp15@60809 ` 934` ``` "closed_segment c b \ (convex hull {a,b,c})" ``` lp15@60809 ` 935` ```by (auto simp: segment_convex_hull linepath_of_real elim!: rev_subsetD [OF _ hull_mono]) ``` lp15@60809 ` 936` lp15@60809 ` 937` ```lemma midpoints_in_convex_hull: ``` lp15@60809 ` 938` ``` assumes "x \ convex hull s" "y \ convex hull s" ``` lp15@60809 ` 939` ``` shows "midpoint x y \ convex hull s" ``` lp15@60809 ` 940` ```proof - ``` lp15@60809 ` 941` ``` have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \ convex hull s" ``` lp15@60809 ` 942` ``` apply (rule mem_convex) ``` lp15@60809 ` 943` ``` using assms ``` lp15@60809 ` 944` ``` apply (auto simp: convex_convex_hull) ``` lp15@60809 ` 945` ``` done ``` lp15@60809 ` 946` ``` then show ?thesis ``` lp15@60809 ` 947` ``` by (simp add: midpoint_def algebra_simps) ``` lp15@60809 ` 948` ```qed ``` lp15@60809 ` 949` lp15@60809 ` 950` ```lemma convex_hull_subset: ``` lp15@60809 ` 951` ``` "s \ convex hull t \ convex hull s \ convex hull t" ``` lp15@60809 ` 952` ``` by (simp add: convex_convex_hull subset_hull) ``` lp15@60809 ` 953` lp15@60809 ` 954` ```lemma not_in_interior_convex_hull_3: ``` lp15@60809 ` 955` ``` fixes a :: "complex" ``` lp15@60809 ` 956` ``` shows "a \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 957` ``` "b \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 958` ``` "c \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 959` ``` by (auto simp: card_insert_le_m1 not_in_interior_convex_hull) ``` lp15@60809 ` 960` lp15@60809 ` 961` lp15@60809 ` 962` ```text\Cauchy's theorem where there's a primitive\ ``` lp15@60809 ` 963` lp15@60809 ` 964` ```lemma path_integral_primitive_lemma: ``` lp15@60809 ` 965` ``` fixes f :: "complex \ complex" and g :: "real \ complex" ``` lp15@60809 ` 966` ``` assumes "a \ b" ``` lp15@60809 ` 967` ``` and "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" ``` lp15@60809 ` 968` ``` and "g piecewise_differentiable_on {a..b}" "\x. x \ {a..b} \ g x \ s" ``` lp15@60809 ` 969` ``` shows "((\x. f'(g x) * vector_derivative g (at x within {a..b})) ``` lp15@60809 ` 970` ``` has_integral (f(g b) - f(g a))) {a..b}" ``` lp15@60809 ` 971` ```proof - ``` lp15@60809 ` 972` ``` obtain k where k: "finite k" "\x\{a..b} - k. g differentiable at x" and cg: "continuous_on {a..b} g" ``` lp15@60809 ` 973` ``` using assms by (auto simp: piecewise_differentiable_on_def) ``` lp15@60809 ` 974` ``` have cfg: "continuous_on {a..b} (\x. f (g x))" ``` lp15@60809 ` 975` ``` apply (rule continuous_on_compose [OF cg, unfolded o_def]) ``` lp15@60809 ` 976` ``` using assms ``` lp15@60809 ` 977` ``` apply (metis complex_differentiable_def complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff) ``` lp15@60809 ` 978` ``` done ``` lp15@60809 ` 979` ``` { fix x::real ``` lp15@60809 ` 980` ``` assume a: "a < x" and b: "x < b" and xk: "x \ k" ``` lp15@60809 ` 981` ``` then have "g differentiable at x within {a..b}" ``` lp15@60809 ` 982` ``` using k by (simp add: differentiable_at_withinI) ``` lp15@60809 ` 983` ``` then have "(g has_vector_derivative vector_derivative g (at x within {a..b})) (at x within {a..b})" ``` lp15@60809 ` 984` ``` by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real) ``` lp15@60809 ` 985` ``` then have gdiff: "(g has_derivative (\u. u * vector_derivative g (at x within {a..b}))) (at x within {a..b})" ``` lp15@60809 ` 986` ``` by (simp add: has_vector_derivative_def scaleR_conv_of_real) ``` lp15@60809 ` 987` ``` have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})" ``` lp15@60809 ` 988` ``` using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def) ``` lp15@60809 ` 989` ``` then have fdiff: "(f has_derivative op * (f' (g x))) (at (g x) within g ` {a..b})" ``` lp15@60809 ` 990` ``` by (simp add: has_field_derivative_def) ``` lp15@60809 ` 991` ``` have "((\x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})" ``` lp15@60809 ` 992` ``` using diff_chain_within [OF gdiff fdiff] ``` lp15@60809 ` 993` ``` by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac) ``` lp15@60809 ` 994` ``` } note * = this ``` lp15@60809 ` 995` ``` show ?thesis ``` lp15@60809 ` 996` ``` apply (rule fundamental_theorem_of_calculus_interior_strong) ``` lp15@60809 ` 997` ``` using k assms cfg * ``` lp15@60809 ` 998` ``` apply (auto simp: at_within_closed_interval) ``` lp15@60809 ` 999` ``` done ``` lp15@60809 ` 1000` ```qed ``` lp15@60809 ` 1001` lp15@60809 ` 1002` ```lemma path_integral_primitive: ``` lp15@60809 ` 1003` ``` assumes "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" ``` lp15@60809 ` 1004` ``` and "valid_path g" "path_image g \ s" ``` lp15@60809 ` 1005` ``` shows "(f' has_path_integral (f(pathfinish g) - f(pathstart g))) g" ``` lp15@60809 ` 1006` ``` using assms ``` lp15@60809 ` 1007` ``` apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_path_integral_def) ``` lp15@60809 ` 1008` ``` apply (auto intro!: path_integral_primitive_lemma [of 0 1 s]) ``` lp15@60809 ` 1009` ``` done ``` lp15@60809 ` 1010` lp15@60809 ` 1011` ```corollary Cauchy_theorem_primitive: ``` lp15@60809 ` 1012` ``` assumes "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" ``` lp15@60809 ` 1013` ``` and "valid_path g" "path_image g \ s" "pathfinish g = pathstart g" ``` lp15@60809 ` 1014` ``` shows "(f' has_path_integral 0) g" ``` lp15@60809 ` 1015` ``` using assms ``` lp15@60809 ` 1016` ``` by (metis diff_self path_integral_primitive) ``` lp15@60809 ` 1017` lp15@60809 ` 1018` lp15@60809 ` 1019` ```text\Existence of path integral for continuous function\ ``` lp15@60809 ` 1020` ```lemma path_integrable_continuous_linepath: ``` lp15@60809 ` 1021` ``` assumes "continuous_on (closed_segment a b) f" ``` lp15@60809 ` 1022` ``` shows "f path_integrable_on (linepath a b)" ``` lp15@60809 ` 1023` ```proof - ``` lp15@60809 ` 1024` ``` have "continuous_on {0..1} ((\x. f x * (b - a)) o linepath a b)" ``` lp15@60809 ` 1025` ``` apply (rule continuous_on_compose [OF continuous_on_linepath], simp add: linepath_image_01) ``` lp15@60809 ` 1026` ``` apply (rule continuous_intros | simp add: assms)+ ``` lp15@60809 ` 1027` ``` done ``` lp15@60809 ` 1028` ``` then show ?thesis ``` lp15@60809 ` 1029` ``` apply (simp add: path_integrable_on_def has_path_integral_def integrable_on_def [symmetric]) ``` lp15@60809 ` 1030` ``` apply (rule integrable_continuous [of 0 "1::real", simplified]) ``` lp15@60809 ` 1031` ``` apply (rule continuous_on_eq [where f = "\x. f(linepath a b x)*(b - a)"]) ``` lp15@60809 ` 1032` ``` apply (auto simp: vector_derivative_linepath_within) ``` lp15@60809 ` 1033` ``` done ``` lp15@60809 ` 1034` ```qed ``` lp15@60809 ` 1035` lp15@60809 ` 1036` ```lemma has_field_der_id: "((\x. x\<^sup>2 / 2) has_field_derivative x) (at x)" ``` lp15@60809 ` 1037` ``` by (rule has_derivative_imp_has_field_derivative) ``` lp15@60809 ` 1038` ``` (rule derivative_intros | simp)+ ``` lp15@60809 ` 1039` lp15@60809 ` 1040` ```lemma path_integral_id [simp]: "path_integral (linepath a b) (\y. y) = (b^2 - a^2)/2" ``` lp15@60809 ` 1041` ``` apply (rule path_integral_unique) ``` lp15@60809 ` 1042` ``` using path_integral_primitive [of UNIV "\x. x^2/2" "\x. x" "linepath a b"] ``` lp15@60809 ` 1043` ``` apply (auto simp: field_simps has_field_der_id) ``` lp15@60809 ` 1044` ``` done ``` lp15@60809 ` 1045` lp15@60809 ` 1046` ```lemma path_integrable_on_const [iff]: "(\x. c) path_integrable_on (linepath a b)" ``` lp15@60809 ` 1047` ``` by (simp add: continuous_on_const path_integrable_continuous_linepath) ``` lp15@60809 ` 1048` lp15@60809 ` 1049` ```lemma path_integrable_on_id [iff]: "(\x. x) path_integrable_on (linepath a b)" ``` lp15@60809 ` 1050` ``` by (simp add: continuous_on_id path_integrable_continuous_linepath) ``` lp15@60809 ` 1051` lp15@60809 ` 1052` lp15@60809 ` 1053` ```subsection\Arithmetical combining theorems\ ``` lp15@60809 ` 1054` lp15@60809 ` 1055` ```lemma has_path_integral_neg: ``` lp15@60809 ` 1056` ``` "(f has_path_integral i) g \ ((\x. -(f x)) has_path_integral (-i)) g" ``` lp15@60809 ` 1057` ``` by (simp add: has_integral_neg has_path_integral_def) ``` lp15@60809 ` 1058` lp15@60809 ` 1059` ```lemma has_path_integral_add: ``` lp15@60809 ` 1060` ``` "\(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\ ``` lp15@60809 ` 1061` ``` \ ((\x. f1 x + f2 x) has_path_integral (i1 + i2)) g" ``` lp15@60809 ` 1062` ``` by (simp add: has_integral_add has_path_integral_def algebra_simps) ``` lp15@60809 ` 1063` lp15@60809 ` 1064` ```lemma has_path_integral_diff: ``` lp15@60809 ` 1065` ``` shows "\(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\ ``` lp15@60809 ` 1066` ``` \ ((\x. f1 x - f2 x) has_path_integral (i1 - i2)) g" ``` lp15@60809 ` 1067` ``` by (simp add: has_integral_sub has_path_integral_def algebra_simps) ``` lp15@60809 ` 1068` lp15@60809 ` 1069` ```lemma has_path_integral_lmul: ``` lp15@60809 ` 1070` ``` shows "(f has_path_integral i) g ``` lp15@60809 ` 1071` ``` \ ((\x. c * (f x)) has_path_integral (c*i)) g" ``` lp15@60809 ` 1072` ```apply (simp add: has_path_integral_def) ``` lp15@60809 ` 1073` ```apply (drule has_integral_mult_right) ``` lp15@60809 ` 1074` ```apply (simp add: algebra_simps) ``` lp15@60809 ` 1075` ```done ``` lp15@60809 ` 1076` lp15@60809 ` 1077` ```lemma has_path_integral_rmul: ``` lp15@60809 ` 1078` ``` shows "(f has_path_integral i) g \ ((\x. (f x) * c) has_path_integral (i*c)) g" ``` lp15@60809 ` 1079` ```apply (drule has_path_integral_lmul) ``` lp15@60809 ` 1080` ```apply (simp add: mult.commute) ``` lp15@60809 ` 1081` ```done ``` lp15@60809 ` 1082` lp15@60809 ` 1083` ```lemma has_path_integral_div: ``` lp15@60809 ` 1084` ``` shows "(f has_path_integral i) g \ ((\x. f x/c) has_path_integral (i/c)) g" ``` lp15@60809 ` 1085` ``` by (simp add: field_class.field_divide_inverse) (metis has_path_integral_rmul) ``` lp15@60809 ` 1086` lp15@60809 ` 1087` ```lemma has_path_integral_eq: ``` lp15@60809 ` 1088` ``` shows ``` lp15@60809 ` 1089` ``` "\(f has_path_integral y) p; \x. x \ path_image p \ f x = g x\ \ (g has_path_integral y) p" ``` lp15@60809 ` 1090` ```apply (simp add: path_image_def has_path_integral_def) ``` lp15@60809 ` 1091` ```by (metis (no_types, lifting) image_eqI has_integral_eq) ``` lp15@60809 ` 1092` lp15@60809 ` 1093` ```lemma has_path_integral_bound_linepath: ``` lp15@60809 ` 1094` ``` assumes "(f has_path_integral i) (linepath a b)" ``` lp15@60809 ` 1095` ``` "0 \ B" "\x. x \ closed_segment a b \ norm(f x) \ B" ``` lp15@60809 ` 1096` ``` shows "norm i \ B * norm(b - a)" ``` lp15@60809 ` 1097` ```proof - ``` lp15@60809 ` 1098` ``` { fix x::real ``` lp15@60809 ` 1099` ``` assume x: "0 \ x" "x \ 1" ``` lp15@60809 ` 1100` ``` have "norm (f (linepath a b x)) * ``` lp15@60809 ` 1101` ``` norm (vector_derivative (linepath a b) (at x within {0..1})) \ B * norm (b - a)" ``` lp15@60809 ` 1102` ``` by (auto intro: mult_mono simp: assms linepath_in_path of_real_linepath vector_derivative_linepath_within x) ``` lp15@60809 ` 1103` ``` } note * = this ``` lp15@60809 ` 1104` ``` have "norm i \ (B * norm (b - a)) * content (cbox 0 (1::real))" ``` lp15@60809 ` 1105` ``` apply (rule has_integral_bound ``` lp15@60809 ` 1106` ``` [of _ "\x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"]) ``` lp15@60809 ` 1107` ``` using assms * unfolding has_path_integral_def ``` lp15@60809 ` 1108` ``` apply (auto simp: norm_mult) ``` lp15@60809 ` 1109` ``` done ``` lp15@60809 ` 1110` ``` then show ?thesis ``` lp15@60809 ` 1111` ``` by (auto simp: content_real) ``` lp15@60809 ` 1112` ```qed ``` lp15@60809 ` 1113` lp15@60809 ` 1114` ```(*UNUSED ``` lp15@60809 ` 1115` ```lemma has_path_integral_bound_linepath_strong: ``` lp15@60809 ` 1116` ``` fixes a :: real and f :: "complex \ real" ``` lp15@60809 ` 1117` ``` assumes "(f has_path_integral i) (linepath a b)" ``` lp15@60809 ` 1118` ``` "finite k" ``` lp15@60809 ` 1119` ``` "0 \ B" "\x::real. x \ closed_segment a b - k \ norm(f x) \ B" ``` lp15@60809 ` 1120` ``` shows "norm i \ B*norm(b - a)" ``` lp15@60809 ` 1121` ```*) ``` lp15@60809 ` 1122` lp15@60809 ` 1123` ```lemma has_path_integral_const_linepath: "((\x. c) has_path_integral c*(b - a))(linepath a b)" ``` lp15@60809 ` 1124` ``` unfolding has_path_integral_linepath ``` lp15@60809 ` 1125` ``` by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one) ``` lp15@60809 ` 1126` lp15@60809 ` 1127` ```lemma has_path_integral_0: "((\x. 0) has_path_integral 0) g" ``` lp15@60809 ` 1128` ``` by (simp add: has_path_integral_def) ``` lp15@60809 ` 1129` lp15@60809 ` 1130` ```lemma has_path_integral_is_0: ``` lp15@60809 ` 1131` ``` "(\z. z \ path_image g \ f z = 0) \ (f has_path_integral 0) g" ``` lp15@60809 ` 1132` ``` by (rule has_path_integral_eq [OF has_path_integral_0]) auto ``` lp15@60809 ` 1133` lp15@60809 ` 1134` ```lemma has_path_integral_setsum: ``` lp15@60809 ` 1135` ``` "\finite s; \a. a \ s \ (f a has_path_integral i a) p\ ``` lp15@60809 ` 1136` ``` \ ((\x. setsum (\a. f a x) s) has_path_integral setsum i s) p" ``` lp15@60809 ` 1137` ``` by (induction s rule: finite_induct) (auto simp: has_path_integral_0 has_path_integral_add) ``` lp15@60809 ` 1138` lp15@60809 ` 1139` lp15@60809 ` 1140` ```subsection \Operations on path integrals\ ``` lp15@60809 ` 1141` lp15@60809 ` 1142` ```lemma path_integral_const_linepath [simp]: "path_integral (linepath a b) (\x. c) = c*(b - a)" ``` lp15@60809 ` 1143` ``` by (rule path_integral_unique [OF has_path_integral_const_linepath]) ``` lp15@60809 ` 1144` lp15@60809 ` 1145` ```lemma path_integral_neg: ``` lp15@60809 ` 1146` ``` "f path_integrable_on g \ path_integral g (\x. -(f x)) = -(path_integral g f)" ``` lp15@60809 ` 1147` ``` by (simp add: path_integral_unique has_path_integral_integral has_path_integral_neg) ``` lp15@60809 ` 1148` lp15@60809 ` 1149` ```lemma path_integral_add: ``` lp15@60809 ` 1150` ``` "f1 path_integrable_on g \ f2 path_integrable_on g \ path_integral g (\x. f1 x + f2 x) = ``` lp15@60809 ` 1151` ``` path_integral g f1 + path_integral g f2" ``` lp15@60809 ` 1152` ``` by (simp add: path_integral_unique has_path_integral_integral has_path_integral_add) ``` lp15@60809 ` 1153` lp15@60809 ` 1154` ```lemma path_integral_diff: ``` lp15@60809 ` 1155` ``` "f1 path_integrable_on g \ f2 path_integrable_on g \ path_integral g (\x. f1 x - f2 x) = ``` lp15@60809 ` 1156` ``` path_integral g f1 - path_integral g f2" ``` lp15@60809 ` 1157` ``` by (simp add: path_integral_unique has_path_integral_integral has_path_integral_diff) ``` lp15@60809 ` 1158` lp15@60809 ` 1159` ```lemma path_integral_lmul: ``` lp15@60809 ` 1160` ``` shows "f path_integrable_on g ``` lp15@60809 ` 1161` ``` \ path_integral g (\x. c * f x) = c*path_integral g f" ``` lp15@60809 ` 1162` ``` by (simp add: path_integral_unique has_path_integral_integral has_path_integral_lmul) ``` lp15@60809 ` 1163` lp15@60809 ` 1164` ```lemma path_integral_rmul: ``` lp15@60809 ` 1165` ``` shows "f path_integrable_on g ``` lp15@60809 ` 1166` ``` \ path_integral g (\x. f x * c) = path_integral g f * c" ``` lp15@60809 ` 1167` ``` by (simp add: path_integral_unique has_path_integral_integral has_path_integral_rmul) ``` lp15@60809 ` 1168` lp15@60809 ` 1169` ```lemma path_integral_div: ``` lp15@60809 ` 1170` ``` shows "f path_integrable_on g ``` lp15@60809 ` 1171` ``` \ path_integral g (\x. f x / c) = path_integral g f / c" ``` lp15@60809 ` 1172` ``` by (simp add: path_integral_unique has_path_integral_integral has_path_integral_div) ``` lp15@60809 ` 1173` lp15@60809 ` 1174` ```lemma path_integral_eq: ``` lp15@60809 ` 1175` ``` "(\x. x \ path_image p \ f x = g x) \ path_integral p f = path_integral p g" ``` lp15@60809 ` 1176` ``` by (simp add: path_integral_def) (metis has_path_integral_eq) ``` lp15@60809 ` 1177` lp15@60809 ` 1178` ```lemma path_integral_eq_0: ``` lp15@60809 ` 1179` ``` "(\z. z \ path_image g \ f z = 0) \ path_integral g f = 0" ``` lp15@60809 ` 1180` ``` by (simp add: has_path_integral_is_0 path_integral_unique) ``` lp15@60809 ` 1181` lp15@60809 ` 1182` ```lemma path_integral_bound_linepath: ``` lp15@60809 ` 1183` ``` shows ``` lp15@60809 ` 1184` ``` "\f path_integrable_on (linepath a b); ``` lp15@60809 ` 1185` ``` 0 \ B; \x. x \ closed_segment a b \ norm(f x) \ B\ ``` lp15@60809 ` 1186` ``` \ norm(path_integral (linepath a b) f) \ B*norm(b - a)" ``` lp15@60809 ` 1187` ``` apply (rule has_path_integral_bound_linepath [of f]) ``` lp15@60809 ` 1188` ``` apply (auto simp: has_path_integral_integral) ``` lp15@60809 ` 1189` ``` done ``` lp15@60809 ` 1190` lp15@60809 ` 1191` ```lemma path_integral_0: "path_integral g (\x. 0) = 0" ``` lp15@60809 ` 1192` ``` by (simp add: path_integral_unique has_path_integral_0) ``` lp15@60809 ` 1193` lp15@60809 ` 1194` ```lemma path_integral_setsum: ``` lp15@60809 ` 1195` ``` "\finite s; \a. a \ s \ (f a) path_integrable_on p\ ``` lp15@60809 ` 1196` ``` \ path_integral p (\x. setsum (\a. f a x) s) = setsum (\a. path_integral p (f a)) s" ``` lp15@60809 ` 1197` ``` by (auto simp: path_integral_unique has_path_integral_setsum has_path_integral_integral) ``` lp15@60809 ` 1198` lp15@60809 ` 1199` ```lemma path_integrable_eq: ``` lp15@60809 ` 1200` ``` "\f path_integrable_on p; \x. x \ path_image p \ f x = g x\ \ g path_integrable_on p" ``` lp15@60809 ` 1201` ``` unfolding path_integrable_on_def ``` lp15@60809 ` 1202` ``` by (metis has_path_integral_eq) ``` lp15@60809 ` 1203` lp15@60809 ` 1204` lp15@60809 ` 1205` ```subsection \Arithmetic theorems for path integrability\ ``` lp15@60809 ` 1206` lp15@60809 ` 1207` ```lemma path_integrable_neg: ``` lp15@60809 ` 1208` ``` "f path_integrable_on g \ (\x. -(f x)) path_integrable_on g" ``` lp15@60809 ` 1209` ``` using has_path_integral_neg path_integrable_on_def by blast ``` lp15@60809 ` 1210` lp15@60809 ` 1211` ```lemma path_integrable_add: ``` lp15@60809 ` 1212` ``` "\f1 path_integrable_on g; f2 path_integrable_on g\ \ (\x. f1 x + f2 x) path_integrable_on g" ``` lp15@60809 ` 1213` ``` using has_path_integral_add path_integrable_on_def ``` lp15@60809 ` 1214` ``` by fastforce ``` lp15@60809 ` 1215` lp15@60809 ` 1216` ```lemma path_integrable_diff: ``` lp15@60809 ` 1217` ``` "\f1 path_integrable_on g; f2 path_integrable_on g\ \ (\x. f1 x - f2 x) path_integrable_on g" ``` lp15@60809 ` 1218` ``` using has_path_integral_diff path_integrable_on_def ``` lp15@60809 ` 1219` ``` by fastforce ``` lp15@60809 ` 1220` lp15@60809 ` 1221` ```lemma path_integrable_lmul: ``` lp15@60809 ` 1222` ``` "f path_integrable_on g \ (\x. c * f x) path_integrable_on g" ``` lp15@60809 ` 1223` ``` using has_path_integral_lmul path_integrable_on_def ``` lp15@60809 ` 1224` ``` by fastforce ``` lp15@60809 ` 1225` lp15@60809 ` 1226` ```lemma path_integrable_rmul: ``` lp15@60809 ` 1227` ``` "f path_integrable_on g \ (\x. f x * c) path_integrable_on g" ``` lp15@60809 ` 1228` ``` using has_path_integral_rmul path_integrable_on_def ``` lp15@60809 ` 1229` ``` by fastforce ``` lp15@60809 ` 1230` lp15@60809 ` 1231` ```lemma path_integrable_div: ``` lp15@60809 ` 1232` ``` "f path_integrable_on g \ (\x. f x / c) path_integrable_on g" ``` lp15@60809 ` 1233` ``` using has_path_integral_div path_integrable_on_def ``` lp15@60809 ` 1234` ``` by fastforce ``` lp15@60809 ` 1235` lp15@60809 ` 1236` ```lemma path_integrable_setsum: ``` lp15@60809 ` 1237` ``` "\finite s; \a. a \ s \ (f a) path_integrable_on p\ ``` lp15@60809 ` 1238` ``` \ (\x. setsum (\a. f a x) s) path_integrable_on p" ``` lp15@60809 ` 1239` ``` unfolding path_integrable_on_def ``` lp15@60809 ` 1240` ``` by (metis has_path_integral_setsum) ``` lp15@60809 ` 1241` lp15@60809 ` 1242` lp15@60809 ` 1243` ```subsection\Reversing a path integral\ ``` lp15@60809 ` 1244` lp15@60809 ` 1245` ```lemma has_path_integral_reverse_linepath: ``` lp15@60809 ` 1246` ``` "(f has_path_integral i) (linepath a b) ``` lp15@60809 ` 1247` ``` \ (f has_path_integral (-i)) (linepath b a)" ``` lp15@60809 ` 1248` ``` using has_path_integral_reversepath valid_path_linepath by fastforce ``` lp15@60809 ` 1249` lp15@60809 ` 1250` ```lemma path_integral_reverse_linepath: ``` lp15@60809 ` 1251` ``` "continuous_on (closed_segment a b) f ``` lp15@60809 ` 1252` ``` \ path_integral (linepath a b) f = - (path_integral(linepath b a) f)" ``` lp15@60809 ` 1253` ```apply (rule path_integral_unique) ``` lp15@60809 ` 1254` ```apply (rule has_path_integral_reverse_linepath) ``` lp15@60809 ` 1255` ```by (simp add: closed_segment_commute path_integrable_continuous_linepath has_path_integral_integral) ``` lp15@60809 ` 1256` lp15@60809 ` 1257` lp15@60809 ` 1258` ```(* Splitting a path integral in a flat way.*) ``` lp15@60809 ` 1259` lp15@60809 ` 1260` ```lemma has_path_integral_split: ``` lp15@60809 ` 1261` ``` assumes f: "(f has_path_integral i) (linepath a c)" "(f has_path_integral j) (linepath c b)" ``` lp15@60809 ` 1262` ``` and k: "0 \ k" "k \ 1" ``` lp15@60809 ` 1263` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@60809 ` 1264` ``` shows "(f has_path_integral (i + j)) (linepath a b)" ``` lp15@60809 ` 1265` ```proof (cases "k = 0 \ k = 1") ``` lp15@60809 ` 1266` ``` case True ``` lp15@60809 ` 1267` ``` then show ?thesis ``` lp15@60809 ` 1268` ``` using assms ``` lp15@60809 ` 1269` ``` apply auto ``` lp15@60809 ` 1270` ``` apply (metis add.left_neutral has_path_integral_trivial has_path_integral_unique) ``` lp15@60809 ` 1271` ``` apply (metis add.right_neutral has_path_integral_trivial has_path_integral_unique) ``` lp15@60809 ` 1272` ``` done ``` lp15@60809 ` 1273` ```next ``` lp15@60809 ` 1274` ``` case False ``` lp15@60809 ` 1275` ``` then have k: "0 < k" "k < 1" "complex_of_real k \ 1" ``` lp15@60809 ` 1276` ``` using assms apply auto ``` lp15@60809 ` 1277` ``` using of_real_eq_iff by fastforce ``` lp15@60809 ` 1278` ``` have c': "c = k *\<^sub>R (b - a) + a" ``` lp15@60809 ` 1279` ``` by (metis diff_add_cancel c) ``` lp15@60809 ` 1280` ``` have bc: "(b - c) = (1 - k) *\<^sub>R (b - a)" ``` lp15@60809 ` 1281` ``` by (simp add: algebra_simps c') ``` lp15@60809 ` 1282` ``` { assume *: "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R c) * (c - a)) has_integral i) {0..1}" ``` lp15@60809 ` 1283` ``` have **: "\x. ((k - x) / k) *\<^sub>R a + (x / k) *\<^sub>R c = (1 - x) *\<^sub>R a + x *\<^sub>R b" ``` lp15@60809 ` 1284` ``` using False ``` lp15@60809 ` 1285` ``` apply (simp add: c' algebra_simps) ``` lp15@60809 ` 1286` ``` apply (simp add: real_vector.scale_left_distrib [symmetric] divide_simps) ``` lp15@60809 ` 1287` ``` done ``` lp15@60809 ` 1288` ``` have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}" ``` lp15@60809 ` 1289` ``` using * k ``` lp15@60809 ` 1290` ``` apply - ``` lp15@60809 ` 1291` ``` apply (drule has_integral_affinity [of _ _ 0 "1::real" "inverse k" "0", simplified]) ``` lp15@60809 ` 1292` ``` apply (simp_all add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost ** c) ``` lp15@60809 ` 1293` ``` apply (drule Integration.has_integral_cmul [where c = "inverse k"]) ``` lp15@60809 ` 1294` ``` apply (simp add: Integration.has_integral_cmul) ``` lp15@60809 ` 1295` ``` done ``` lp15@60809 ` 1296` ``` } note fi = this ``` lp15@60809 ` 1297` ``` { assume *: "((\x. f ((1 - x) *\<^sub>R c + x *\<^sub>R b) * (b - c)) has_integral j) {0..1}" ``` lp15@60809 ` 1298` ``` have **: "\x. (((1 - x) / (1 - k)) *\<^sub>R c + ((x - k) / (1 - k)) *\<^sub>R b) = ((1 - x) *\<^sub>R a + x *\<^sub>R b)" ``` lp15@60809 ` 1299` ``` using k ``` lp15@60809 ` 1300` ``` apply (simp add: c' field_simps) ``` lp15@60809 ` 1301` ``` apply (simp add: scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 1302` ``` apply (simp add: field_simps) ``` lp15@60809 ` 1303` ``` done ``` lp15@60809 ` 1304` ``` have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral j) {k..1}" ``` lp15@60809 ` 1305` ``` using * k ``` lp15@60809 ` 1306` ``` apply - ``` lp15@60809 ` 1307` ``` apply (drule has_integral_affinity [of _ _ 0 "1::real" "inverse(1 - k)" "-(k/(1 - k))", simplified]) ``` lp15@60809 ` 1308` ``` apply (simp_all add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc) ``` lp15@60809 ` 1309` ``` apply (drule Integration.has_integral_cmul [where k = "(1 - k) *\<^sub>R j" and c = "inverse (1 - k)"]) ``` lp15@60809 ` 1310` ``` apply (simp add: Integration.has_integral_cmul) ``` lp15@60809 ` 1311` ``` done ``` lp15@60809 ` 1312` ``` } note fj = this ``` lp15@60809 ` 1313` ``` show ?thesis ``` lp15@60809 ` 1314` ``` using f k ``` lp15@60809 ` 1315` ``` apply (simp add: has_path_integral_linepath) ``` lp15@60809 ` 1316` ``` apply (simp add: linepath_def) ``` lp15@60809 ` 1317` ``` apply (rule has_integral_combine [OF _ _ fi fj], simp_all) ``` lp15@60809 ` 1318` ``` done ``` lp15@60809 ` 1319` ```qed ``` lp15@60809 ` 1320` lp15@60809 ` 1321` ```lemma continuous_on_closed_segment_transform: ``` lp15@60809 ` 1322` ``` assumes f: "continuous_on (closed_segment a b) f" ``` lp15@60809 ` 1323` ``` and k: "0 \ k" "k \ 1" ``` lp15@60809 ` 1324` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@60809 ` 1325` ``` shows "continuous_on (closed_segment a c) f" ``` lp15@60809 ` 1326` ```proof - ``` lp15@60809 ` 1327` ``` have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b" ``` lp15@60809 ` 1328` ``` using c by (simp add: algebra_simps) ``` lp15@60809 ` 1329` ``` show "continuous_on (closed_segment a c) f" ``` lp15@60809 ` 1330` ``` apply (rule continuous_on_subset [OF f]) ``` lp15@60809 ` 1331` ``` apply (simp add: segment_convex_hull) ``` lp15@60809 ` 1332` ``` apply (rule convex_hull_subset) ``` lp15@60809 ` 1333` ``` using assms ``` lp15@60809 ` 1334` ``` apply (auto simp: hull_inc c' Convex.mem_convex) ``` lp15@60809 ` 1335` ``` done ``` lp15@60809 ` 1336` ```qed ``` lp15@60809 ` 1337` lp15@60809 ` 1338` ```lemma path_integral_split: ``` lp15@60809 ` 1339` ``` assumes f: "continuous_on (closed_segment a b) f" ``` lp15@60809 ` 1340` ``` and k: "0 \ k" "k \ 1" ``` lp15@60809 ` 1341` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@60809 ` 1342` ``` shows "path_integral(linepath a b) f = path_integral(linepath a c) f + path_integral(linepath c b) f" ``` lp15@60809 ` 1343` ```proof - ``` lp15@60809 ` 1344` ``` have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b" ``` lp15@60809 ` 1345` ``` using c by (simp add: algebra_simps) ``` lp15@60809 ` 1346` ``` have *: "continuous_on (closed_segment a c) f" "continuous_on (closed_segment c b) f" ``` lp15@60809 ` 1347` ``` apply (rule_tac [!] continuous_on_subset [OF f]) ``` lp15@60809 ` 1348` ``` apply (simp_all add: segment_convex_hull) ``` lp15@60809 ` 1349` ``` apply (rule_tac [!] convex_hull_subset) ``` lp15@60809 ` 1350` ``` using assms ``` lp15@60809 ` 1351` ``` apply (auto simp: hull_inc c' Convex.mem_convex) ``` lp15@60809 ` 1352` ``` done ``` lp15@60809 ` 1353` ``` show ?thesis ``` lp15@60809 ` 1354` ``` apply (rule path_integral_unique) ``` lp15@60809 ` 1355` ``` apply (rule has_path_integral_split [OF has_path_integral_integral has_path_integral_integral k c]) ``` lp15@60809 ` 1356` ``` apply (rule path_integrable_continuous_linepath *)+ ``` lp15@60809 ` 1357` ``` done ``` lp15@60809 ` 1358` ```qed ``` lp15@60809 ` 1359` lp15@60809 ` 1360` ```lemma path_integral_split_linepath: ``` lp15@60809 ` 1361` ``` assumes f: "continuous_on (closed_segment a b) f" ``` lp15@60809 ` 1362` ``` and c: "c \ closed_segment a b" ``` lp15@60809 ` 1363` ``` shows "path_integral(linepath a b) f = path_integral(linepath a c) f + path_integral(linepath c b) f" ``` lp15@60809 ` 1364` ``` using c ``` lp15@60809 ` 1365` ``` by (auto simp: closed_segment_def algebra_simps intro!: path_integral_split [OF f]) ``` lp15@60809 ` 1366` lp15@60809 ` 1367` ```(* The special case of midpoints used in the main quadrisection.*) ``` lp15@60809 ` 1368` lp15@60809 ` 1369` ```lemma has_path_integral_midpoint: ``` lp15@60809 ` 1370` ``` assumes "(f has_path_integral i) (linepath a (midpoint a b))" ``` lp15@60809 ` 1371` ``` "(f has_path_integral j) (linepath (midpoint a b) b)" ``` lp15@60809 ` 1372` ``` shows "(f has_path_integral (i + j)) (linepath a b)" ``` lp15@60809 ` 1373` ``` apply (rule has_path_integral_split [where c = "midpoint a b" and k = "1/2"]) ``` lp15@60809 ` 1374` ``` using assms ``` lp15@60809 ` 1375` ``` apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) ``` lp15@60809 ` 1376` ``` done ``` lp15@60809 ` 1377` lp15@60809 ` 1378` ```lemma path_integral_midpoint: ``` lp15@60809 ` 1379` ``` "continuous_on (closed_segment a b) f ``` lp15@60809 ` 1380` ``` \ path_integral (linepath a b) f = ``` lp15@60809 ` 1381` ``` path_integral (linepath a (midpoint a b)) f + path_integral (linepath (midpoint a b) b) f" ``` lp15@60809 ` 1382` ``` apply (rule path_integral_split [where c = "midpoint a b" and k = "1/2"]) ``` lp15@60809 ` 1383` ``` using assms ``` lp15@60809 ` 1384` ``` apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) ``` lp15@60809 ` 1385` ``` done ``` lp15@60809 ` 1386` lp15@60809 ` 1387` lp15@60809 ` 1388` ```text\A couple of special case lemmas that are useful below\ ``` lp15@60809 ` 1389` lp15@60809 ` 1390` ```lemma triangle_linear_has_chain_integral: ``` lp15@60809 ` 1391` ``` "((\x. m*x + d) has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 1392` ``` apply (rule Cauchy_theorem_primitive [of UNIV "\x. m/2 * x^2 + d*x"]) ``` lp15@60809 ` 1393` ``` apply (auto intro!: derivative_eq_intros) ``` lp15@60809 ` 1394` ``` done ``` lp15@60809 ` 1395` lp15@60809 ` 1396` ```lemma has_chain_integral_chain_integral3: ``` lp15@60809 ` 1397` ``` "(f has_path_integral i) (linepath a b +++ linepath b c +++ linepath c d) ``` lp15@60809 ` 1398` ``` \ path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c d) f = i" ``` lp15@60809 ` 1399` ``` apply (subst path_integral_unique [symmetric], assumption) ``` lp15@60809 ` 1400` ``` apply (drule has_path_integral_integrable) ``` lp15@60809 ` 1401` ``` apply (simp add: valid_path_join) ``` lp15@60809 ` 1402` ``` done ``` lp15@60809 ` 1403` lp15@60809 ` 1404` ```subsection\Reversing the order in a double path integral\ ``` lp15@60809 ` 1405` lp15@60809 ` 1406` ```text\The condition is stronger than needed but it's often true in typical situations\ ``` lp15@60809 ` 1407` lp15@60809 ` 1408` ```lemma fst_im_cbox [simp]: "cbox c d \ {} \ (fst ` cbox (a,c) (b,d)) = cbox a b" ``` lp15@60809 ` 1409` ``` by (auto simp: cbox_Pair_eq) ``` lp15@60809 ` 1410` lp15@60809 ` 1411` ```lemma snd_im_cbox [simp]: "cbox a b \ {} \ (snd ` cbox (a,c) (b,d)) = cbox c d" ``` lp15@60809 ` 1412` ``` by (auto simp: cbox_Pair_eq) ``` lp15@60809 ` 1413` lp15@60809 ` 1414` ```lemma path_integral_swap: ``` lp15@60809 ` 1415` ``` assumes fcon: "continuous_on (path_image g \ path_image h) (\(y1,y2). f y1 y2)" ``` lp15@60809 ` 1416` ``` and vp: "valid_path g" "valid_path h" ``` lp15@60809 ` 1417` ``` and gvcon: "continuous_on {0..1} (\t. vector_derivative g (at t))" ``` lp15@60809 ` 1418` ``` and hvcon: "continuous_on {0..1} (\t. vector_derivative h (at t))" ``` lp15@60809 ` 1419` ``` shows "path_integral g (\w. path_integral h (f w)) = ``` lp15@60809 ` 1420` ``` path_integral h (\z. path_integral g (\w. f w z))" ``` lp15@60809 ` 1421` ```proof - ``` lp15@60809 ` 1422` ``` have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h" ``` lp15@60809 ` 1423` ``` using assms by (auto simp: valid_path_def piecewise_differentiable_on_def) ``` lp15@60809 ` 1424` ``` have fgh1: "\x. (\t. f (g x) (h t)) = (\(y1,y2). f y1 y2) o (\t. (g x, h t))" ``` lp15@60809 ` 1425` ``` by (rule ext) simp ``` lp15@60809 ` 1426` ``` have fgh2: "\x. (\t. f (g t) (h x)) = (\(y1,y2). f y1 y2) o (\t. (g t, h x))" ``` lp15@60809 ` 1427` ``` by (rule ext) simp ``` lp15@60809 ` 1428` ``` have fcon_im1: "\x. 0 \ x \ x \ 1 \ continuous_on ((\t. (g x, h t)) ` {0..1}) (\(x, y). f x y)" ``` lp15@60809 ` 1429` ``` by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def) ``` lp15@60809 ` 1430` ``` have fcon_im2: "\x. 0 \ x \ x \ 1 \ continuous_on ((\t. (g t, h x)) ` {0..1}) (\(x, y). f x y)" ``` lp15@60809 ` 1431` ``` by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def) ``` lp15@60809 ` 1432` ``` have vdg: "\y. y \ {0..1} \ (\x. f (g x) (h y) * vector_derivative g (at x)) integrable_on {0..1}" ``` lp15@60809 ` 1433` ``` apply (rule integrable_continuous_real) ``` lp15@60809 ` 1434` ``` apply (rule continuous_on_mult [OF _ gvcon]) ``` lp15@60809 ` 1435` ``` apply (subst fgh2) ``` lp15@60809 ` 1436` ``` apply (rule fcon_im2 gcon continuous_intros | simp)+ ``` lp15@60809 ` 1437` ``` done ``` lp15@60809 ` 1438` ``` have "(\z. vector_derivative g (at (fst z))) = (\x. vector_derivative g (at x)) o fst" ``` lp15@60809 ` 1439` ``` by auto ``` lp15@60809 ` 1440` ``` then have gvcon': "continuous_on (cbox (0, 0) (1, 1::real)) (\x. vector_derivative g (at (fst x)))" ``` lp15@60809 ` 1441` ``` apply (rule ssubst) ``` lp15@60809 ` 1442` ``` apply (rule continuous_intros | simp add: gvcon)+ ``` lp15@60809 ` 1443` ``` done ``` lp15@60809 ` 1444` ``` have "(\z. vector_derivative h (at (snd z))) = (\x. vector_derivative h (at x)) o snd" ``` lp15@60809 ` 1445` ``` by auto ``` lp15@60809 ` 1446` ``` then have hvcon': "continuous_on (cbox (0, 0) (1::real, 1)) (\x. vector_derivative h (at (snd x)))" ``` lp15@60809 ` 1447` ``` apply (rule ssubst) ``` lp15@60809 ` 1448` ``` apply (rule continuous_intros | simp add: hvcon)+ ``` lp15@60809 ` 1449` ``` done ``` lp15@60809 ` 1450` ``` have "(\x. f (g (fst x)) (h (snd x))) = (\(y1,y2). f y1 y2) o (\w. ((g o fst) w, (h o snd) w))" ``` lp15@60809 ` 1451` ``` by auto ``` lp15@60809 ` 1452` ``` then have fgh: "continuous_on (cbox (0, 0) (1, 1)) (\x. f (g (fst x)) (h (snd x)))" ``` lp15@60809 ` 1453` ``` apply (rule ssubst) ``` lp15@60809 ` 1454` ``` apply (rule gcon hcon continuous_intros | simp)+ ``` lp15@60809 ` 1455` ``` apply (auto simp: path_image_def intro: continuous_on_subset [OF fcon]) ``` lp15@60809 ` 1456` ``` done ``` lp15@60809 ` 1457` ``` have "integral {0..1} (\x. path_integral h (f (g x)) * vector_derivative g (at x)) = ``` lp15@60809 ` 1458` ``` integral {0..1} (\x. path_integral h (\y. f (g x) y * vector_derivative g (at x)))" ``` lp15@60809 ` 1459` ``` apply (rule integral_cong [OF path_integral_rmul [symmetric]]) ``` lp15@60809 ` 1460` ``` apply (clarsimp simp: path_integrable_on) ``` lp15@60809 ` 1461` ``` apply (rule integrable_continuous_real) ``` lp15@60809 ` 1462` ``` apply (rule continuous_on_mult [OF _ hvcon]) ``` lp15@60809 ` 1463` ``` apply (subst fgh1) ``` lp15@60809 ` 1464` ``` apply (rule fcon_im1 hcon continuous_intros | simp)+ ``` lp15@60809 ` 1465` ``` done ``` lp15@60809 ` 1466` ``` also have "... = integral {0..1} ``` lp15@60809 ` 1467` ``` (\y. path_integral g (\x. f x (h y) * vector_derivative h (at y)))" ``` lp15@60809 ` 1468` ``` apply (simp add: path_integral_integral) ``` lp15@60809 ` 1469` ``` apply (subst integral_swap_continuous [where 'a = real and 'b = real, of 0 0 1 1, simplified]) ``` lp15@60809 ` 1470` ``` apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+ ``` lp15@60809 ` 1471` ``` apply (simp add: algebra_simps) ``` lp15@60809 ` 1472` ``` done ``` lp15@60809 ` 1473` ``` also have "... = path_integral h (\z. path_integral g (\w. f w z))" ``` lp15@60809 ` 1474` ``` apply (simp add: path_integral_integral) ``` lp15@60809 ` 1475` ``` apply (rule integral_cong) ``` lp15@60809 ` 1476` ``` apply (subst integral_mult_left [symmetric]) ``` lp15@60809 ` 1477` ``` apply (blast intro: vdg) ``` lp15@60809 ` 1478` ``` apply (simp add: algebra_simps) ``` lp15@60809 ` 1479` ``` done ``` lp15@60809 ` 1480` ``` finally show ?thesis ``` lp15@60809 ` 1481` ``` by (simp add: path_integral_integral) ``` lp15@60809 ` 1482` ```qed ``` lp15@60809 ` 1483` lp15@60809 ` 1484` lp15@60809 ` 1485` ```subsection\The key quadrisection step\ ``` lp15@60809 ` 1486` lp15@60809 ` 1487` ```lemma norm_sum_half: ``` lp15@60809 ` 1488` ``` assumes "norm(a + b) >= e" ``` lp15@60809 ` 1489` ``` shows "norm a >= e/2 \ norm b >= e/2" ``` lp15@60809 ` 1490` ```proof - ``` lp15@60809 ` 1491` ``` have "e \ norm (- a - b)" ``` lp15@60809 ` 1492` ``` by (simp add: add.commute assms norm_minus_commute) ``` lp15@60809 ` 1493` ``` thus ?thesis ``` lp15@60809 ` 1494` ``` using norm_triangle_ineq4 order_trans by fastforce ``` lp15@60809 ` 1495` ```qed ``` lp15@60809 ` 1496` lp15@60809 ` 1497` ```lemma norm_sum_lemma: ``` lp15@60809 ` 1498` ``` assumes "e \ norm (a + b + c + d)" ``` lp15@60809 ` 1499` ``` shows "e / 4 \ norm a \ e / 4 \ norm b \ e / 4 \ norm c \ e / 4 \ norm d" ``` lp15@60809 ` 1500` ```proof - ``` lp15@60809 ` 1501` ``` have "e \ norm ((a + b) + (c + d))" using assms ``` lp15@60809 ` 1502` ``` by (simp add: algebra_simps) ``` lp15@60809 ` 1503` ``` then show ?thesis ``` lp15@60809 ` 1504` ``` by (auto dest!: norm_sum_half) ``` lp15@60809 ` 1505` ```qed ``` lp15@60809 ` 1506` lp15@60809 ` 1507` ```lemma Cauchy_theorem_quadrisection: ``` lp15@60809 ` 1508` ``` assumes f: "continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 1509` ``` and dist: "dist a b \ K" "dist b c \ K" "dist c a \ K" ``` lp15@60809 ` 1510` ``` and e: "e * K^2 \ ``` lp15@60809 ` 1511` ``` norm (path_integral(linepath a b) f + path_integral(linepath b c) f + path_integral(linepath c a) f)" ``` lp15@60809 ` 1512` ``` shows "\a' b' c'. ``` lp15@60809 ` 1513` ``` a' \ convex hull {a,b,c} \ b' \ convex hull {a,b,c} \ c' \ convex hull {a,b,c} \ ``` lp15@60809 ` 1514` ``` dist a' b' \ K/2 \ dist b' c' \ K/2 \ dist c' a' \ K/2 \ ``` lp15@60809 ` 1515` ``` e * (K/2)^2 \ norm(path_integral(linepath a' b') f + path_integral(linepath b' c') f + path_integral(linepath c' a') f)" ``` lp15@60809 ` 1516` ```proof - ``` lp15@60809 ` 1517` ``` note divide_le_eq_numeral1 [simp del] ``` lp15@60809 ` 1518` ``` def a' \ "midpoint b c" ``` lp15@60809 ` 1519` ``` def b' \ "midpoint c a" ``` lp15@60809 ` 1520` ``` def c' \ "midpoint a b" ``` lp15@60809 ` 1521` ``` have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" ``` lp15@60809 ` 1522` ``` using f continuous_on_subset segments_subset_convex_hull by metis+ ``` lp15@60809 ` 1523` ``` have fcont': "continuous_on (closed_segment c' b') f" ``` lp15@60809 ` 1524` ``` "continuous_on (closed_segment a' c') f" ``` lp15@60809 ` 1525` ``` "continuous_on (closed_segment b' a') f" ``` lp15@60809 ` 1526` ``` unfolding a'_def b'_def c'_def ``` lp15@60809 ` 1527` ``` apply (rule continuous_on_subset [OF f], ``` lp15@60809 ` 1528` ``` metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+ ``` lp15@60809 ` 1529` ``` done ``` lp15@60809 ` 1530` ``` let ?pathint = "\x y. path_integral(linepath x y) f" ``` lp15@60809 ` 1531` ``` have *: "?pathint a b + ?pathint b c + ?pathint c a = ``` lp15@60809 ` 1532` ``` (?pathint a c' + ?pathint c' b' + ?pathint b' a) + ``` lp15@60809 ` 1533` ``` (?pathint a' c' + ?pathint c' b + ?pathint b a') + ``` lp15@60809 ` 1534` ``` (?pathint a' c + ?pathint c b' + ?pathint b' a') + ``` lp15@60809 ` 1535` ``` (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" ``` lp15@60809 ` 1536` ``` apply (simp add: fcont' path_integral_reverse_linepath) ``` lp15@60809 ` 1537` ``` apply (simp add: a'_def b'_def c'_def path_integral_midpoint fabc) ``` lp15@60809 ` 1538` ``` done ``` lp15@60809 ` 1539` ``` have [simp]: "\x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2" ``` lp15@60809 ` 1540` ``` by (metis left_diff_distrib mult.commute norm_mult_numeral1) ``` lp15@60809 ` 1541` ``` have [simp]: "\x y. cmod (x - y) = cmod (y - x)" ``` lp15@60809 ` 1542` ``` by (simp add: norm_minus_commute) ``` lp15@60809 ` 1543` ``` consider "e * K\<^sup>2 / 4 \ cmod (?pathint a c' + ?pathint c' b' + ?pathint b' a)" | ``` lp15@60809 ` 1544` ``` "e * K\<^sup>2 / 4 \ cmod (?pathint a' c' + ?pathint c' b + ?pathint b a')" | ``` lp15@60809 ` 1545` ``` "e * K\<^sup>2 / 4 \ cmod (?pathint a' c + ?pathint c b' + ?pathint b' a')" | ``` lp15@60809 ` 1546` ``` "e * K\<^sup>2 / 4 \ cmod (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" ``` lp15@60809 ` 1547` ``` using assms ``` lp15@60809 ` 1548` ``` apply (simp only: *) ``` lp15@60809 ` 1549` ``` apply (blast intro: that dest!: norm_sum_lemma) ``` lp15@60809 ` 1550` ``` done ``` lp15@60809 ` 1551` ``` then show ?thesis ``` lp15@60809 ` 1552` ``` proof cases ``` lp15@60809 ` 1553` ``` case 1 then show ?thesis ``` lp15@60809 ` 1554` ``` apply (rule_tac x=a in exI) ``` lp15@60809 ` 1555` ``` apply (rule exI [where x=c']) ``` lp15@60809 ` 1556` ``` apply (rule exI [where x=b']) ``` lp15@60809 ` 1557` ``` using assms ``` lp15@60809 ` 1558` ``` apply (auto simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@60809 ` 1559` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 1560` ``` done ``` lp15@60809 ` 1561` ``` next ``` lp15@60809 ` 1562` ``` case 2 then show ?thesis ``` lp15@60809 ` 1563` ``` apply (rule_tac x=a' in exI) ``` lp15@60809 ` 1564` ``` apply (rule exI [where x=c']) ``` lp15@60809 ` 1565` ``` apply (rule exI [where x=b]) ``` lp15@60809 ` 1566` ``` using assms ``` lp15@60809 ` 1567` ``` apply (auto simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@60809 ` 1568` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 1569` ``` done ``` lp15@60809 ` 1570` ``` next ``` lp15@60809 ` 1571` ``` case 3 then show ?thesis ``` lp15@60809 ` 1572` ``` apply (rule_tac x=a' in exI) ``` lp15@60809 ` 1573` ``` apply (rule exI [where x=c]) ``` lp15@60809 ` 1574` ``` apply (rule exI [where x=b']) ``` lp15@60809 ` 1575` ``` using assms ``` lp15@60809 ` 1576` ``` apply (auto simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@60809 ` 1577` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 1578` ``` done ``` lp15@60809 ` 1579` ``` next ``` lp15@60809 ` 1580` ``` case 4 then show ?thesis ``` lp15@60809 ` 1581` ``` apply (rule_tac x=a' in exI) ``` lp15@60809 ` 1582` ``` apply (rule exI [where x=b']) ``` lp15@60809 ` 1583` ``` apply (rule exI [where x=c']) ``` lp15@60809 ` 1584` ``` using assms ``` lp15@60809 ` 1585` ``` apply (auto simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) ``` lp15@60809 ` 1586` ``` apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real divide_simps) ``` lp15@60809 ` 1587` ``` done ``` lp15@60809 ` 1588` ``` qed ``` lp15@60809 ` 1589` ```qed ``` lp15@60809 ` 1590` lp15@60809 ` 1591` ```subsection\Cauchy's theorem for triangles\ ``` lp15@60809 ` 1592` lp15@60809 ` 1593` ```lemma triangle_points_closer: ``` lp15@60809 ` 1594` ``` fixes a::complex ``` lp15@60809 ` 1595` ``` shows "\x \ convex hull {a,b,c}; y \ convex hull {a,b,c}\ ``` lp15@60809 ` 1596` ``` \ norm(x - y) \ norm(a - b) \ ``` lp15@60809 ` 1597` ``` norm(x - y) \ norm(b - c) \ ``` lp15@60809 ` 1598` ``` norm(x - y) \ norm(c - a)" ``` lp15@60809 ` 1599` ``` using simplex_extremal_le [of "{a,b,c}"] ``` lp15@60809 ` 1600` ``` by (auto simp: norm_minus_commute) ``` lp15@60809 ` 1601` lp15@60809 ` 1602` ```lemma holomorphic_point_small_triangle: ``` lp15@60809 ` 1603` ``` assumes x: "x \ s" ``` lp15@60809 ` 1604` ``` and f: "continuous_on s f" ``` lp15@60809 ` 1605` ``` and cd: "f complex_differentiable (at x within s)" ``` lp15@60809 ` 1606` ``` and e: "0 < e" ``` lp15@60809 ` 1607` ``` shows "\k>0. \a b c. dist a b \ k \ dist b c \ k \ dist c a \ k \ ``` lp15@60809 ` 1608` ``` x \ convex hull {a,b,c} \ convex hull {a,b,c} \ s ``` lp15@60809 ` 1609` ``` \ norm(path_integral(linepath a b) f + path_integral(linepath b c) f + ``` lp15@60809 ` 1610` ``` path_integral(linepath c a) f) ``` lp15@60809 ` 1611` ``` \ e*(dist a b + dist b c + dist c a)^2" ``` lp15@60809 ` 1612` ``` (is "\k>0. \a b c. _ \ ?normle a b c") ``` lp15@60809 ` 1613` ```proof - ``` lp15@60809 ` 1614` ``` have le_of_3: "\a x y z. \0 \ x*y; 0 \ x*z; 0 \ y*z; a \ (e*(x + y + z))*x + (e*(x + y + z))*y + (e*(x + y + z))*z\ ``` lp15@60809 ` 1615` ``` \ a \ e*(x + y + z)^2" ``` lp15@60809 ` 1616` ``` by (simp add: algebra_simps power2_eq_square) ``` lp15@60809 ` 1617` ``` have disj_le: "\x \ a \ x \ b \ x \ c; 0 \ a; 0 \ b; 0 \ c\ \ x \ a + b + c" ``` lp15@60809 ` 1618` ``` for x::real and a b c ``` lp15@60809 ` 1619` ``` by linarith ``` lp15@60809 ` 1620` ``` have fabc: "f path_integrable_on linepath a b" "f path_integrable_on linepath b c" "f path_integrable_on linepath c a" ``` lp15@60809 ` 1621` ``` if "convex hull {a, b, c} \ s" for a b c ``` lp15@60809 ` 1622` ``` using segments_subset_convex_hull that ``` lp15@60809 ` 1623` ``` by (metis continuous_on_subset f path_integrable_continuous_linepath)+ ``` lp15@60809 ` 1624` ``` note path_bound = has_path_integral_bound_linepath [simplified norm_minus_commute, OF has_path_integral_integral] ``` lp15@60809 ` 1625` ``` { fix f' a b c d ``` lp15@60809 ` 1626` ``` assume d: "0 < d" ``` lp15@60809 ` 1627` ``` and f': "\y. \cmod (y - x) \ d; y \ s\ \ cmod (f y - f x - f' * (y - x)) \ e * cmod (y - x)" ``` lp15@60809 ` 1628` ``` and le: "cmod (a - b) \ d" "cmod (b - c) \ d" "cmod (c - a) \ d" ``` lp15@60809 ` 1629` ``` and xc: "x \ convex hull {a, b, c}" ``` lp15@60809 ` 1630` ``` and s: "convex hull {a, b, c} \ s" ``` lp15@60809 ` 1631` ``` have pa: "path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c a) f = ``` lp15@60809 ` 1632` ``` path_integral (linepath a b) (\y. f y - f x - f'*(y - x)) + ``` lp15@60809 ` 1633` ``` path_integral (linepath b c) (\y. f y - f x - f'*(y - x)) + ``` lp15@60809 ` 1634` ``` path_integral (linepath c a) (\y. f y - f x - f'*(y - x))" ``` lp15@60809 ` 1635` ``` apply (simp add: path_integral_diff path_integral_lmul path_integrable_lmul path_integrable_diff fabc [OF s]) ``` lp15@60809 ` 1636` ``` apply (simp add: field_simps) ``` lp15@60809 ` 1637` ``` done ``` lp15@60809 ` 1638` ``` { fix y ``` lp15@60809 ` 1639` ``` assume yc: "y \ convex hull {a,b,c}" ``` lp15@60809 ` 1640` ``` have "cmod (f y - f x - f' * (y - x)) \ e*norm(y - x)" ``` lp15@60809 ` 1641` ``` apply (rule f') ``` lp15@60809 ` 1642` ``` apply (metis triangle_points_closer [OF xc yc] le norm_minus_commute order_trans) ``` lp15@60809 ` 1643` ``` using s yc by blast ``` lp15@60809 ` 1644` ``` also have "... \ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" ``` lp15@60809 ` 1645` ``` by (simp add: yc e xc disj_le [OF triangle_points_closer]) ``` lp15@60809 ` 1646` ``` finally have "cmod (f y - f x - f' * (y - x)) \ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" . ``` lp15@60809 ` 1647` ``` } note cm_le = this ``` lp15@60809 ` 1648` ``` have "?normle a b c" ``` lp15@60809 ` 1649` ``` apply (simp add: dist_norm pa) ``` lp15@60809 ` 1650` ``` apply (rule le_of_3) ``` lp15@60809 ` 1651` ``` using f' xc s e ``` lp15@60809 ` 1652` ``` apply simp_all ``` lp15@60809 ` 1653` ``` apply (intro norm_triangle_le add_mono path_bound) ``` lp15@60809 ` 1654` ``` apply (simp_all add: path_integral_diff path_integral_lmul path_integrable_lmul path_integrable_diff fabc) ``` lp15@60809 ` 1655` ``` apply (blast intro: cm_le elim: dest: segments_subset_convex_hull [THEN subsetD])+ ``` lp15@60809 ` 1656` ``` done ``` lp15@60809 ` 1657` ``` } note * = this ``` lp15@60809 ` 1658` ``` show ?thesis ``` lp15@60809 ` 1659` ``` using cd e ``` lp15@60809 ` 1660` ``` apply (simp add: complex_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def) ``` lp15@60809 ` 1661` ``` apply (clarify dest!: spec mp) ``` lp15@60809 ` 1662` ``` using * ``` lp15@60809 ` 1663` ``` apply (simp add: dist_norm, blast) ``` lp15@60809 ` 1664` ``` done ``` lp15@60809 ` 1665` ```qed ``` lp15@60809 ` 1666` lp15@60809 ` 1667` lp15@60809 ` 1668` ```(* Hence the most basic theorem for a triangle.*) ``` lp15@60809 ` 1669` ```locale Chain = ``` lp15@60809 ` 1670` ``` fixes x0 At Follows ``` lp15@60809 ` 1671` ``` assumes At0: "At x0 0" ``` lp15@60809 ` 1672` ``` and AtSuc: "\x n. At x n \ \x'. At x' (Suc n) \ Follows x' x" ``` lp15@60809 ` 1673` ```begin ``` lp15@60809 ` 1674` ``` primrec f where ``` lp15@60809 ` 1675` ``` "f 0 = x0" ``` lp15@60809 ` 1676` ``` | "f (Suc n) = (SOME x. At x (Suc n) \ Follows x (f n))" ``` lp15@60809 ` 1677` lp15@60809 ` 1678` ``` lemma At: "At (f n) n" ``` lp15@60809 ` 1679` ``` proof (induct n) ``` lp15@60809 ` 1680` ``` case 0 show ?case ``` lp15@60809 ` 1681` ``` by (simp add: At0) ``` lp15@60809 ` 1682` ``` next ``` lp15@60809 ` 1683` ``` case (Suc n) show ?case ``` lp15@60809 ` 1684` ``` by (metis (no_types, lifting) AtSuc [OF Suc] f.simps(2) someI_ex) ``` lp15@60809 ` 1685` ``` qed ``` lp15@60809 ` 1686` lp15@60809 ` 1687` ``` lemma Follows: "Follows (f(Suc n)) (f n)" ``` lp15@60809 ` 1688` ``` by (metis (no_types, lifting) AtSuc [OF At [of n]] f.simps(2) someI_ex) ``` lp15@60809 ` 1689` lp15@60809 ` 1690` ``` declare f.simps(2) [simp del] ``` lp15@60809 ` 1691` ```end ``` lp15@60809 ` 1692` lp15@60809 ` 1693` ```lemma Chain3: ``` lp15@60809 ` 1694` ``` assumes At0: "At x0 y0 z0 0" ``` lp15@60809 ` 1695` ``` and AtSuc: "\x y z n. At x y z n \ \x' y' z'. At x' y' z' (Suc n) \ Follows x' y' z' x y z" ``` lp15@60809 ` 1696` ``` obtains f g h where ``` lp15@60809 ` 1697` ``` "f 0 = x0" "g 0 = y0" "h 0 = z0" ``` lp15@60809 ` 1698` ``` "\n. At (f n) (g n) (h n) n" ``` lp15@60809 ` 1699` ``` "\n. Follows (f(Suc n)) (g(Suc n)) (h(Suc n)) (f n) (g n) (h n)" ``` lp15@60809 ` 1700` ```proof - ``` lp15@60809 ` 1701` ``` interpret three: Chain "(x0,y0,z0)" "\(x,y,z). At x y z" "\(x',y',z'). \(x,y,z). Follows x' y' z' x y z" ``` lp15@60809 ` 1702` ``` apply unfold_locales ``` lp15@60809 ` 1703` ``` using At0 AtSuc by auto ``` lp15@60809 ` 1704` ``` show ?thesis ``` lp15@60809 ` 1705` ``` apply (rule that [of "\n. fst (three.f n)" "\n. fst (snd (three.f n))" "\n. snd (snd (three.f n))"]) ``` lp15@60809 ` 1706` ``` apply simp_all ``` lp15@60809 ` 1707` ``` using three.At three.Follows ``` lp15@60809 ` 1708` ``` apply (simp_all add: split_beta') ``` lp15@60809 ` 1709` ``` done ``` lp15@60809 ` 1710` ```qed ``` lp15@60809 ` 1711` lp15@60809 ` 1712` ```lemma Cauchy_theorem_triangle: ``` lp15@60809 ` 1713` ``` assumes "f holomorphic_on (convex hull {a,b,c})" ``` lp15@60809 ` 1714` ``` shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 1715` ```proof - ``` lp15@60809 ` 1716` ``` have contf: "continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 1717` ``` by (metis assms holomorphic_on_imp_continuous_on) ``` lp15@60809 ` 1718` ``` let ?pathint = "\x y. path_integral(linepath x y) f" ``` lp15@60809 ` 1719` ``` { fix y::complex ``` lp15@60809 ` 1720` ``` assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 1721` ``` and ynz: "y \ 0" ``` lp15@60809 ` 1722` ``` def K \ "1 + max (dist a b) (max (dist b c) (dist c a))" ``` lp15@60809 ` 1723` ``` def e \ "norm y / K^2" ``` lp15@60809 ` 1724` ``` have K1: "K \ 1" by (simp add: K_def max.coboundedI1) ``` lp15@60809 ` 1725` ``` then have K: "K > 0" by linarith ``` lp15@60809 ` 1726` ``` have [iff]: "dist a b \ K" "dist b c \ K" "dist c a \ K" ``` lp15@60809 ` 1727` ``` by (simp_all add: K_def) ``` lp15@60809 ` 1728` ``` have e: "e > 0" ``` lp15@60809 ` 1729` ``` unfolding e_def using ynz K1 by simp ``` lp15@60809 ` 1730` ``` def At \ "\x y z n. convex hull {x,y,z} \ convex hull {a,b,c} \ ``` lp15@60809 ` 1731` ``` dist x y \ K/2^n \ dist y z \ K/2^n \ dist z x \ K/2^n \ ``` lp15@60809 ` 1732` ``` norm(?pathint x y + ?pathint y z + ?pathint z x) \ e*(K/2^n)^2" ``` lp15@60809 ` 1733` ``` have At0: "At a b c 0" ``` lp15@60809 ` 1734` ``` using fy ``` lp15@60809 ` 1735` ``` by (simp add: At_def e_def has_chain_integral_chain_integral3) ``` lp15@60809 ` 1736` ``` { fix x y z n ``` lp15@60809 ` 1737` ``` assume At: "At x y z n" ``` lp15@60809 ` 1738` ``` then have contf': "continuous_on (convex hull {x,y,z}) f" ``` lp15@60809 ` 1739` ``` using contf At_def continuous_on_subset by blast ``` lp15@60809 ` 1740` ``` have "\x' y' z'. At x' y' z' (Suc n) \ convex hull {x',y',z'} \ convex hull {x,y,z}" ``` lp15@60809 ` 1741` ``` using At ``` lp15@60809 ` 1742` ``` apply (simp add: At_def) ``` lp15@60809 ` 1743` ``` using Cauchy_theorem_quadrisection [OF contf', of "K/2^n" e] ``` lp15@60809 ` 1744` ``` apply clarsimp ``` lp15@60809 ` 1745` ``` apply (rule_tac x="a'" in exI) ``` lp15@60809 ` 1746` ``` apply (rule_tac x="b'" in exI) ``` lp15@60809 ` 1747` ``` apply (rule_tac x="c'" in exI) ``` lp15@60809 ` 1748` ``` apply (simp add: algebra_simps) ``` lp15@60809 ` 1749` ``` apply (meson convex_hull_subset empty_subsetI insert_subset subsetCE) ``` lp15@60809 ` 1750` ``` done ``` lp15@60809 ` 1751` ``` } note AtSuc = this ``` lp15@60809 ` 1752` ``` obtain fa fb fc ``` lp15@60809 ` 1753` ``` where f0 [simp]: "fa 0 = a" "fb 0 = b" "fc 0 = c" ``` lp15@60809 ` 1754` ``` and cosb: "\n. convex hull {fa n, fb n, fc n} \ convex hull {a,b,c}" ``` lp15@60809 ` 1755` ``` and dist: "\n. dist (fa n) (fb n) \ K/2^n" ``` lp15@60809 ` 1756` ``` "\n. dist (fb n) (fc n) \ K/2^n" ``` lp15@60809 ` 1757` ``` "\n. dist (fc n) (fa n) \ K/2^n" ``` lp15@60809 ` 1758` ``` and no: "\n. norm(?pathint (fa n) (fb n) + ``` lp15@60809 ` 1759` ``` ?pathint (fb n) (fc n) + ``` lp15@60809 ` 1760` ``` ?pathint (fc n) (fa n)) \ e * (K/2^n)^2" ``` lp15@60809 ` 1761` ``` and conv_le: "\n. convex hull {fa(Suc n), fb(Suc n), fc(Suc n)} \ convex hull {fa n, fb n, fc n}" ``` lp15@60809 ` 1762` ``` apply (rule Chain3 [of At, OF At0 AtSuc]) ``` lp15@60809 ` 1763` ``` apply (auto simp: At_def) ``` lp15@60809 ` 1764` ``` done ``` lp15@60809 ` 1765` ``` have "\x. \n. x \ convex hull {fa n, fb n, fc n}" ``` lp15@60809 ` 1766` ``` apply (rule bounded_closed_nest) ``` lp15@60809 ` 1767` ``` apply (simp_all add: compact_imp_closed finite_imp_compact_convex_hull finite_imp_bounded_convex_hull) ``` lp15@60809 ` 1768` ``` apply (rule allI) ``` lp15@60809 ` 1769` ``` apply (rule transitive_stepwise_le) ``` lp15@60809 ` 1770` ``` apply (auto simp: conv_le) ``` lp15@60809 ` 1771` ``` done ``` lp15@60809 ` 1772` ``` then obtain x where x: "\n. x \ convex hull {fa n, fb n, fc n}" by auto ``` lp15@60809 ` 1773` ``` then have xin: "x \ convex hull {a,b,c}" ``` lp15@60809 ` 1774` ``` using assms f0 by blast ``` lp15@60809 ` 1775` ``` then have fx: "f complex_differentiable at x within (convex hull {a,b,c})" ``` lp15@60809 ` 1776` ``` using assms holomorphic_on_def by blast ``` lp15@60809 ` 1777` ``` { fix k n ``` lp15@60809 ` 1778` ``` assume k: "0 < k" ``` lp15@60809 ` 1779` ``` and le: ``` lp15@60809 ` 1780` ``` "\x' y' z'. ``` lp15@60809 ` 1781` ``` \dist x' y' \ k; dist y' z' \ k; dist z' x' \ k; ``` lp15@60809 ` 1782` ``` x \ convex hull {x',y',z'}; ``` lp15@60809 ` 1783` ``` convex hull {x',y',z'} \ convex hull {a,b,c}\ ``` lp15@60809 ` 1784` ``` \ ``` lp15@60809 ` 1785` ``` cmod (?pathint x' y' + ?pathint y' z' + ?pathint z' x') * 10 ``` lp15@60809 ` 1786` ``` \ e * (dist x' y' + dist y' z' + dist z' x')\<^sup>2" ``` lp15@60809 ` 1787` ``` and Kk: "K / k < 2 ^ n" ``` lp15@60809 ` 1788` ``` have "K / 2 ^ n < k" using Kk k ``` lp15@60809 ` 1789` ``` by (auto simp: field_simps) ``` lp15@60809 ` 1790` ``` then have DD: "dist (fa n) (fb n) \ k" "dist (fb n) (fc n) \ k" "dist (fc n) (fa n) \ k" ``` lp15@60809 ` 1791` ``` using dist [of n] k ``` lp15@60809 ` 1792` ``` by linarith+ ``` lp15@60809 ` 1793` ``` have dle: "(dist (fa n) (fb n) + dist (fb n) (fc n) + dist (fc n) (fa n))\<^sup>2 ``` lp15@60809 ` 1794` ``` \ (3 * K / 2 ^ n)\<^sup>2" ``` lp15@60809 ` 1795` ``` using dist [of n] e K ``` lp15@60809 ` 1796` ``` by (simp add: abs_le_square_iff [symmetric]) ``` lp15@60809 ` 1797` ``` have less10: "\x y::real. 0 < x \ y \ 9*x \ y < x*10" ``` lp15@60809 ` 1798` ``` by linarith ``` lp15@60809 ` 1799` ``` have "e * (dist (fa n) (fb n) + dist (fb n) (fc n) + dist (fc n) (fa n))\<^sup>2 \ e * (3 * K / 2 ^ n)\<^sup>2" ``` lp15@60809 ` 1800` ``` using ynz dle e mult_le_cancel_left_pos by blast ``` lp15@60809 ` 1801` ``` also have "... < ``` lp15@60809 ` 1802` ``` cmod (?pathint (fa n) (fb n) + ?pathint (fb n) (fc n) + ?pathint (fc n) (fa n)) * 10" ``` lp15@60809 ` 1803` ``` using no [of n] e K ``` lp15@60809 ` 1804` ``` apply (simp add: e_def field_simps) ``` lp15@60809 ` 1805` ``` apply (simp only: zero_less_norm_iff [symmetric]) ``` lp15@60809 ` 1806` ``` done ``` lp15@60809 ` 1807` ``` finally have False ``` lp15@60809 ` 1808` ``` using le [OF DD x cosb] by auto ``` lp15@60809 ` 1809` ``` } then ``` lp15@60809 ` 1810` ``` have ?thesis ``` lp15@60809 ` 1811` ``` using holomorphic_point_small_triangle [OF xin contf fx, of "e/10"] e ``` lp15@60809 ` 1812` ``` apply clarsimp ``` lp15@60809 ` 1813` ``` apply (rule_tac x1="K/k" in exE [OF real_arch_pow2], blast) ``` lp15@60809 ` 1814` ``` done ``` lp15@60809 ` 1815` ``` } ``` lp15@60809 ` 1816` ``` moreover have "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 1817` ``` by simp (meson contf continuous_on_subset path_integrable_continuous_linepath segments_subset_convex_hull(1) ``` lp15@60809 ` 1818` ``` segments_subset_convex_hull(3) segments_subset_convex_hull(5)) ``` lp15@60809 ` 1819` ``` ultimately show ?thesis ``` lp15@60809 ` 1820` ``` using has_path_integral_integral by fastforce ``` lp15@60809 ` 1821` ```qed ``` lp15@60809 ` 1822` lp15@60809 ` 1823` lp15@60809 ` 1824` ```subsection\Version needing function holomorphic in interior only\ ``` lp15@60809 ` 1825` lp15@60809 ` 1826` ```lemma Cauchy_theorem_flat_lemma: ``` lp15@60809 ` 1827` ``` assumes f: "continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 1828` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@60809 ` 1829` ``` and k: "0 \ k" ``` lp15@60809 ` 1830` ``` shows "path_integral (linepath a b) f + path_integral (linepath b c) f + ``` lp15@60809 ` 1831` ``` path_integral (linepath c a) f = 0" ``` lp15@60809 ` 1832` ```proof - ``` lp15@60809 ` 1833` ``` have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" ``` lp15@60809 ` 1834` ``` using f continuous_on_subset segments_subset_convex_hull by metis+ ``` lp15@60809 ` 1835` ``` show ?thesis ``` lp15@60809 ` 1836` ``` proof (cases "k \ 1") ``` lp15@60809 ` 1837` ``` case True show ?thesis ``` lp15@60809 ` 1838` ``` by (simp add: path_integral_split [OF fabc(1) k True c] path_integral_reverse_linepath fabc) ``` lp15@60809 ` 1839` ``` next ``` lp15@60809 ` 1840` ``` case False then show ?thesis ``` lp15@60809 ` 1841` ``` using fabc c ``` lp15@60809 ` 1842` ``` apply (subst path_integral_split [of a c f "1/k" b, symmetric]) ``` lp15@60809 ` 1843` ``` apply (metis closed_segment_commute fabc(3)) ``` lp15@60809 ` 1844` ``` apply (auto simp: k path_integral_reverse_linepath) ``` lp15@60809 ` 1845` ``` done ``` lp15@60809 ` 1846` ``` qed ``` lp15@60809 ` 1847` ```qed ``` lp15@60809 ` 1848` lp15@60809 ` 1849` ```lemma Cauchy_theorem_flat: ``` lp15@60809 ` 1850` ``` assumes f: "continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 1851` ``` and c: "c - a = k *\<^sub>R (b - a)" ``` lp15@60809 ` 1852` ``` shows "path_integral (linepath a b) f + ``` lp15@60809 ` 1853` ``` path_integral (linepath b c) f + ``` lp15@60809 ` 1854` ``` path_integral (linepath c a) f = 0" ``` lp15@60809 ` 1855` ```proof (cases "0 \ k") ``` lp15@60809 ` 1856` ``` case True with assms show ?thesis ``` lp15@60809 ` 1857` ``` by (blast intro: Cauchy_theorem_flat_lemma) ``` lp15@60809 ` 1858` ```next ``` lp15@60809 ` 1859` ``` case False ``` lp15@60809 ` 1860` ``` have "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" ``` lp15@60809 ` 1861` ``` using f continuous_on_subset segments_subset_convex_hull by metis+ ``` lp15@60809 ` 1862` ``` moreover have "path_integral (linepath b a) f + path_integral (linepath a c) f + ``` lp15@60809 ` 1863` ``` path_integral (linepath c b) f = 0" ``` lp15@60809 ` 1864` ``` apply (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"]) ``` lp15@60809 ` 1865` ``` using False c ``` lp15@60809 ` 1866` ``` apply (auto simp: f insert_commute scaleR_conv_of_real algebra_simps) ``` lp15@60809 ` 1867` ``` done ``` lp15@60809 ` 1868` ``` ultimately show ?thesis ``` lp15@60809 ` 1869` ``` apply (auto simp: path_integral_reverse_linepath) ``` lp15@60809 ` 1870` ``` using add_eq_0_iff by force ``` lp15@60809 ` 1871` ```qed ``` lp15@60809 ` 1872` lp15@60809 ` 1873` lp15@60809 ` 1874` ```lemma Cauchy_theorem_triangle_interior: ``` lp15@60809 ` 1875` ``` assumes contf: "continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 1876` ``` and holf: "f holomorphic_on interior (convex hull {a,b,c})" ``` lp15@60809 ` 1877` ``` shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 1878` ```proof - ``` lp15@60809 ` 1879` ``` have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" ``` lp15@60809 ` 1880` ``` using contf continuous_on_subset segments_subset_convex_hull by metis+ ``` lp15@60809 ` 1881` ``` have "bounded (f ` (convex hull {a,b,c}))" ``` lp15@60809 ` 1882` ``` by (simp add: compact_continuous_image compact_convex_hull compact_imp_bounded contf) ``` lp15@60809 ` 1883` ``` then obtain B where "0 < B" and Bnf: "\x. x \ convex hull {a,b,c} \ norm (f x) \ B" ``` lp15@60809 ` 1884` ``` by (auto simp: dest!: bounded_pos [THEN iffD1]) ``` lp15@60809 ` 1885` ``` have "bounded (convex hull {a,b,c})" ``` lp15@60809 ` 1886` ``` by (simp add: bounded_convex_hull) ``` lp15@60809 ` 1887` ``` then obtain C where C: "0 < C" and Cno: "\y. y \ convex hull {a,b,c} \ norm y < C" ``` lp15@60809 ` 1888` ``` using bounded_pos_less by blast ``` lp15@60809 ` 1889` ``` then have diff_2C: "norm(x - y) \ 2*C" ``` lp15@60809 ` 1890` ``` if x: "x \ convex hull {a, b, c}" and y: "y \ convex hull {a, b, c}" for x y ``` lp15@60809 ` 1891` ``` proof - ``` lp15@60809 ` 1892` ``` have "cmod x \ C" ``` lp15@60809 ` 1893` ``` using x by (meson Cno not_le not_less_iff_gr_or_eq) ``` lp15@60809 ` 1894` ``` hence "cmod (x - y) \ C + C" ``` lp15@60809 ` 1895` ``` using y by (meson Cno add_mono_thms_linordered_field(4) less_eq_real_def norm_triangle_ineq4 order_trans) ``` lp15@60809 ` 1896` ``` thus "cmod (x - y) \ 2 * C" ``` lp15@60809 ` 1897` ``` by (metis mult_2) ``` lp15@60809 ` 1898` ``` qed ``` lp15@60809 ` 1899` ``` have contf': "continuous_on (convex hull {b,a,c}) f" ``` lp15@60809 ` 1900` ``` using contf by (simp add: insert_commute) ``` lp15@60809 ` 1901` ``` { fix y::complex ``` lp15@60809 ` 1902` ``` assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 1903` ``` and ynz: "y \ 0" ``` lp15@60809 ` 1904` ``` have pi_eq_y: "path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c a) f = y" ``` lp15@60809 ` 1905` ``` by (rule has_chain_integral_chain_integral3 [OF fy]) ``` lp15@60809 ` 1906` ``` have ?thesis ``` lp15@60809 ` 1907` ``` proof (cases "c=a \ a=b \ b=c") ``` lp15@60809 ` 1908` ``` case True then show ?thesis ``` lp15@60809 ` 1909` ``` using Cauchy_theorem_flat [OF contf, of 0] ``` lp15@60809 ` 1910` ``` using has_chain_integral_chain_integral3 [OF fy] ynz ``` lp15@60809 ` 1911` ``` by (force simp: fabc path_integral_reverse_linepath) ``` lp15@60809 ` 1912` ``` next ``` lp15@60809 ` 1913` ``` case False ``` lp15@60809 ` 1914` ``` then have car3: "card {a, b, c} = Suc (DIM(complex))" ``` lp15@60809 ` 1915` ``` by auto ``` lp15@60809 ` 1916` ``` { assume "interior(convex hull {a,b,c}) = {}" ``` lp15@60809 ` 1917` ``` then have "collinear{a,b,c}" ``` lp15@60809 ` 1918` ``` using interior_convex_hull_eq_empty [OF car3] ``` lp15@60809 ` 1919` ``` by (simp add: collinear_3_eq_affine_dependent) ``` lp15@60809 ` 1920` ``` then have "False" ``` lp15@60809 ` 1921` ``` using False ``` lp15@60809 ` 1922` ``` apply (clarsimp simp add: collinear_3 collinear_lemma) ``` lp15@60809 ` 1923` ``` apply (drule Cauchy_theorem_flat [OF contf']) ``` lp15@60809 ` 1924` ``` using pi_eq_y ynz ``` lp15@60809 ` 1925` ``` apply (simp add: fabc add_eq_0_iff path_integral_reverse_linepath) ``` lp15@60809 ` 1926` ``` done ``` lp15@60809 ` 1927` ``` } ``` lp15@60809 ` 1928` ``` then obtain d where d: "d \ interior (convex hull {a, b, c})" ``` lp15@60809 ` 1929` ``` by blast ``` lp15@60809 ` 1930` ``` { fix d1 ``` lp15@60809 ` 1931` ``` assume d1_pos: "0 < d1" ``` lp15@60809 ` 1932` ``` and d1: "\x x'. \x\convex hull {a, b, c}; x'\convex hull {a, b, c}; cmod (x' - x) < d1\ ``` lp15@60809 ` 1933` ``` \ cmod (f x' - f x) < cmod y / (24 * C)" ``` lp15@60809 ` 1934` ``` def e \ "min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))" ``` lp15@60809 ` 1935` ``` def shrink \ "\x. x - e *\<^sub>R (x - d)" ``` lp15@60809 ` 1936` ``` let ?pathint = "\x y. path_integral(linepath x y) f" ``` lp15@60809 ` 1937` ``` have e: "0 < e" "e \ 1" "e \ d1 / (4 * C)" "e \ cmod y / 24 / C / B" ``` lp15@60809 ` 1938` ``` using d1_pos `C>0` `B>0` ynz by (simp_all add: e_def) ``` lp15@60809 ` 1939` ``` then have eCB: "24 * e * C * B \ cmod y" ``` lp15@60809 ` 1940` ``` using `C>0` `B>0` by (simp add: field_simps) ``` lp15@60809 ` 1941` ``` have e_le_d1: "e * (4 * C) \ d1" ``` lp15@60809 ` 1942` ``` using e `C>0` by (simp add: field_simps) ``` lp15@60809 ` 1943` ``` have "shrink a \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 1944` ``` "shrink b \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 1945` ``` "shrink c \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 1946` ``` using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) ``` lp15@60809 ` 1947` ``` then have fhp0: "(f has_path_integral 0) ``` lp15@60809 ` 1948` ``` (linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))" ``` lp15@60809 ` 1949` ``` by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal convex_interior) ``` lp15@60809 ` 1950` ``` then have f_0_shrink: "?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a) = 0" ``` lp15@60809 ` 1951` ``` by (simp add: has_chain_integral_chain_integral3) ``` lp15@60809 ` 1952` ``` have fpi_abc: "f path_integrable_on linepath (shrink a) (shrink b)" ``` lp15@60809 ` 1953` ``` "f path_integrable_on linepath (shrink b) (shrink c)" ``` lp15@60809 ` 1954` ``` "f path_integrable_on linepath (shrink c) (shrink a)" ``` lp15@60809 ` 1955` ``` using fhp0 by (auto simp: valid_path_join dest: has_path_integral_integrable) ``` lp15@60809 ` 1956` ``` have cmod_shr: "\x y. cmod (shrink y - shrink x - (y - x)) = e * cmod (x - y)" ``` lp15@60809 ` 1957` ``` using e by (simp add: shrink_def real_vector.scale_right_diff_distrib [symmetric]) ``` lp15@60809 ` 1958` ``` have sh_eq: "\a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)" ``` lp15@60809 ` 1959` ``` by (simp add: algebra_simps) ``` lp15@60809 ` 1960` ``` have "cmod y / (24 * C) \ cmod y / cmod (b - a) / 12" ``` lp15@60809 ` 1961` ``` using False `C>0` diff_2C [of b a] ynz ``` lp15@60809 ` 1962` ``` by (auto simp: divide_simps hull_inc) ``` lp15@60809 ` 1963` ``` have less_C: "\u \ convex hull {a, b, c}; 0 \ x; x \ 1\ \ x * cmod u < C" for x u ``` lp15@60809 ` 1964` ``` apply (cases "x=0", simp add: `0 convex hull {a, b, c}" "v \ convex hull {a, b, c}" "u\v" ``` lp15@60809 ` 1968` ``` and fpi_uv: "f path_integrable_on linepath (shrink u) (shrink v)" ``` lp15@60809 ` 1969` ``` have shr_uv: "shrink u \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 1970` ``` "shrink v \ interior(convex hull {a,b,c})" ``` lp15@60809 ` 1971` ``` using d e uv ``` lp15@60809 ` 1972` ``` by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) ``` lp15@60809 ` 1973` ``` have cmod_fuv: "\x. 0\x \ x\1 \ cmod (f (linepath (shrink u) (shrink v) x)) \ B" ``` lp15@60809 ` 1974` ``` using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD]) ``` lp15@60809 ` 1975` ``` have By_uv: "B * (12 * (e * cmod (u - v))) \ cmod y" ``` lp15@60809 ` 1976` ``` apply (rule order_trans [OF _ eCB]) ``` lp15@60809 ` 1977` ``` using e `B>0` diff_2C [of u v] uv ``` lp15@60809 ` 1978` ``` by (auto simp: field_simps) ``` lp15@60809 ` 1979` ``` { fix x::real assume x: "0\x" "x\1" ``` lp15@60809 ` 1980` ``` have cmod_less_4C: "cmod ((1 - x) *\<^sub>R u - (1 - x) *\<^sub>R d) + cmod (x *\<^sub>R v - x *\<^sub>R d) < (C+C) + (C+C)" ``` lp15@60809 ` 1981` ``` apply (rule add_strict_mono; rule norm_triangle_half_l [of _ 0]) ``` lp15@60809 ` 1982` ``` using uv x d interior_subset ``` lp15@60809 ` 1983` ``` apply (auto simp: hull_inc intro!: less_C) ``` lp15@60809 ` 1984` ``` done ``` lp15@60809 ` 1985` ``` have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))" ``` lp15@60809 ` 1986` ``` by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real) ``` lp15@60809 ` 1987` ``` have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1" ``` lp15@60809 ` 1988` ``` using `e>0` ``` lp15@60809 ` 1989` ``` apply (simp add: ll norm_mult scaleR_diff_right) ``` lp15@60809 ` 1990` ``` apply (rule less_le_trans [OF _ e_le_d1]) ``` lp15@60809 ` 1991` ``` using cmod_less_4C ``` lp15@60809 ` 1992` ``` apply (force intro: norm_triangle_lt) ``` lp15@60809 ` 1993` ``` done ``` lp15@60809 ` 1994` ``` have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)" ``` lp15@60809 ` 1995` ``` using x uv shr_uv cmod_less_dt ``` lp15@60809 ` 1996` ``` by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull) ``` lp15@60809 ` 1997` ``` also have "... \ cmod y / cmod (v - u) / 12" ``` lp15@60809 ` 1998` ``` using False uv `C>0` diff_2C [of v u] ynz ``` lp15@60809 ` 1999` ``` by (auto simp: divide_simps hull_inc) ``` lp15@60809 ` 2000` ``` finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \ cmod y / cmod (v - u) / 12" ``` lp15@60809 ` 2001` ``` by simp ``` lp15@60809 ` 2002` ``` then have cmod_12_le: "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) * 12 \ cmod y" ``` lp15@60809 ` 2003` ``` using uv False by (auto simp: field_simps) ``` lp15@60809 ` 2004` ``` have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) + ``` lp15@60809 ` 2005` ``` cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) ``` lp15@60809 ` 2006` ``` \ cmod y / 6" ``` lp15@60809 ` 2007` ``` apply (rule order_trans [of _ "B*((norm y / 24 / C / B)*2*C) + (2*C)*(norm y /24 / C)"]) ``` lp15@60809 ` 2008` ``` apply (rule add_mono [OF mult_mono]) ``` lp15@60809 ` 2009` ``` using By_uv e `0 < B` `0 < C` x ynz ``` lp15@60809 ` 2010` ``` apply (simp_all add: cmod_fuv cmod_shr cmod_12_le hull_inc) ``` lp15@60809 ` 2011` ``` apply (simp add: field_simps) ``` lp15@60809 ` 2012` ``` done ``` lp15@60809 ` 2013` ``` } note cmod_diff_le = this ``` lp15@60809 ` 2014` ``` have f_uv: "continuous_on (closed_segment u v) f" ``` lp15@60809 ` 2015` ``` by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull]) ``` lp15@60809 ` 2016` ``` have **: "\f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)" ``` lp15@60809 ` 2017` ``` by (simp add: algebra_simps) ``` lp15@60809 ` 2018` ``` have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) \ norm y / 6" ``` lp15@60809 ` 2019` ``` apply (rule order_trans) ``` lp15@60809 ` 2020` ``` apply (rule has_integral_bound ``` lp15@60809 ` 2021` ``` [of "B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)" ``` lp15@60809 ` 2022` ``` "\x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)" ``` lp15@60809 ` 2023` ``` _ 0 1 ]) ``` lp15@60809 ` 2024` ``` using ynz `0 < B` `0 < C` ``` lp15@60809 ` 2025` ``` apply (simp_all del: le_divide_eq_numeral1) ``` lp15@60809 ` 2026` ``` apply (simp add: has_integral_sub has_path_integral_linepath [symmetric] has_path_integral_integral ``` lp15@60809 ` 2027` ``` fpi_uv f_uv path_integrable_continuous_linepath, clarify) ``` lp15@60809 ` 2028` ``` apply (simp only: **) ``` lp15@60809 ` 2029` ``` apply (simp add: norm_triangle_le norm_mult cmod_diff_le del: le_divide_eq_numeral1) ``` lp15@60809 ` 2030` ``` done ``` lp15@60809 ` 2031` ``` } note * = this ``` lp15@60809 ` 2032` ``` have "norm (?pathint (shrink a) (shrink b) - ?pathint a b) \ norm y / 6" ``` lp15@60809 ` 2033` ``` using False fpi_abc by (rule_tac *) (auto simp: hull_inc) ``` lp15@60809 ` 2034` ``` moreover ``` lp15@60809 ` 2035` ``` have "norm (?pathint (shrink b) (shrink c) - ?pathint b c) \ norm y / 6" ``` lp15@60809 ` 2036` ``` using False fpi_abc by (rule_tac *) (auto simp: hull_inc) ``` lp15@60809 ` 2037` ``` moreover ``` lp15@60809 ` 2038` ``` have "norm (?pathint (shrink c) (shrink a) - ?pathint c a) \ norm y / 6" ``` lp15@60809 ` 2039` ``` using False fpi_abc by (rule_tac *) (auto simp: hull_inc) ``` lp15@60809 ` 2040` ``` ultimately ``` lp15@60809 ` 2041` ``` have "norm((?pathint (shrink a) (shrink b) - ?pathint a b) + ``` lp15@60809 ` 2042` ``` (?pathint (shrink b) (shrink c) - ?pathint b c) + (?pathint (shrink c) (shrink a) - ?pathint c a)) ``` lp15@60809 ` 2043` ``` \ norm y / 6 + norm y / 6 + norm y / 6" ``` lp15@60809 ` 2044` ``` by (metis norm_triangle_le add_mono) ``` lp15@60809 ` 2045` ``` also have "... = norm y / 2" ``` lp15@60809 ` 2046` ``` by simp ``` lp15@60809 ` 2047` ``` finally have "norm((?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a)) - ``` lp15@60809 ` 2048` ``` (?pathint a b + ?pathint b c + ?pathint c a)) ``` lp15@60809 ` 2049` ``` \ norm y / 2" ``` lp15@60809 ` 2050` ``` by (simp add: algebra_simps) ``` lp15@60809 ` 2051` ``` then ``` lp15@60809 ` 2052` ``` have "norm(?pathint a b + ?pathint b c + ?pathint c a) \ norm y / 2" ``` lp15@60809 ` 2053` ``` by (simp add: f_0_shrink) (metis (mono_tags) add.commute minus_add_distrib norm_minus_cancel uminus_add_conv_diff) ``` lp15@60809 ` 2054` ``` then have "False" ``` lp15@60809 ` 2055` ``` using pi_eq_y ynz by auto ``` lp15@60809 ` 2056` ``` } ``` lp15@60809 ` 2057` ``` moreover have "uniformly_continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 2058` ``` by (simp add: contf compact_convex_hull compact_uniformly_continuous) ``` lp15@60809 ` 2059` ``` ultimately have "False" ``` lp15@60809 ` 2060` ``` unfolding uniformly_continuous_on_def ``` lp15@60809 ` 2061` ``` by (force simp: ynz `0 < C` dist_norm) ``` lp15@60809 ` 2062` ``` then show ?thesis .. ``` lp15@60809 ` 2063` ``` qed ``` lp15@60809 ` 2064` ``` } ``` lp15@60809 ` 2065` ``` moreover have "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 2066` ``` using fabc path_integrable_continuous_linepath by auto ``` lp15@60809 ` 2067` ``` ultimately show ?thesis ``` lp15@60809 ` 2068` ``` using has_path_integral_integral by fastforce ``` lp15@60809 ` 2069` ```qed ``` lp15@60809 ` 2070` lp15@60809 ` 2071` lp15@60809 ` 2072` lp15@60809 ` 2073` ```subsection\Version allowing finite number of exceptional points\ ``` lp15@60809 ` 2074` lp15@60809 ` 2075` ```lemma Cauchy_theorem_triangle_cofinite: ``` lp15@60809 ` 2076` ``` assumes "continuous_on (convex hull {a,b,c}) f" ``` lp15@60809 ` 2077` ``` and "finite s" ``` lp15@60809 ` 2078` ``` and "(\x. x \ interior(convex hull {a,b,c}) - s \ f complex_differentiable (at x))" ``` lp15@60809 ` 2079` ``` shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 2080` ```using assms ``` lp15@60809 ` 2081` ```proof (induction "card s" arbitrary: a b c s rule: less_induct) ``` lp15@60809 ` 2082` ``` case (less s a b c) ``` lp15@60809 ` 2083` ``` show ?case ``` lp15@60809 ` 2084` ``` proof (cases "s={}") ``` lp15@60809 ` 2085` ``` case True with less show ?thesis ``` lp15@60809 ` 2086` ``` by (simp add: holomorphic_on_def complex_differentiable_at_within ``` lp15@60809 ` 2087` ``` Cauchy_theorem_triangle_interior) ``` lp15@60809 ` 2088` ``` next ``` lp15@60809 ` 2089` ``` case False ``` lp15@60809 ` 2090` ``` then obtain d s' where d: "s = insert d s'" "d \ s'" ``` lp15@60809 ` 2091` ``` by (meson Set.set_insert all_not_in_conv) ``` lp15@60809 ` 2092` ``` then show ?thesis ``` lp15@60809 ` 2093` ``` proof (cases "d \ convex hull {a,b,c}") ``` lp15@60809 ` 2094` ``` case False ``` lp15@60809 ` 2095` ``` show "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 2096` ``` apply (rule less.hyps [of "s'"]) ``` lp15@60809 ` 2097` ``` using False d `finite s` interior_subset ``` lp15@60809 ` 2098` ``` apply (auto intro!: less.prems) ``` lp15@60809 ` 2099` ``` done ``` lp15@60809 ` 2100` ``` next ``` lp15@60809 ` 2101` ``` case True ``` lp15@60809 ` 2102` ``` have *: "convex hull {a, b, d} \ convex hull {a, b, c}" ``` lp15@60809 ` 2103` ``` by (meson True hull_subset insert_subset convex_hull_subset) ``` lp15@60809 ` 2104` ``` have abd: "(f has_path_integral 0) (linepath a b +++ linepath b d +++ linepath d a)" ``` lp15@60809 ` 2105` ``` apply (rule less.hyps [of "s'"]) ``` lp15@60809 ` 2106` ``` using True d `finite s` not_in_interior_convex_hull_3 ``` lp15@60809 ` 2107` ``` apply (auto intro!: less.prems continuous_on_subset [OF _ *]) ``` lp15@60809 ` 2108` ``` apply (metis * insert_absorb insert_subset interior_mono) ``` lp15@60809 ` 2109` ``` done ``` lp15@60809 ` 2110` ``` have *: "convex hull {b, c, d} \ convex hull {a, b, c}" ``` lp15@60809 ` 2111` ``` by (meson True hull_subset insert_subset convex_hull_subset) ``` lp15@60809 ` 2112` ``` have bcd: "(f has_path_integral 0) (linepath b c +++ linepath c d +++ linepath d b)" ``` lp15@60809 ` 2113` ``` apply (rule less.hyps [of "s'"]) ``` lp15@60809 ` 2114` ``` using True d `finite s` not_in_interior_convex_hull_3 ``` lp15@60809 ` 2115` ``` apply (auto intro!: less.prems continuous_on_subset [OF _ *]) ``` lp15@60809 ` 2116` ``` apply (metis * insert_absorb insert_subset interior_mono) ``` lp15@60809 ` 2117` ``` done ``` lp15@60809 ` 2118` ``` have *: "convex hull {c, a, d} \ convex hull {a, b, c}" ``` lp15@60809 ` 2119` ``` by (meson True hull_subset insert_subset convex_hull_subset) ``` lp15@60809 ` 2120` ``` have cad: "(f has_path_integral 0) (linepath c a +++ linepath a d +++ linepath d c)" ``` lp15@60809 ` 2121` ``` apply (rule less.hyps [of "s'"]) ``` lp15@60809 ` 2122` ``` using True d `finite s` not_in_interior_convex_hull_3 ``` lp15@60809 ` 2123` ``` apply (auto intro!: less.prems continuous_on_subset [OF _ *]) ``` lp15@60809 ` 2124` ``` apply (metis * insert_absorb insert_subset interior_mono) ``` lp15@60809 ` 2125` ``` done ``` lp15@60809 ` 2126` ``` have "f path_integrable_on linepath a b" ``` lp15@60809 ` 2127` ``` using less.prems ``` lp15@60809 ` 2128` ``` by (metis continuous_on_subset insert_commute path_integrable_continuous_linepath segments_subset_convex_hull(3)) ``` lp15@60809 ` 2129` ``` moreover have "f path_integrable_on linepath b c" ``` lp15@60809 ` 2130` ``` using less.prems ``` lp15@60809 ` 2131` ``` by (metis continuous_on_subset path_integrable_continuous_linepath segments_subset_convex_hull(3)) ``` lp15@60809 ` 2132` ``` moreover have "f path_integrable_on linepath c a" ``` lp15@60809 ` 2133` ``` using less.prems ``` lp15@60809 ` 2134` ``` by (metis continuous_on_subset insert_commute path_integrable_continuous_linepath segments_subset_convex_hull(3)) ``` lp15@60809 ` 2135` ``` ultimately have fpi: "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 2136` ``` by auto ``` lp15@60809 ` 2137` ``` { fix y::complex ``` lp15@60809 ` 2138` ``` assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 2139` ``` and ynz: "y \ 0" ``` lp15@60809 ` 2140` ``` have cont_ad: "continuous_on (closed_segment a d) f" ``` lp15@60809 ` 2141` ``` by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(3)) ``` lp15@60809 ` 2142` ``` have cont_bd: "continuous_on (closed_segment b d) f" ``` lp15@60809 ` 2143` ``` by (meson True closed_segment_subset_convex_hull continuous_on_subset hull_subset insert_subset less.prems(1)) ``` lp15@60809 ` 2144` ``` have cont_cd: "continuous_on (closed_segment c d) f" ``` lp15@60809 ` 2145` ``` by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(2)) ``` lp15@60809 ` 2146` ``` have "path_integral (linepath a b) f = - (path_integral (linepath b d) f + (path_integral (linepath d a) f))" ``` lp15@60809 ` 2147` ``` "path_integral (linepath b c) f = - (path_integral (linepath c d) f + (path_integral (linepath d b) f))" ``` lp15@60809 ` 2148` ``` "path_integral (linepath c a) f = - (path_integral (linepath a d) f + path_integral (linepath d c) f)" ``` lp15@60809 ` 2149` ``` using has_chain_integral_chain_integral3 [OF abd] ``` lp15@60809 ` 2150` ``` has_chain_integral_chain_integral3 [OF bcd] ``` lp15@60809 ` 2151` ``` has_chain_integral_chain_integral3 [OF cad] ``` lp15@60809 ` 2152` ``` by (simp_all add: algebra_simps add_eq_0_iff) ``` lp15@60809 ` 2153` ``` then have ?thesis ``` lp15@60809 ` 2154` ``` using cont_ad cont_bd cont_cd fy has_chain_integral_chain_integral3 path_integral_reverse_linepath by fastforce ``` lp15@60809 ` 2155` ``` } ``` lp15@60809 ` 2156` ``` then show ?thesis ``` lp15@60809 ` 2157` ``` using fpi path_integrable_on_def by blast ``` lp15@60809 ` 2158` ``` qed ``` lp15@60809 ` 2159` ``` qed ``` lp15@60809 ` 2160` ```qed ``` lp15@60809 ` 2161` lp15@60809 ` 2162` lp15@60809 ` 2163` ```subsection\Cauchy's theorem for an open starlike set\ ``` lp15@60809 ` 2164` lp15@60809 ` 2165` ```lemma starlike_convex_subset: ``` lp15@60809 ` 2166` ``` assumes s: "a \ s" "closed_segment b c \ s" and subs: "\x. x \ s \ closed_segment a x \ s" ``` lp15@60809 ` 2167` ``` shows "convex hull {a,b,c} \ s" ``` lp15@60809 ` 2168` ``` using s ``` lp15@60809 ` 2169` ``` apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull) ``` lp15@60809 ` 2170` ``` apply (meson subs convexD convex_segment ends_in_segment(1) ends_in_segment(2) subsetCE) ``` lp15@60809 ` 2171` ``` done ``` lp15@60809 ` 2172` lp15@60809 ` 2173` ```lemma triangle_path_integrals_starlike_primitive: ``` lp15@60809 ` 2174` ``` assumes contf: "continuous_on s f" ``` lp15@60809 ` 2175` ``` and s: "a \ s" "open s" ``` lp15@60809 ` 2176` ``` and x: "x \ s" ``` lp15@60809 ` 2177` ``` and subs: "\y. y \ s \ closed_segment a y \ s" ``` lp15@60809 ` 2178` ``` and zer: "\b c. closed_segment b c \ s ``` lp15@60809 ` 2179` ``` \ path_integral (linepath a b) f + path_integral (linepath b c) f + ``` lp15@60809 ` 2180` ``` path_integral (linepath c a) f = 0" ``` lp15@60809 ` 2181` ``` shows "((\x. path_integral(linepath a x) f) has_field_derivative f x) (at x)" ``` lp15@60809 ` 2182` ```proof - ``` lp15@60809 ` 2183` ``` let ?pathint = "\x y. path_integral(linepath x y) f" ``` lp15@60809 ` 2184` ``` { fix e y ``` lp15@60809 ` 2185` ``` assume e: "0 < e" and bxe: "ball x e \ s" and close: "cmod (y - x) < e" ``` lp15@60809 ` 2186` ``` have y: "y \ s" ``` lp15@60809 ` 2187` ``` using bxe close by (force simp: dist_norm norm_minus_commute) ``` lp15@60809 ` 2188` ``` have cont_ayf: "continuous_on (closed_segment a y) f" ``` lp15@60809 ` 2189` ``` using contf continuous_on_subset subs y by blast ``` lp15@60809 ` 2190` ``` have xys: "closed_segment x y \ s" ``` lp15@60809 ` 2191` ``` apply (rule order_trans [OF _ bxe]) ``` lp15@60809 ` 2192` ``` using close ``` lp15@60809 ` 2193` ``` by (auto simp: dist_norm ball_def norm_minus_commute dest: segment_bound) ``` lp15@60809 ` 2194` ``` have "?pathint a y - ?pathint a x = ?pathint x y" ``` lp15@60809 ` 2195` ``` using zer [OF xys] path_integral_reverse_linepath [OF cont_ayf] add_eq_0_iff by force ``` lp15@60809 ` 2196` ``` } note [simp] = this ``` lp15@60809 ` 2197` ``` { fix e::real ``` lp15@60809 ` 2198` ``` assume e: "0 < e" ``` lp15@60809 ` 2199` ``` have cont_atx: "continuous (at x) f" ``` lp15@60809 ` 2200` ``` using x s contf continuous_on_eq_continuous_at by blast ``` lp15@60809 ` 2201` ``` then obtain d1 where d1: "d1>0" and d1_less: "\y. cmod (y - x) < d1 \ cmod (f y - f x) < e/2" ``` lp15@60809 ` 2202` ``` unfolding continuous_at Lim_at dist_norm using e ``` lp15@60809 ` 2203` ``` by (drule_tac x="e/2" in spec) force ``` lp15@60809 ` 2204` ``` obtain d2 where d2: "d2>0" "ball x d2 \ s" using `open s` x ``` lp15@60809 ` 2205` ``` by (auto simp: open_contains_ball) ``` lp15@60809 ` 2206` ``` have dpos: "min d1 d2 > 0" using d1 d2 by simp ``` lp15@60809 ` 2207` ``` { fix y ``` lp15@60809 ` 2208` ``` assume yx: "y \ x" and close: "cmod (y - x) < min d1 d2" ``` lp15@60809 ` 2209` ``` have y: "y \ s" ``` lp15@60809 ` 2210` ``` using d2 close by (force simp: dist_norm norm_minus_commute) ``` lp15@60809 ` 2211` ``` have fxy: "f path_integrable_on linepath x y" ``` lp15@60809 ` 2212` ``` apply (rule path_integrable_continuous_linepath) ``` lp15@60809 ` 2213` ``` apply (rule continuous_on_subset [OF contf]) ``` lp15@60809 ` 2214` ``` using close d2 ``` lp15@60809 ` 2215` ``` apply (auto simp: dist_norm norm_minus_commute dest!: segment_bound(1)) ``` lp15@60809 ` 2216` ``` done ``` lp15@60809 ` 2217` ``` then obtain i where i: "(f has_path_integral i) (linepath x y)" ``` lp15@60809 ` 2218` ``` by (auto simp: path_integrable_on_def) ``` lp15@60809 ` 2219` ``` then have "((\w. f w - f x) has_path_integral (i - f x * (y - x))) (linepath x y)" ``` lp15@60809 ` 2220` ``` by (rule has_path_integral_diff [OF _ has_path_integral_const_linepath]) ``` lp15@60809 ` 2221` ``` then have "cmod (i - f x * (y - x)) \ e / 2 * cmod (y - x)" ``` lp15@60809 ` 2222` ``` apply (rule has_path_integral_bound_linepath [where B = "e/2"]) ``` lp15@60809 ` 2223` ``` using e apply simp ``` lp15@60809 ` 2224` ``` apply (rule d1_less [THEN less_imp_le]) ``` lp15@60809 ` 2225` ``` using close segment_bound ``` lp15@60809 ` 2226` ``` apply force ``` lp15@60809 ` 2227` ``` done ``` lp15@60809 ` 2228` ``` also have "... < e * cmod (y - x)" ``` lp15@60809 ` 2229` ``` by (simp add: e yx) ``` lp15@60809 ` 2230` ``` finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" ``` lp15@60809 ` 2231` ``` using i yx by (simp add: path_integral_unique divide_less_eq) ``` lp15@60809 ` 2232` ``` } ``` lp15@60809 ` 2233` ``` then have "\d>0. \y. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" ``` lp15@60809 ` 2234` ``` using dpos by blast ``` lp15@60809 ` 2235` ``` } ``` lp15@60809 ` 2236` ``` then have *: "(\y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) -- x --> 0" ``` lp15@60809 ` 2237` ``` by (simp add: Lim_at dist_norm inverse_eq_divide) ``` lp15@60809 ` 2238` ``` show ?thesis ``` lp15@60809 ` 2239` ``` apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right) ``` lp15@60809 ` 2240` ``` apply (rule Lim_transform [OF * Lim_eventually]) ``` lp15@60809 ` 2241` ``` apply (simp add: inverse_eq_divide [symmetric] eventually_at) ``` lp15@60809 ` 2242` ``` using `open s` x ``` lp15@60809 ` 2243` ``` apply (force simp: dist_norm open_contains_ball) ``` lp15@60809 ` 2244` ``` done ``` lp15@60809 ` 2245` ```qed ``` lp15@60809 ` 2246` lp15@60809 ` 2247` ```(** Existence of a primitive.*) ``` lp15@60809 ` 2248` lp15@60809 ` 2249` ```lemma holomorphic_starlike_primitive: ``` lp15@60809 ` 2250` ``` assumes contf: "continuous_on s f" ``` lp15@60809 ` 2251` ``` and s: "starlike s" and os: "open s" ``` lp15@60809 ` 2252` ``` and k: "finite k" ``` lp15@60809 ` 2253` ``` and fcd: "\x. x \ s - k \ f complex_differentiable at x" ``` lp15@60809 ` 2254` ``` shows "\g. \x \ s. (g has_field_derivative f x) (at x)" ``` lp15@60809 ` 2255` ```proof - ``` lp15@60809 ` 2256` ``` obtain a where a: "a\s" and a_cs: "\x. x\s \ closed_segment a x \ s" ``` lp15@60809 ` 2257` ``` using s by (auto simp: starlike_def) ``` lp15@60809 ` 2258` ``` { fix x b c ``` lp15@60809 ` 2259` ``` assume "x \ s" "closed_segment b c \ s" ``` lp15@60809 ` 2260` ``` then have abcs: "convex hull {a, b, c} \ s" ``` lp15@60809 ` 2261` ``` by (simp add: a a_cs starlike_convex_subset) ``` lp15@60809 ` 2262` ``` then have *: "continuous_on (convex hull {a, b, c}) f" ``` lp15@60809 ` 2263` ``` by (simp add: continuous_on_subset [OF contf]) ``` lp15@60809 ` 2264` ``` have "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" ``` lp15@60809 ` 2265` ``` apply (rule Cauchy_theorem_triangle_cofinite [OF _ k]) ``` lp15@60809 ` 2266` ``` using abcs apply (simp add: continuous_on_subset [OF contf]) ``` lp15@60809 ` 2267` ``` using * abcs interior_subset apply (auto intro: fcd) ``` lp15@60809 ` 2268` ``` done ``` lp15@60809 ` 2269` ``` } note 0 = this ``` lp15@60809 ` 2270` ``` show ?thesis ``` lp15@60809 ` 2271` ``` apply (intro exI ballI) ``` lp15@60809 ` 2272` ``` apply (rule triangle_path_integrals_starlike_primitive [OF contf a os], assumption) ``` lp15@60809 ` 2273` ``` apply (metis a_cs) ``` lp15@60809 ` 2274` ``` apply (metis has_chain_integral_chain_integral3 0) ``` lp15@60809 ` 2275` ``` done ``` lp15@60809 ` 2276` ```qed ``` lp15@60809 ` 2277` lp15@60809 ` 2278` ```lemma Cauchy_theorem_starlike: ``` lp15@60809 ` 2279` ``` "\open s; starlike s; finite k; continuous_on s f; ``` lp15@60809 ` 2280` ``` \x. x \ s - k \ f complex_differentiable at x; ``` lp15@60809 ` 2281` ``` valid_path g; path_image g \ s; pathfinish g = pathstart g\ ``` lp15@60809 ` 2282` ``` \ (f has_path_integral 0) g" ``` lp15@60809 ` 2283` ``` by (metis holomorphic_starlike_primitive Cauchy_theorem_primitive at_within_open) ``` lp15@60809 ` 2284` lp15@60809 ` 2285` ```lemma Cauchy_theorem_starlike_simple: ``` lp15@60809 ` 2286` ``` "\open s; starlike s; f holomorphic_on s; valid_path g; path_image g \ s; pathfinish g = pathstart g\ ``` lp15@60809 ` 2287` ``` \ (f has_path_integral 0) g" ``` lp15@60809 ` 2288` ```apply (rule Cauchy_theorem_starlike [OF _ _ finite.emptyI]) ``` lp15@60809 ` 2289` ```apply (simp_all add: holomorphic_on_imp_continuous_on) ``` lp15@60809 ` 2290` ```apply (metis at_within_open holomorphic_on_def) ``` lp15@60809 ` 2291` ```done ``` lp15@60809 ` 2292` lp15@60809 ` 2293` lp15@60809 ` 2294` ```subsection\Cauchy's theorem for a convex set\ ``` lp15@60809 ` 2295` lp15@60809 ` 2296` ```text\For a convex set we can avoid assuming openness and boundary analyticity\ ``` lp15@60809 ` 2297` lp15@60809 ` 2298` ```lemma triangle_path_integrals_convex_primitive: ``` lp15@60809 ` 2299` ``` assumes contf: "continuous_on s f" ``` lp15@60809 ` 2300` ``` and s: "a \ s" "convex s" ``` lp15@60809 ` 2301` ``` and x: "x \ s" ``` lp15@60809 ` 2302` ``` and zer: "\b c. \b \ s; c \ s\ ``` lp15@60809 ` 2303` ``` \ path_integral (linepath a b) f + path_integral (linepath b c) f + ``` lp15@60809 ` 2304` ``` path_integral (linepath c a) f = 0" ``` lp15@60809 ` 2305` ``` shows "((\x. path_integral(linepath a x) f) has_field_derivative f x) (at x within s)" ``` lp15@60809 ` 2306` ```proof - ``` lp15@60809 ` 2307` ``` let ?pathint = "\x y. path_integral(linepath x y) f" ``` lp15@60809 ` 2308` ``` { fix y ``` lp15@60809 ` 2309` ``` assume y: "y \ s" ``` lp15@60809 ` 2310` ` have cont_ayf: "continuous_on (closed_segment a`