--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Aug 22 14:34:26 2017 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Aug 22 21:36:48 2017 +0200
@@ -367,6 +367,14 @@
"(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
unfolding holomorphic_on_def by (metis field_differentiable_sum)
+lemma holomorphic_pochhammer [holomorphic_intros]:
+ "f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
+ by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)
+
+lemma holomorphic_on_scaleR [holomorphic_intros]:
+ "f holomorphic_on A \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) holomorphic_on A"
+ by (auto simp: scaleR_conv_of_real intro!: holomorphic_intros)
+
lemma DERIV_deriv_iff_field_differentiable:
"DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
unfolding field_differentiable_def by (metis DERIV_imp_deriv)
--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Aug 22 14:34:26 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Aug 22 21:36:48 2017 +0200
@@ -3928,6 +3928,166 @@
subsection \<open>More facts about poles and residues\<close>
+lemma zorder_cong:
+ assumes "eventually (\<lambda>z. f z = g z) (nhds z)" "z = z'"
+ shows "zorder f z = zorder g z'"
+proof -
+ let ?P = "(\<lambda>f n h r. 0 < r \<and> h holomorphic_on cball z r \<and>
+ (\<forall>w\<in>cball z r. f w = h w * (w - z) ^ n \<and> h w \<noteq> 0))"
+ have "(\<lambda>n. n > 0 \<and> (\<exists>h r. ?P f n h r)) = (\<lambda>n. n > 0 \<and> (\<exists>h r. ?P g n h r))"
+ proof (intro ext conj_cong refl iff_exI[where ?'a = "complex \<Rightarrow> complex"], goal_cases)
+ case (1 n h)
+ have *: "\<exists>r. ?P g n h r" if "\<exists>r. ?P f n h r" and "eventually (\<lambda>x. f x = g x) (nhds z)" for f g
+ proof -
+ from that(1) obtain r where "?P f n h r" by blast
+ moreover from that(2) obtain r' where "r' > 0" "\<And>w. dist w z < r' \<Longrightarrow> f w = g w"
+ by (auto simp: eventually_nhds_metric)
+ hence "\<forall>w\<in>cball z (r'/2). f w = g w" by (auto simp: dist_commute)
+ ultimately show ?thesis using \<open>r' > 0\<close>
+ by (intro exI[of _ "min r (r'/2)"]) (auto simp: cball_def)
+ qed
+ from assms have eq': "eventually (\<lambda>z. g z = f z) (nhds z)"
+ by (simp add: eq_commute)
+ show ?case
+ by (rule iffI[OF *[OF _ assms(1)] *[OF _ eq']])
+ qed
+ with assms(2) show ?thesis unfolding zorder_def by simp
+qed
+
+lemma porder_cong:
+ assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'"
+ shows "porder f z = porder g z'"
+proof -
+ from assms(1) have *: "eventually (\<lambda>w. w \<noteq> z \<longrightarrow> f w = g w) (nhds z)"
+ by (auto simp: eventually_at_filter)
+ from assms(2) show ?thesis
+ unfolding porder_def Let_def
+ by (intro zorder_cong eventually_mono [OF *]) auto
+qed
+
+lemma zer_poly_cong:
+ assumes "eventually (\<lambda>z. f z = g z) (nhds z)" "z = z'"
+ shows "zer_poly f z = zer_poly g z'"
+ unfolding zer_poly_def
+proof (rule Eps_cong, goal_cases)
+ case (1 h)
+ let ?P = "\<lambda>w f. f w = h w * (w - z) ^ zorder f z \<and> h w \<noteq> 0"
+ from assms have eq': "eventually (\<lambda>z. g z = f z) (nhds z)"
+ by (simp add: eq_commute)
+ have "\<exists>r>0. h holomorphic_on cball z r \<and> (\<forall>w\<in>cball z r. ?P w g)"
+ if "r > 0" "h holomorphic_on cball z r" "\<And>w. w \<in> cball z r \<Longrightarrow> ?P w f"
+ "eventually (\<lambda>z. f z = g z) (nhds z)" for f g r
+ proof -
+ from that have [simp]: "zorder f z = zorder g z"
+ by (intro zorder_cong) auto
+ from that(4) obtain r' where r': "r' > 0" "\<And>w. w \<in> ball z r' \<Longrightarrow> g w = f w"
+ by (auto simp: eventually_nhds_metric ball_def dist_commute)
+ define R where "R = min r (r' / 2)"
+ have "R > 0" "cball z R \<subseteq> cball z r" "cball z R \<subseteq> ball z r'"
+ using that(1) r' by (auto simp: R_def)
+ with that(1,2,3) r'
+ have "R > 0" "h holomorphic_on cball z R" "\<forall>w\<in>cball z R. ?P w g"
+ by force+
+ thus ?thesis by blast
+ qed
+ from this[of _ f g] and this[of _ g f] and assms and eq'
+ show ?case by blast
+qed
+
+lemma pol_poly_cong:
+ assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'"
+ shows "pol_poly f z = pol_poly g z'"
+proof -
+ from assms have *: "eventually (\<lambda>w. w \<noteq> z \<longrightarrow> f w = g w) (nhds z)"
+ by (auto simp: eventually_at_filter)
+ have "zer_poly (\<lambda>x. if x = z then 0 else inverse (f x)) z =
+ zer_poly (\<lambda>x. if x = z' then 0 else inverse (g x)) z"
+ by (intro zer_poly_cong eventually_mono[OF *] refl) (auto simp: assms(2))
+ thus "pol_poly f z = pol_poly g z'"
+ by (simp add: pol_poly_def Let_def o_def fun_eq_iff assms(2))
+qed
+
+lemma porder_nonzero_div_power:
+ assumes "open s" "z \<in> s" "f holomorphic_on s" "f z \<noteq> 0" "n > 0"
+ shows "porder (\<lambda>w. f w / (w - z) ^ n) z = n"
+proof -
+ let ?s' = "(f -` (-{0}) \<inter> s)"
+ have "continuous_on s f"
+ by (rule holomorphic_on_imp_continuous_on) fact
+ moreover have "open (-{0::complex})" by auto
+ ultimately have s': "open ?s'"
+ unfolding continuous_on_open_vimage[OF \<open>open s\<close>] by blast
+ show ?thesis unfolding Let_def porder_def
+ proof (rule zorder_eqI)
+ show "(\<lambda>x. inverse (f x)) holomorphic_on ?s'"
+ using assms by (auto intro!: holomorphic_intros)
+ qed (insert assms s', auto simp: field_simps)
+qed
+
+lemma is_pole_inverse_power: "n > 0 \<Longrightarrow> is_pole (\<lambda>z::complex. 1 / (z - a) ^ n) a"
+ unfolding is_pole_def inverse_eq_divide [symmetric]
+ by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros)
+ (auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros)
+
+lemma is_pole_inverse: "is_pole (\<lambda>z::complex. 1 / (z - a)) a"
+ using is_pole_inverse_power[of 1 a] by simp
+
+lemma is_pole_divide:
+ fixes f :: "'a :: t2_space \<Rightarrow> 'b :: real_normed_field"
+ assumes "isCont f z" "filterlim g (at 0) (at z)" "f z \<noteq> 0"
+ shows "is_pole (\<lambda>z. f z / g z) z"
+proof -
+ have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
+ by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"]
+ filterlim_compose[OF filterlim_inverse_at_infinity])+
+ (insert assms, auto simp: isCont_def)
+ thus ?thesis by (simp add: divide_simps is_pole_def)
+qed
+
+lemma is_pole_basic:
+ assumes "f holomorphic_on A" "open A" "z \<in> A" "f z \<noteq> 0" "n > 0"
+ shows "is_pole (\<lambda>w. f w / (w - z) ^ n) z"
+proof (rule is_pole_divide)
+ have "continuous_on A f" by (rule holomorphic_on_imp_continuous_on) fact
+ with assms show "isCont f z" by (auto simp: continuous_on_eq_continuous_at)
+ have "filterlim (\<lambda>w. (w - z) ^ n) (nhds 0) (at z)"
+ using assms by (auto intro!: tendsto_eq_intros)
+ thus "filterlim (\<lambda>w. (w - z) ^ n) (at 0) (at z)"
+ by (intro filterlim_atI tendsto_eq_intros)
+ (insert assms, auto simp: eventually_at_filter)
+qed fact+
+
+lemma is_pole_basic':
+ assumes "f holomorphic_on A" "open A" "0 \<in> A" "f 0 \<noteq> 0" "n > 0"
+ shows "is_pole (\<lambda>w. f w / w ^ n) 0"
+ using is_pole_basic[of f A 0] assms by simp
+
+lemma zer_poly_eq:
+ assumes "open s" "connected s" "z \<in> s" "f holomorphic_on s" "f z = 0" "\<exists>w\<in>s. f w \<noteq> 0"
+ shows "eventually (\<lambda>w. zer_poly f z w = f w / (w - z) ^ zorder f z) (at z)"
+proof -
+ from zorder_exist [OF assms] obtain r where r: "r > 0"
+ and "\<forall>w\<in>cball z r. f w = zer_poly f z w * (w - z) ^ zorder f z" by blast
+ hence *: "\<forall>w\<in>ball z r - {z}. zer_poly f z w = f w / (w - z) ^ zorder f z"
+ by (auto simp: field_simps)
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r eventually_at_ball'[of r z UNIV] by auto
+ thus ?thesis by eventually_elim (insert *, auto)
+qed
+
+lemma pol_poly_eq:
+ assumes "open s" "z \<in> s" "f holomorphic_on s - {z}" "is_pole f z" "\<exists>w\<in>s. f w \<noteq> 0"
+ shows "eventually (\<lambda>w. pol_poly f z w = f w * (w - z) ^ porder f z) (at z)"
+proof -
+ from porder_exist[OF assms(1-4)] obtain r where r: "r > 0"
+ and "\<forall>w\<in>cball z r. w \<noteq> z \<longrightarrow> f w = pol_poly f z w / (w - z) ^ porder f z" by blast
+ hence *: "\<forall>w\<in>ball z r - {z}. pol_poly f z w = f w * (w - z) ^ porder f z"
+ by (auto simp: field_simps)
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r eventually_at_ball'[of r z UNIV] by auto
+ thus ?thesis by eventually_elim (insert *, auto)
+qed
+
lemma lhopital_complex_simple:
assumes "(f has_field_derivative f') (at z)"
assumes "(g has_field_derivative g') (at z)"
--- a/src/HOL/Analysis/Inner_Product.thy Tue Aug 22 14:34:26 2017 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy Tue Aug 22 21:36:48 2017 +0200
@@ -305,6 +305,56 @@
unfolding inner_complex_def by simp
+lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
+ by (simp only: power2_norm_eq_inner) (* TODO: move? *)
+
+lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> inner x x = a\<^sup>2"
+ by (auto simp add: norm_eq_sqrt_inner)
+
+lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<^sup>2"
+ apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
+ apply arith
+ done
+
+lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> inner x x \<ge> a\<^sup>2"
+ apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
+ apply arith
+ done
+
+lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> inner x x < a\<^sup>2"
+ by (metis not_le norm_ge_square)
+
+lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> inner x x > a\<^sup>2"
+ by (metis norm_le_square not_less)
+
+text\<open>Dot product in terms of the norm rather than conversely.\<close>
+
+lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
+ inner_scaleR_left inner_scaleR_right
+
+lemma dot_norm: "inner x y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
+ by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
+
+lemma dot_norm_neg: "inner x y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
+ by (simp only: power2_norm_eq_inner inner_simps inner_commute)
+ (auto simp add: algebra_simps)
+
+lemma of_real_inner_1 [simp]:
+ "inner (of_real x) (1 :: 'a :: {real_inner, real_normed_algebra_1}) = x"
+ by (simp add: of_real_def dot_square_norm)
+
+lemma summable_of_real_iff:
+ "summable (\<lambda>x. of_real (f x) :: 'a :: {real_normed_algebra_1,real_inner}) \<longleftrightarrow> summable f"
+proof
+ assume *: "summable (\<lambda>x. of_real (f x) :: 'a)"
+ interpret bounded_linear "\<lambda>x::'a. inner x 1"
+ by (rule bounded_linear_inner_left)
+ from summable [OF *] show "summable f" by simp
+qed (auto intro: summable_of_real)
+
+
subsection \<open>Gradient derivative\<close>
definition
--- a/src/HOL/Analysis/Linear_Algebra.thy Tue Aug 22 14:34:26 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue Aug 22 21:36:48 2017 +0200
@@ -1397,43 +1397,6 @@
lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
by (simp add: norm_eq_sqrt_inner)
-text\<open>Squaring equations and inequalities involving norms.\<close>
-
-lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
- by (simp only: power2_norm_eq_inner) (* TODO: move? *)
-
-lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
- by (auto simp add: norm_eq_sqrt_inner)
-
-lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
- apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
- using norm_ge_zero[of x]
- apply arith
- done
-
-lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
- apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
- using norm_ge_zero[of x]
- apply arith
- done
-
-lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
- by (metis not_le norm_ge_square)
-
-lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
- by (metis norm_le_square not_less)
-
-text\<open>Dot product in terms of the norm rather than conversely.\<close>
-
-lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
- inner_scaleR_left inner_scaleR_right
-
-lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
- by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
-
-lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
- by (simp only: power2_norm_eq_inner inner_simps inner_commute)
- (auto simp add: algebra_simps)
text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
--- a/src/HOL/Library/Permutations.thy Tue Aug 22 14:34:26 2017 +0200
+++ b/src/HOL/Library/Permutations.thy Tue Aug 22 21:36:48 2017 +0200
@@ -204,6 +204,82 @@
by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv])
+subsection \<open>Mapping permutations with bijections\<close>
+
+lemma bij_betw_permutations:
+ assumes "bij_betw f A B"
+ shows "bij_betw (\<lambda>\<pi> x. if x \<in> B then f (\<pi> (inv_into A f x)) else x)
+ {\<pi>. \<pi> permutes A} {\<pi>. \<pi> permutes B}" (is "bij_betw ?f _ _")
+proof -
+ let ?g = "(\<lambda>\<pi> x. if x \<in> A then inv_into A f (\<pi> (f x)) else x)"
+ show ?thesis
+ proof (rule bij_betw_byWitness [of _ ?g], goal_cases)
+ case 3
+ show ?case using permutes_bij_inv_into[OF _ assms] by auto
+ next
+ case 4
+ have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms)
+ {
+ fix \<pi> assume "\<pi> permutes B"
+ from permutes_bij_inv_into[OF this bij_inv] and assms
+ have "(\<lambda>x. if x \<in> A then inv_into A f (\<pi> (f x)) else x) permutes A"
+ by (simp add: inv_into_inv_into_eq cong: if_cong)
+ }
+ from this show ?case by (auto simp: permutes_inv)
+ next
+ case 1
+ thus ?case using assms
+ by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left
+ dest: bij_betwE)
+ next
+ case 2
+ moreover have "bij_betw (inv_into A f) B A"
+ by (intro bij_betw_inv_into assms)
+ ultimately show ?case using assms
+ by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right
+ dest: bij_betwE)
+ qed
+qed
+
+lemma bij_betw_derangements:
+ assumes "bij_betw f A B"
+ shows "bij_betw (\<lambda>\<pi> x. if x \<in> B then f (\<pi> (inv_into A f x)) else x)
+ {\<pi>. \<pi> permutes A \<and> (\<forall>x\<in>A. \<pi> x \<noteq> x)} {\<pi>. \<pi> permutes B \<and> (\<forall>x\<in>B. \<pi> x \<noteq> x)}"
+ (is "bij_betw ?f _ _")
+proof -
+ let ?g = "(\<lambda>\<pi> x. if x \<in> A then inv_into A f (\<pi> (f x)) else x)"
+ show ?thesis
+ proof (rule bij_betw_byWitness [of _ ?g], goal_cases)
+ case 3
+ have "?f \<pi> x \<noteq> x" if "\<pi> permutes A" "\<And>x. x \<in> A \<Longrightarrow> \<pi> x \<noteq> x" "x \<in> B" for \<pi> x
+ using that and assms by (metis bij_betwE bij_betw_imp_inj_on bij_betw_imp_surj_on
+ inv_into_f_f inv_into_into permutes_imp_bij)
+ with permutes_bij_inv_into[OF _ assms] show ?case by auto
+ next
+ case 4
+ have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms)
+ have "?g \<pi> permutes A" if "\<pi> permutes B" for \<pi>
+ using permutes_bij_inv_into[OF that bij_inv] and assms
+ by (simp add: inv_into_inv_into_eq cong: if_cong)
+ moreover have "?g \<pi> x \<noteq> x" if "\<pi> permutes B" "\<And>x. x \<in> B \<Longrightarrow> \<pi> x \<noteq> x" "x \<in> A" for \<pi> x
+ using that and assms by (metis bij_betwE bij_betw_imp_surj_on f_inv_into_f permutes_imp_bij)
+ ultimately show ?case by auto
+ next
+ case 1
+ thus ?case using assms
+ by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left
+ dest: bij_betwE)
+ next
+ case 2
+ moreover have "bij_betw (inv_into A f) B A"
+ by (intro bij_betw_inv_into assms)
+ ultimately show ?case using assms
+ by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right
+ dest: bij_betwE)
+ qed
+qed
+
+
subsection \<open>The number of permutations on a finite set\<close>
lemma permutes_insert_lemma:
--- a/src/HOL/Transcendental.thy Tue Aug 22 14:34:26 2017 +0200
+++ b/src/HOL/Transcendental.thy Tue Aug 22 21:36:48 2017 +0200
@@ -1313,6 +1313,9 @@
for A :: "'a::real_normed_field set"
by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)
+lemmas continuous_on_pochhammer' [continuous_intros] =
+ continuous_on_compose2[OF continuous_on_pochhammer _ subset_UNIV]
+
subsection \<open>Exponential Function\<close>