# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1503430608 -7200
# Node ID ffaaa83543b2b753eceb25636d9853ac415ee00f
# Parent  ddb31006e3150fbbc4a11eb9893f06210c36d8da
Lemmas about analysis and permutations

diff -r ddb31006e315 -r ffaaa83543b2 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- 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)
diff -r ddb31006e315 -r ffaaa83543b2 src/HOL/Analysis/Conformal_Mappings.thy
--- 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)"
diff -r ddb31006e315 -r ffaaa83543b2 src/HOL/Analysis/Inner_Product.thy
--- 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
diff -r ddb31006e315 -r ffaaa83543b2 src/HOL/Analysis/Linear_Algebra.thy
--- 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>
 
diff -r ddb31006e315 -r ffaaa83543b2 src/HOL/Library/Permutations.thy
--- 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:
diff -r ddb31006e315 -r ffaaa83543b2 src/HOL/Transcendental.thy
--- 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>