# HG changeset patch # User paulson # Date 1527369115 -3600 # Node ID 69d680e9496174d11862edf3645b514a7978a01d # Parent b9160ca067ae3a4e2254c0cad8257867da6b374d tidying and reorganisation around Cauchy Integral Theorem diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sat May 26 10:11:11 2018 +0100 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Sat May 26 22:11:55 2018 +0100 @@ -2036,7 +2036,8 @@ by (simp add: continuous_on_id retraction) lemma retract_of_refl [iff]: "S retract_of S" - using continuous_on_id retract_of_def retraction_def by fastforce + unfolding retract_of_def retraction_def + using continuous_on_id by blast lemma retract_of_imp_subset: "S retract_of T \ S \ T" @@ -2047,8 +2048,7 @@ by (auto simp: retract_of_def retraction_def) lemma retract_of_singleton [iff]: "({x} retract_of S) \ x \ S" - using continuous_on_const - by (auto simp: retract_of_def retraction_def) + unfolding retract_of_def retraction_def by force lemma retraction_comp: "\retraction S T f; retraction T U g\ diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat May 26 10:11:11 2018 +0100 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat May 26 22:11:55 2018 +0100 @@ -255,7 +255,7 @@ by (simp add: \finite S\) show "g1 differentiable at x within {0..1}" if "x \ {0..1} - insert 1 (( * ) 2 ` S)" for x proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within) - have "g1 +++ g2 differentiable at (x / 2) within {0..1 / 2}" + have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}" by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+ then show "g1 +++ g2 \ ( * ) (inverse 2) differentiable at x within {0..1}" by (auto intro: differentiable_chain_within) @@ -288,7 +288,7 @@ by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+ then show "g1 +++ g2 \ (\x. (x+1) / 2) differentiable at x within {0..1}" by (auto intro: differentiable_chain_within) - show "(g1 +++ g2 \ (\x. (x + 1) / 2)) x' = g2 x'" if "x' \ {0..1}" "dist x' x < dist ((x + 1) / 2) (1 / 2)" for x' + show "(g1 +++ g2 \ (\x. (x + 1) / 2)) x' = g2 x'" if "x' \ {0..1}" "dist x' x < dist ((x + 1) / 2) (1/2)" for x' proof - have [simp]: "(2*x'+2)/2 = x'+1" by (simp add: divide_simps) @@ -323,65 +323,78 @@ definition C1_differentiable_on :: "(real \ 'a::real_normed_vector) \ real set \ bool" (infix "C1'_differentiable'_on" 50) where - "f C1_differentiable_on s \ - (\D. (\x \ s. (f has_vector_derivative (D x)) (at x)) \ continuous_on s D)" + "f C1_differentiable_on S \ + (\D. (\x \ S. (f has_vector_derivative (D x)) (at x)) \ continuous_on S D)" lemma C1_differentiable_on_eq: - "f C1_differentiable_on s \ - (\x \ s. f differentiable at x) \ continuous_on s (\x. vector_derivative f (at x))" - unfolding C1_differentiable_on_def - apply safe - using differentiable_def has_vector_derivative_def apply blast - apply (erule continuous_on_eq) - using vector_derivative_at apply fastforce - using vector_derivative_works apply fastforce - done + "f C1_differentiable_on S \ + (\x \ S. f differentiable at x) \ continuous_on S (\x. vector_derivative f (at x))" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + unfolding C1_differentiable_on_def + by (metis (no_types, lifting) continuous_on_eq differentiableI_vector vector_derivative_at) +next + assume ?rhs + then show ?lhs + using C1_differentiable_on_def vector_derivative_works by fastforce +qed lemma C1_differentiable_on_subset: - "f C1_differentiable_on t \ s \ t \ f C1_differentiable_on s" + "f C1_differentiable_on T \ S \ T \ f C1_differentiable_on S" unfolding C1_differentiable_on_def continuous_on_eq_continuous_within by (blast intro: continuous_within_subset) lemma C1_differentiable_compose: - "\f C1_differentiable_on s; g C1_differentiable_on (f ` s); - \x. finite (s \ f-`{x})\ - \ (g o f) C1_differentiable_on s" - apply (simp add: C1_differentiable_on_eq, safe) - using differentiable_chain_at apply blast - apply (rule continuous_on_eq [of _ "\x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"]) - apply (rule Limits.continuous_on_scaleR, assumption) - apply (metis (mono_tags, lifting) continuous_on_eq continuous_at_imp_continuous_on continuous_on_compose differentiable_imp_continuous_within o_def) - by (simp add: vector_derivative_chain_at) - -lemma C1_diff_imp_diff: "f C1_differentiable_on s \ f differentiable_on s" + assumes fg: "f C1_differentiable_on S" "g C1_differentiable_on (f ` S)" and fin: "\x. finite (S \ f-`{x})" + shows "(g o f) C1_differentiable_on S" +proof - + have "\x. x \ S \ g \ f differentiable at x" + by (meson C1_differentiable_on_eq assms differentiable_chain_at imageI) + moreover have "continuous_on S (\x. vector_derivative (g \ f) (at x))" + proof (rule continuous_on_eq [of _ "\x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"]) + show "continuous_on S (\x. vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)))" + using fg + apply (clarsimp simp add: C1_differentiable_on_eq) + apply (rule Limits.continuous_on_scaleR, assumption) + by (metis (mono_tags, lifting) continuous_at_imp_continuous_on continuous_on_compose continuous_on_cong differentiable_imp_continuous_within o_def) + show "\x. x \ S \ vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x)) = vector_derivative (g \ f) (at x)" + by (metis (mono_tags, hide_lams) C1_differentiable_on_eq fg imageI vector_derivative_chain_at) + qed + ultimately show ?thesis + by (simp add: C1_differentiable_on_eq) +qed + +lemma C1_diff_imp_diff: "f C1_differentiable_on S \ f differentiable_on S" by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on) -lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\x. x) C1_differentiable_on s" +lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\x. x) C1_differentiable_on S" by (auto simp: C1_differentiable_on_eq continuous_on_const) -lemma C1_differentiable_on_const [simp, derivative_intros]: "(\z. a) C1_differentiable_on s" +lemma C1_differentiable_on_const [simp, derivative_intros]: "(\z. a) C1_differentiable_on S" by (auto simp: C1_differentiable_on_eq continuous_on_const) lemma C1_differentiable_on_add [simp, derivative_intros]: - "f C1_differentiable_on s \ g C1_differentiable_on s \ (\x. f x + g x) C1_differentiable_on s" + "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x + g x) C1_differentiable_on S" unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) lemma C1_differentiable_on_minus [simp, derivative_intros]: - "f C1_differentiable_on s \ (\x. - f x) C1_differentiable_on s" + "f C1_differentiable_on S \ (\x. - f x) C1_differentiable_on S" unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) lemma C1_differentiable_on_diff [simp, derivative_intros]: - "f C1_differentiable_on s \ g C1_differentiable_on s \ (\x. f x - g x) C1_differentiable_on s" + "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x - g x) C1_differentiable_on S" unfolding C1_differentiable_on_eq by (auto intro: continuous_intros) lemma C1_differentiable_on_mult [simp, derivative_intros]: fixes f g :: "real \ 'a :: real_normed_algebra" - shows "f C1_differentiable_on s \ g C1_differentiable_on s \ (\x. f x * g x) C1_differentiable_on s" + shows "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x * g x) C1_differentiable_on S" unfolding C1_differentiable_on_eq by (auto simp: continuous_on_add continuous_on_mult continuous_at_imp_continuous_on differentiable_imp_continuous_within) lemma C1_differentiable_on_scaleR [simp, derivative_intros]: - "f C1_differentiable_on s \ g C1_differentiable_on s \ (\x. f x *\<^sub>R g x) C1_differentiable_on s" + "f C1_differentiable_on S \ g C1_differentiable_on S \ (\x. f x *\<^sub>R g x) C1_differentiable_on S" unfolding C1_differentiable_on_eq by (rule continuous_intros | simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+ @@ -390,10 +403,10 @@ (infixr "piecewise'_C1'_differentiable'_on" 50) where "f piecewise_C1_differentiable_on i \ continuous_on i f \ - (\s. finite s \ (f C1_differentiable_on (i - s)))" + (\S. finite S \ (f C1_differentiable_on (i - S)))" lemma C1_differentiable_imp_piecewise: - "f C1_differentiable_on s \ f piecewise_C1_differentiable_on s" + "f C1_differentiable_on S \ f piecewise_C1_differentiable_on S" by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_at_imp_continuous_on differentiable_imp_continuous_within) lemma piecewise_C1_imp_differentiable: @@ -403,25 +416,38 @@ intro: has_derivative_at_withinI) lemma piecewise_C1_differentiable_compose: - "\f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s); - \x. finite (s \ f-`{x})\ - \ (g o f) piecewise_C1_differentiable_on s" - apply (simp add: piecewise_C1_differentiable_on_def, safe) - apply (blast intro: continuous_on_compose2) - apply (rename_tac A B) - apply (rule_tac x="A \ (\x\B. s \ f-`{x})" in exI) - apply (rule conjI, blast) - apply (rule C1_differentiable_compose) - apply (blast intro: C1_differentiable_on_subset) - apply (blast intro: C1_differentiable_on_subset) - by (simp add: Diff_Int_distrib2) + assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "\x. finite (S \ f-`{x})" + shows "(g o f) piecewise_C1_differentiable_on S" +proof - + have "continuous_on S (\x. g (f x))" + by (metis continuous_on_compose2 fg order_refl piecewise_C1_differentiable_on_def) + moreover have "\T. finite T \ g \ f C1_differentiable_on S - T" + proof - + obtain F where "finite F" and F: "f C1_differentiable_on S - F" and f: "f piecewise_C1_differentiable_on S" + using fg by (auto simp: piecewise_C1_differentiable_on_def) + obtain G where "finite G" and G: "g C1_differentiable_on f ` S - G" and g: "g piecewise_C1_differentiable_on f ` S" + using fg by (auto simp: piecewise_C1_differentiable_on_def) + show ?thesis + proof (intro exI conjI) + show "finite (F \ (\x\G. S \ f-`{x}))" + using fin by (auto simp only: Int_Union \finite F\ \finite G\ finite_UN finite_imageI) + show "g \ f C1_differentiable_on S - (F \ (\x\G. S \ f -` {x}))" + apply (rule C1_differentiable_compose) + apply (blast intro: C1_differentiable_on_subset [OF F]) + apply (blast intro: C1_differentiable_on_subset [OF G]) + by (simp add: C1_differentiable_on_subset G Diff_Int_distrib2 fin) + qed + qed + ultimately show ?thesis + by (simp add: piecewise_C1_differentiable_on_def) +qed lemma piecewise_C1_differentiable_on_subset: - "f piecewise_C1_differentiable_on s \ t \ s \ f piecewise_C1_differentiable_on t" + "f piecewise_C1_differentiable_on S \ T \ S \ f piecewise_C1_differentiable_on T" by (auto simp: piecewise_C1_differentiable_on_def elim!: continuous_on_subset C1_differentiable_on_subset) lemma C1_differentiable_imp_continuous_on: - "f C1_differentiable_on s \ continuous_on s f" + "f C1_differentiable_on S \ continuous_on S f" unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within using differentiable_at_withinI differentiable_imp_continuous_within by blast @@ -431,19 +457,19 @@ lemma piecewise_C1_differentiable_affine: fixes m::real - assumes "f piecewise_C1_differentiable_on ((\x. m * x + c) ` s)" - shows "(f o (\x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on s" + assumes "f piecewise_C1_differentiable_on ((\x. m * x + c) ` S)" + shows "(f o (\x. m *\<^sub>R x + c)) piecewise_C1_differentiable_on S" proof (cases "m = 0") case True then show ?thesis unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const) next case False + have *: "\x. finite (S \ {y. m * y + c = x})" + using False not_finite_existsD by fastforce show ?thesis apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise]) - apply (rule assms derivative_intros | simp add: False vimage_def)+ - using real_vector_affinity_eq [OF False, where c=c, unfolded scaleR_conv_of_real] - apply simp + apply (rule * assms derivative_intros | simp add: False vimage_def)+ done qed @@ -454,13 +480,13 @@ "a \ c" "c \ b" "f c = g c" shows "(\x. if x \ c then f x else g x) piecewise_C1_differentiable_on {a..b}" proof - - obtain s t where st: "f C1_differentiable_on ({a..c} - s)" - "g C1_differentiable_on ({c..b} - t)" - "finite s" "finite t" + obtain S T where st: "f C1_differentiable_on ({a..c} - S)" + "g C1_differentiable_on ({c..b} - T)" + "finite S" "finite T" using assms by (force simp: piecewise_C1_differentiable_on_def) - then have f_diff: "f differentiable_on {a..x. x\c"] assms by (force simp: ivl_disj_un_two_touch) { fix x - assume x: "x \ {a..b} - insert c (s \ t)" + assume x: "x \ {a..b} - insert c (S \ T)" have "(\x. if x \ c then f x else g x) differentiable at x" (is "?diff_fg") proof (cases x c rule: le_cases) case le show ?diff_fg @@ -482,48 +508,61 @@ using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq) qed } - then have "(\x \ {a..b} - insert c (s \ t). (\x. if x \ c then f x else g x) differentiable at x)" + then have "(\x \ {a..b} - insert c (S \ T). (\x. if x \ c then f x else g x) differentiable at x)" by auto moreover - { assume fcon: "continuous_on ({a<..x. vector_derivative f (at x))" - and gcon: "continuous_on ({c<..x. vector_derivative g (at x))" - have "open ({a<..x. vector_derivative f (at x))" + and gcon: "continuous_on ({c<..x. vector_derivative g (at x))" + have "open ({a<..x. vector_derivative (\x. if x \ c then f x else g x) (at x))" - apply (rule continuous_on_eq [OF fcon]) - apply (simp add:) - apply (rule vector_derivative_at [symmetric]) - apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within) - apply (simp_all add: dist_norm vector_derivative_works [symmetric]) - apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff linorder_not_le order_less_irrefl st(1)) - apply auto - done - moreover have "continuous_on ({c<..x. vector_derivative (\x. if x \ c then f x else g x) (at x))" - apply (rule continuous_on_eq [OF gcon]) - apply (simp add:) - apply (rule vector_derivative_at [symmetric]) - apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within) - apply (simp_all add: dist_norm vector_derivative_works [symmetric]) - apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff less_irrefl not_le st(2)) - apply auto - done - ultimately have "continuous_on ({a<.. t)) + moreover have "continuous_on ({a<..x. vector_derivative (\x. if x \ c then f x else g x) (at x))" + proof - + have "((\x. if x \ c then f x else g x) has_vector_derivative vector_derivative f (at x)) (at x)" + if "a < x" "x < c" "x \ S" for x + proof - + have f: "f differentiable at x" + by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_eq_real_def st(1) that) + show ?thesis + using that + apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within) + apply (auto simp add: dist_norm vector_derivative_works [symmetric] f) + done + qed + then show ?thesis + by (metis (no_types, lifting) continuous_on_eq [OF fcon] DiffE greaterThanLessThan_iff vector_derivative_at) + qed + moreover have "continuous_on ({c<..x. vector_derivative (\x. if x \ c then f x else g x) (at x))" + proof - + have "((\x. if x \ c then f x else g x) has_vector_derivative vector_derivative g (at x)) (at x)" + if "c < x" "x < b" "x \ T" for x + proof - + have g: "g differentiable at x" + by (metis C1_differentiable_on_eq DiffD1 DiffI atLeastAtMost_diff_ends greaterThanLessThan_iff st(2) that) + show ?thesis + using that + apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within) + apply (auto simp add: dist_norm vector_derivative_works [symmetric] g) + done + qed + then show ?thesis + by (metis (no_types, lifting) continuous_on_eq [OF gcon] DiffE greaterThanLessThan_iff vector_derivative_at) + qed + ultimately have "continuous_on ({a<.. T)) (\x. vector_derivative (\x. if x \ c then f x else g x) (at x))" - apply (rule continuous_on_subset [OF continuous_on_open_Un], auto) - done + by (rule continuous_on_subset [OF continuous_on_open_Un], auto) } note * = this - have "continuous_on ({a<.. t)) (\x. vector_derivative (\x. if x \ c then f x else g x) (at x))" + have "continuous_on ({a<.. T)) (\x. vector_derivative (\x. if x \ c then f x else g x) (at x))" using st by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset intro: *) - ultimately have "\s. finite s \ ((\x. if x \ c then f x else g x) C1_differentiable_on {a..b} - s)" - apply (rule_tac x="{a,b,c} \ s \ t" in exI) + ultimately have "\S. finite S \ ((\x. if x \ c then f x else g x) C1_differentiable_on {a..b} - S)" + apply (rule_tac x="{a,b,c} \ S \ T" in exI) using st by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset) with cab show ?thesis by (simp add: piecewise_C1_differentiable_on_def) qed lemma piecewise_C1_differentiable_neg: - "f piecewise_C1_differentiable_on s \ (\x. -(f x)) piecewise_C1_differentiable_on s" + "f piecewise_C1_differentiable_on S \ (\x. -(f x)) piecewise_C1_differentiable_on S" unfolding piecewise_C1_differentiable_on_def by (auto intro!: continuous_on_minus C1_differentiable_on_minus) @@ -532,11 +571,11 @@ "g piecewise_C1_differentiable_on i" shows "(\x. f x + g x) piecewise_C1_differentiable_on i" proof - - obtain s t where st: "finite s" "finite t" - "f C1_differentiable_on (i-s)" + obtain S t where st: "finite S" "finite t" + "f C1_differentiable_on (i-S)" "g C1_differentiable_on (i-t)" using assms by (auto simp: piecewise_C1_differentiable_on_def) - then have "finite (s \ t) \ (\x. f x + g x) C1_differentiable_on i - (s \ t)" + then have "finite (S \ t) \ (\x. f x + g x) C1_differentiable_on i - (S \ t)" by (auto intro: C1_differentiable_on_add elim!: C1_differentiable_on_subset) moreover have "continuous_on i f" "continuous_on i g" using assms piecewise_C1_differentiable_on_def by auto @@ -545,8 +584,8 @@ qed lemma piecewise_C1_differentiable_diff: - "\f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on s\ - \ (\x. f x - g x) piecewise_C1_differentiable_on s" + "\f piecewise_C1_differentiable_on S; g piecewise_C1_differentiable_on S\ + \ (\x. f x - g x) piecewise_C1_differentiable_on S" unfolding diff_conv_add_uminus by (metis piecewise_C1_differentiable_add piecewise_C1_differentiable_neg) @@ -555,44 +594,53 @@ assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" shows "g1 piecewise_C1_differentiable_on {0..1}" proof - - obtain s where "finite s" - and co12: "continuous_on ({0..1} - s) (\x. vector_derivative (g1 +++ g2) (at x))" - and g12D: "\x\{0..1} - s. g1 +++ g2 differentiable at x" + obtain S where "finite S" + and co12: "continuous_on ({0..1} - S) (\x. vector_derivative (g1 +++ g2) (at x))" + and g12D: "\x\{0..1} - S. g1 +++ g2 differentiable at x" using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) - then have g1D: "g1 differentiable at x" if "x \ {0..1} - insert 1 (( * ) 2 ` s)" for x - apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (( * )(inverse 2))" in differentiable_transform_within) - using that - apply (simp_all add: dist_real_def joinpaths_def) - apply (rule differentiable_chain_at derivative_intros | force)+ - done + have g1D: "g1 differentiable at x" if "x \ {0..1} - insert 1 (( * ) 2 ` S)" for x + proof (rule differentiable_transform_within) + show "g1 +++ g2 \ ( * ) (inverse 2) differentiable at x" + using that g12D + apply (simp only: joinpaths_def) + by (rule differentiable_chain_at derivative_intros | force)+ + show "\x'. \dist x' x < dist (x/2) (1/2)\ + \ (g1 +++ g2 \ ( * ) (inverse 2)) x' = g1 x'" + using that by (auto simp add: dist_real_def joinpaths_def) + qed (use that in \auto simp: dist_real_def\) have [simp]: "vector_derivative (g1 \ ( * ) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)" - if "x \ {0..1} - insert 1 (( * ) 2 ` s)" for x + if "x \ {0..1} - insert 1 (( * ) 2 ` S)" for x apply (subst vector_derivative_chain_at) using that apply (rule derivative_eq_intros g1D | simp)+ done - have "continuous_on ({0..1/2} - insert (1/2) s) (\x. vector_derivative (g1 +++ g2) (at x))" + have "continuous_on ({0..1/2} - insert (1/2) S) (\x. vector_derivative (g1 +++ g2) (at x))" using co12 by (rule continuous_on_subset) force - then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\x. vector_derivative (g1 o ( * )2) (at x))" - apply (rule continuous_on_eq [OF _ vector_derivative_at]) - apply (rule_tac f="g1 o ( * )2" and d="dist x (1/2)" in has_vector_derivative_transform_within) - apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric]) - apply (force intro: g1D differentiable_chain_at) - apply auto - done - have "continuous_on ({0..1} - insert 1 (( * ) 2 ` s)) + then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\x. vector_derivative (g1 o ( * )2) (at x))" + proof (rule continuous_on_eq [OF _ vector_derivative_at]) + show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \ ( * ) 2) (at x)) (at x)" + if "x \ {0..1/2} - insert (1/2) S" for x + proof (rule has_vector_derivative_transform_within) + show "(g1 \ ( * ) 2 has_vector_derivative vector_derivative (g1 \ ( * ) 2) (at x)) (at x)" + using that + by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric]) + show "\x'. \dist x' x < dist x (1/2)\ \ (g1 \ ( * ) 2) x' = (g1 +++ g2) x'" + using that by (auto simp: dist_norm joinpaths_def) + qed (use that in \auto simp: dist_norm\) + qed + have "continuous_on ({0..1} - insert 1 (( * ) 2 ` S)) ((\x. 1/2 * vector_derivative (g1 o ( * )2) (at x)) o ( * )(1/2))" apply (rule continuous_intros)+ using coDhalf apply (simp add: scaleR_conv_of_real image_set_diff image_image) done - then have con_g1: "continuous_on ({0..1} - insert 1 (( * ) 2 ` s)) (\x. vector_derivative g1 (at x))" + then have con_g1: "continuous_on ({0..1} - insert 1 (( * ) 2 ` S)) (\x. vector_derivative g1 (at x))" by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) have "continuous_on {0..1} g1" using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast - with \finite s\ show ?thesis + with \finite S\ show ?thesis apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) - apply (rule_tac x="insert 1 ((( * )2)`s)" in exI) + apply (rule_tac x="insert 1 ((( * )2)`S)" in exI) apply (simp add: g1D con_g1) done qed @@ -602,44 +650,53 @@ assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2" shows "g2 piecewise_C1_differentiable_on {0..1}" proof - - obtain s where "finite s" - and co12: "continuous_on ({0..1} - s) (\x. vector_derivative (g1 +++ g2) (at x))" - and g12D: "\x\{0..1} - s. g1 +++ g2 differentiable at x" + obtain S where "finite S" + and co12: "continuous_on ({0..1} - S) (\x. vector_derivative (g1 +++ g2) (at x))" + and g12D: "\x\{0..1} - S. g1 +++ g2 differentiable at x" using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) - then have g2D: "g2 differentiable at x" if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` s)" for x - apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\x. (x+1)/2)" in differentiable_transform_within) - using that - apply (simp_all add: dist_real_def joinpaths_def) - apply (auto simp: dist_real_def joinpaths_def field_simps) - apply (rule differentiable_chain_at derivative_intros | force)+ - apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps) - apply assumption - done + have g2D: "g2 differentiable at x" if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` S)" for x + proof (rule differentiable_transform_within) + show "g1 +++ g2 \ (\x. (x + 1) / 2) differentiable at x" + using g12D that + apply (simp only: joinpaths_def) + apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps) + apply (rule differentiable_chain_at derivative_intros | force)+ + done + show "\x'. dist x' x < dist ((x + 1) / 2) (1/2) \ (g1 +++ g2 \ (\x. (x + 1) / 2)) x' = g2 x'" + using that by (auto simp: dist_real_def joinpaths_def field_simps) + qed (use that in \auto simp: dist_norm\) have [simp]: "vector_derivative (g2 \ (\x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)" - if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` s)" for x + if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` S)" for x using that by (auto simp: vector_derivative_chain_at divide_simps g2D) - have "continuous_on ({1/2..1} - insert (1/2) s) (\x. vector_derivative (g1 +++ g2) (at x))" + have "continuous_on ({1/2..1} - insert (1/2) S) (\x. vector_derivative (g1 +++ g2) (at x))" using co12 by (rule continuous_on_subset) force - then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) s) (\x. vector_derivative (g2 o (\x. 2*x-1)) (at x))" - apply (rule continuous_on_eq [OF _ vector_derivative_at]) - apply (rule_tac f="g2 o (\x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within) - apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric] - intro!: g2D differentiable_chain_at) - done - have [simp]: "((\x. (x+1) / 2) ` ({0..1} - insert 0 ((\x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)" + then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) S) (\x. vector_derivative (g2 o (\x. 2*x-1)) (at x))" + proof (rule continuous_on_eq [OF _ vector_derivative_at]) + show "(g1 +++ g2 has_vector_derivative vector_derivative (g2 \ (\x. 2 * x - 1)) (at x)) + (at x)" + if "x \ {1 / 2..1} - insert (1 / 2) S" for x + proof (rule_tac f="g2 o (\x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within) + show "(g2 \ (\x. 2 * x - 1) has_vector_derivative vector_derivative (g2 \ (\x. 2 * x - 1)) (at x)) + (at x)" + using that by (force intro: g2D differentiable_chain_at simp: vector_derivative_works [symmetric]) + show "\x'. \dist x' x < dist (3 / 4) ((x + 1) / 2)\ \ (g2 \ (\x. 2 * x - 1)) x' = (g1 +++ g2) x'" + using that by (auto simp: dist_norm joinpaths_def add_divide_distrib) + qed (use that in \auto simp: dist_norm\) + qed + have [simp]: "((\x. (x+1) / 2) ` ({0..1} - insert 0 ((\x. 2 * x - 1) ` S))) = ({1/2..1} - insert (1/2) S)" apply (simp add: image_set_diff inj_on_def image_image) apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib) done - have "continuous_on ({0..1} - insert 0 ((\x. 2*x-1) ` s)) + have "continuous_on ({0..1} - insert 0 ((\x. 2*x-1) ` S)) ((\x. 1/2 * vector_derivative (g2 \ (\x. 2*x-1)) (at x)) o (\x. (x+1)/2))" by (rule continuous_intros | simp add: coDhalf)+ - then have con_g2: "continuous_on ({0..1} - insert 0 ((\x. 2*x-1) ` s)) (\x. vector_derivative g2 (at x))" + then have con_g2: "continuous_on ({0..1} - insert 0 ((\x. 2*x-1) ` S)) (\x. vector_derivative g2 (at x))" by (rule continuous_on_eq) (simp add: scaleR_conv_of_real) have "continuous_on {0..1} g2" using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast - with \finite s\ show ?thesis + with \finite S\ show ?thesis apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) - apply (rule_tac x="insert 0 ((\x. 2 * x - 1) ` s)" in exI) + apply (rule_tac x="insert 0 ((\x. 2 * x - 1) ` S)" in exI) apply (simp add: g2D con_g2) done qed @@ -675,32 +732,32 @@ and con: "continuous_on (path_image g) (deriv f)" shows "valid_path (f o g)" proof - - obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1} - s" + obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S" using \valid_path g\ unfolding valid_path_def piecewise_C1_differentiable_on_def by auto - have "f \ g differentiable at t" when "t\{0..1} - s" for t + have "f \ g differentiable at t" when "t\{0..1} - S" for t proof (rule differentiable_chain_at) show "g differentiable at t" using \valid_path g\ - by (meson C1_differentiable_on_eq \g C1_differentiable_on {0..1} - s\ that) + by (meson C1_differentiable_on_eq \g C1_differentiable_on {0..1} - S\ that) next have "g t\path_image g" using that DiffD1 image_eqI path_image_def by metis then show "f differentiable at (g t)" using der[THEN field_differentiable_imp_differentiable] by auto qed - moreover have "continuous_on ({0..1} - s) (\x. vector_derivative (f \ g) (at x))" + moreover have "continuous_on ({0..1} - S) (\x. vector_derivative (f \ g) (at x))" proof (rule continuous_on_eq [where f = "\x. vector_derivative g (at x) * deriv f (g x)"], rule continuous_intros) - show "continuous_on ({0..1} - s) (\x. vector_derivative g (at x))" + show "continuous_on ({0..1} - S) (\x. vector_derivative g (at x))" using g_diff C1_differentiable_on_eq by auto next have "continuous_on {0..1} (\x. deriv f (g x))" using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def] \valid_path g\ piecewise_C1_differentiable_on_def valid_path_def by blast - then show "continuous_on ({0..1} - s) (\x. deriv f (g x))" + then show "continuous_on ({0..1} - S) (\x. deriv f (g x))" using continuous_on_subset by blast next show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \ g) (at t)" - when "t \ {0..1} - s" for t + when "t \ {0..1} - S" for t proof (rule vector_derivative_chain_at_general[symmetric]) show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that) next @@ -708,14 +765,14 @@ then show "f field_differentiable at (g t)" using der by auto qed qed - ultimately have "f o g C1_differentiable_on {0..1} - s" + ultimately have "f o g C1_differentiable_on {0..1} - S" using C1_differentiable_on_eq by blast moreover have "path (f \ g)" apply (rule path_continuous_image[OF valid_path_imp_path[OF \valid_path g\]]) using der by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at) ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def - using \finite s\ by auto + using \finite S\ by auto qed @@ -763,24 +820,17 @@ lemma has_contour_integral_integrable: "(f has_contour_integral i) g \ f contour_integrable_on g" using contour_integrable_on_def by blast -(* Show that we can forget about the localized derivative.*) - -lemma vector_derivative_within_interior: - "\x \ interior s; NO_MATCH UNIV s\ - \ vector_derivative f (at x within s) = vector_derivative f (at x)" - apply (simp add: vector_derivative_def has_vector_derivative_def has_derivative_def netlimit_within_interior) - apply (subst lim_within_interior, auto) - done +subsubsection\Show that we can forget about the localized derivative.\ lemma has_integral_localized_vector_derivative: "((\x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \ ((\x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}" proof - - have "{a..b} - {a,b} = interior {a..b}" + have *: "{a..b} - {a,b} = interior {a..b}" by (simp add: atLeastAtMost_diff_ends) show ?thesis apply (rule has_integral_spike_eq [of "{a,b}"]) - apply (auto simp: vector_derivative_within_interior) + apply (auto simp: at_within_interior [of _ "{a..b}"]) done qed @@ -805,17 +855,16 @@ assumes "valid_path g" shows "valid_path(reversepath g)" proof - - obtain s where "finite s" "g C1_differentiable_on ({0..1} - s)" + obtain S where "finite S" and S: "g C1_differentiable_on ({0..1} - S)" using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) - then have "finite ((-) 1 ` s)" "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` s))" - apply (auto simp: reversepath_def) + then have "finite ((-) 1 ` S)" + by auto + moreover have "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` S))" + unfolding reversepath_def apply (rule C1_differentiable_compose [of "\x::real. 1-x" _ g, unfolded o_def]) - apply (auto simp: C1_differentiable_on_eq) - apply (rule continuous_intros, force) - apply (force elim!: continuous_on_subset) - apply (simp add: finite_vimageI inj_on_def) - done - then show ?thesis using assms + using S + by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq continuous_on_const elim!: continuous_on_subset)+ + ultimately show ?thesis using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric]) qed @@ -823,38 +872,37 @@ using valid_path_imp_reverse by force lemma has_contour_integral_reversepath: - assumes "valid_path g" "(f has_contour_integral i) g" + assumes "valid_path g" and f: "(f has_contour_integral i) g" shows "(f has_contour_integral (-i)) (reversepath g)" proof - - { fix s x - assume xs: "g C1_differentiable_on ({0..1} - s)" "x \ (-) 1 ` s" "0 \ x" "x \ 1" - have "vector_derivative (\x. g (1 - x)) (at x within {0..1}) = + { fix S x + assume xs: "g C1_differentiable_on ({0..1} - S)" "x \ (-) 1 ` S" "0 \ x" "x \ 1" + have "vector_derivative (\x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})" - proof - - obtain f' where f': "(g has_vector_derivative f') (at (1 - x))" - using xs - by (force simp: has_vector_derivative_def C1_differentiable_on_def) - have "(g o (\x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)" - apply (rule vector_diff_chain_within) - apply (intro vector_diff_chain_within derivative_eq_intros | simp)+ - apply (rule has_vector_derivative_at_within [OF f']) - done - then have mf': "((\x. g (1 - x)) has_vector_derivative -f') (at x)" - by (simp add: o_def) - show ?thesis - using xs - by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f']) - qed + proof - + obtain f' where f': "(g has_vector_derivative f') (at (1 - x))" + using xs + by (force simp: has_vector_derivative_def C1_differentiable_on_def) + have "(g o (\x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)" + by (intro vector_diff_chain_within has_vector_derivative_at_within [OF f'] derivative_eq_intros | simp)+ + then have mf': "((\x. g (1 - x)) has_vector_derivative -f') (at x)" + by (simp add: o_def) + show ?thesis + using xs + by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f']) + qed } note * = this - have 01: "{0..1::real} = cbox 0 1" - by simp - show ?thesis using assms - apply (auto simp: has_contour_integral_def) - apply (drule has_integral_affinity01 [where m= "-1" and c=1]) - apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def) - apply (drule has_integral_neg) - apply (rule_tac S = "(\x. 1 - x) ` s" in has_integral_spike_finite) - apply (auto simp: *) + obtain S where S: "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S" + using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) + have "((\x. - (f (g (1 - x)) * vector_derivative g (at (1 - x) within {0..1}))) has_integral -i) + {0..1}" + using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]] + by (simp add: has_integral_neg) + then show ?thesis + using S + apply (clarsimp simp: reversepath_def has_contour_integral_def) + apply (rule_tac S = "(\x. 1 - x) ` S" in has_integral_spike_finite) + apply (auto simp: *) done qed @@ -891,7 +939,6 @@ apply (rule piecewise_C1_differentiable_compose) using assms apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths) - apply (rule continuous_intros | simp)+ apply (force intro: finite_vimageI [where h = "( * )2"] inj_onI) done moreover have "(g2 o (\x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}" @@ -1179,7 +1226,7 @@ [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]]) using s g assms x apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath - vector_derivative_within_interior vector_derivative_works [symmetric]) + at_within_interior [of _ "{0..1}"] vector_derivative_works [symmetric]) apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"]) apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm) done @@ -1268,6 +1315,9 @@ lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)" by (simp add: has_contour_integral_linepath) +lemma has_contour_integral_trivial_iff [simp]: "(f has_contour_integral i) (linepath a a) \ i=0" + using has_contour_integral_unique by blast + lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0" using has_contour_integral_trivial contour_integral_unique by blast @@ -1738,11 +1788,7 @@ proof (cases "k = 0 \ k = 1") case True then show ?thesis - using assms - apply auto - apply (metis add.left_neutral has_contour_integral_trivial has_contour_integral_unique) - apply (metis add.right_neutral has_contour_integral_trivial has_contour_integral_unique) - done + using assms by auto next case False then have k: "0 < k" "k < 1" "complex_of_real k \ 1" @@ -1758,12 +1804,9 @@ apply (simp add: real_vector.scale_left_distrib [symmetric] divide_simps) done have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral i) {0..k}" - using * k - apply - - apply (drule has_integral_affinity [of _ _ 0 "1::real" "inverse k" "0", simplified]) - apply (simp_all add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost ** c) - apply (drule has_integral_cmul [where c = "inverse k"]) - apply (simp add: has_integral_cmul) + using k has_integral_affinity01 [OF *, of "inverse k" "0"] + apply (simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost ** c) + apply (auto dest: has_integral_cmul [where c = "inverse k"]) done } note fi = this { assume *: "((\x. f ((1 - x) *\<^sub>R c + x *\<^sub>R b) * (b - c)) has_integral j) {0..1}" @@ -1774,12 +1817,9 @@ apply (simp add: field_simps) done have "((\x. f ((1 - x) *\<^sub>R a + x *\<^sub>R b) * (b - a)) has_integral j) {k..1}" - using * k - apply - - apply (drule has_integral_affinity [of _ _ 0 "1::real" "inverse(1 - k)" "-(k/(1 - k))", simplified]) - apply (simp_all add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc) - apply (drule has_integral_cmul [where k = "(1 - k) *\<^sub>R j" and c = "inverse (1 - k)"]) - apply (simp add: has_integral_cmul) + using k has_integral_affinity01 [OF *, of "inverse(1 - k)" "-(k/(1 - k))"] + apply (simp add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc) + apply (auto dest: has_integral_cmul [where k = "(1 - k) *\<^sub>R j" and c = "inverse (1 - k)"]) done } note fj = this show ?thesis @@ -1836,7 +1876,7 @@ using c by (auto simp: closed_segment_def algebra_simps intro!: contour_integral_split [OF f]) -(* The special case of midpoints used in the main quadrisection.*) +text\The special case of midpoints used in the main quadrisection\ lemma has_contour_integral_midpoint: assumes "(f has_contour_integral i) (linepath a (midpoint a b))" @@ -5119,7 +5159,7 @@ lemma circlepath_minus: "circlepath z (-r) x = circlepath z r (x + 1/2)" proof - - have "z + of_real r * exp (2 * pi * \ * (x + 1 / 2)) = + have "z + of_real r * exp (2 * pi * \ * (x + 1/2)) = z + of_real r * exp (2 * pi * \ * x + pi * \)" by (simp add: divide_simps) (simp add: algebra_simps) also have "... = z - r * exp (2 * pi * \ * x)" diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Sat May 26 10:11:11 2018 +0100 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Sat May 26 22:11:55 2018 +0100 @@ -47,26 +47,6 @@ lemma lambda_one: "(\x::'a::monoid_mult. x) = ( * ) 1" by auto -lemma continuous_mult_left: - fixes c::"'a::real_normed_algebra" - shows "continuous F f \ continuous F (\x. c * f x)" -by (rule continuous_mult [OF continuous_const]) - -lemma continuous_mult_right: - fixes c::"'a::real_normed_algebra" - shows "continuous F f \ continuous F (\x. f x * c)" -by (rule continuous_mult [OF _ continuous_const]) - -lemma continuous_on_mult_left: - fixes c::"'a::real_normed_algebra" - shows "continuous_on s f \ continuous_on s (\x. c * f x)" -by (rule continuous_on_mult [OF continuous_on_const]) - -lemma continuous_on_mult_right: - fixes c::"'a::real_normed_algebra" - shows "continuous_on s f \ continuous_on s (\x. f x * c)" -by (rule continuous_on_mult [OF _ continuous_on_const]) - lemma uniformly_continuous_on_cmul_right [continuous_intros]: fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. f x * c)" diff -r b9160ca067ae -r 69d680e94961 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Sat May 26 10:11:11 2018 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Sat May 26 22:11:55 2018 +0100 @@ -8371,15 +8371,12 @@ (\x \ sphere a r. g x = f x))" (is "?lhs = ?rhs") proof%unimportant (cases r "0::real" rule: linorder_cases) - case less - then show ?thesis by simp -next case equal - with continuous_on_const show ?thesis + then show ?thesis apply (auto simp: homotopic_with) apply (rule_tac x="\x. h (0, a)" in exI) - apply (fastforce simp add:) - done + apply (fastforce simp add:) + using continuous_on_const by blast next case greater let ?P = "continuous_on {x. norm(x - a) = r} f \ f ` {x. norm(x - a) = r} \ S" @@ -8494,6 +8491,6 @@ qed ultimately show ?thesis by meson -qed +qed simp end diff -r b9160ca067ae -r 69d680e94961 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sat May 26 10:11:11 2018 +0100 +++ b/src/HOL/Limits.thy Sat May 26 22:11:55 2018 +0100 @@ -842,6 +842,32 @@ lemmas tendsto_mult_right_zero = bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] + +lemma continuous_mult_left: + fixes c::"'a::real_normed_algebra" + shows "continuous F f \ continuous F (\x. c * f x)" +by (rule continuous_mult [OF continuous_const]) + +lemma continuous_mult_right: + fixes c::"'a::real_normed_algebra" + shows "continuous F f \ continuous F (\x. f x * c)" +by (rule continuous_mult [OF _ continuous_const]) + +lemma continuous_on_mult_left: + fixes c::"'a::real_normed_algebra" + shows "continuous_on s f \ continuous_on s (\x. c * f x)" +by (rule continuous_on_mult [OF continuous_on_const]) + +lemma continuous_on_mult_right: + fixes c::"'a::real_normed_algebra" + shows "continuous_on s f \ continuous_on s (\x. f x * c)" +by (rule continuous_on_mult [OF _ continuous_on_const]) + +lemma continuous_on_mult_const [simp]: + fixes c::"'a::real_normed_algebra" + shows "continuous_on s (( * ) c)" + by (intro continuous_on_mult_left continuous_on_id) + lemma tendsto_divide_zero: fixes c :: "'a::real_normed_field" shows "(f \ 0) F \ ((\x. f x / c) \ 0) F" diff -r b9160ca067ae -r 69d680e94961 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Sat May 26 10:11:11 2018 +0100 +++ b/src/HOL/Topological_Spaces.thy Sat May 26 22:11:55 2018 +0100 @@ -1924,13 +1924,13 @@ continuous_on (s \ t) (\x. if P x then f x else g x)" by (rule continuous_on_If) auto -lemma continuous_on_id[continuous_intros]: "continuous_on s (\x. x)" +lemma continuous_on_id[continuous_intros,simp]: "continuous_on s (\x. x)" unfolding continuous_on_def by fast -lemma continuous_on_id'[continuous_intros]: "continuous_on s id" +lemma continuous_on_id'[continuous_intros,simp]: "continuous_on s id" unfolding continuous_on_def id_def by fast -lemma continuous_on_const[continuous_intros]: "continuous_on s (\x. c)" +lemma continuous_on_const[continuous_intros,simp]: "continuous_on s (\x. c)" unfolding continuous_on_def by auto lemma continuous_on_subset: "continuous_on s f \ t \ s \ continuous_on t f"