# HG changeset patch
# User eberlm
# Date 1465824192 -7200
# Node ID 52792bb9126e34f84a487359aa22cc067c922e56
# Parent  a97a3a95be93797eba63bc8592188daa880a0f34
Facts about HK integration, complex powers, Gamma function

diff -r a97a3a95be93 -r 52792bb9126e src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Jun 13 08:33:29 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Jun 13 15:23:12 2016 +0200
@@ -1646,8 +1646,124 @@
 by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
 
 lemma norm_powr_real_powr:
-  "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
-  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
+  "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
+  by (cases "w = 0") (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 
+                                     complex_is_Real_iff in_Reals_norm complex_eq_iff)
+
+lemma tendsto_ln_complex [tendsto_intros]:
+  assumes "(f \<longlongrightarrow> a) F" "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  shows   "((\<lambda>z. ln (f z :: complex)) \<longlongrightarrow> ln a) F"
+  using tendsto_compose[OF continuous_at_Ln[of a, unfolded isCont_def] assms(1)] assms(2) by simp
+
+lemma tendsto_powr_complex:
+  fixes f g :: "_ \<Rightarrow> complex"
+  assumes a: "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F"
+  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
+proof -
+  from a have [simp]: "a \<noteq> 0" by auto
+  from f g a have "((\<lambda>z. exp (g z * ln (f z))) \<longlongrightarrow> a powr b) F" (is ?P)
+    by (auto intro!: tendsto_intros simp: powr_def)
+  also {
+    have "eventually (\<lambda>z. z \<noteq> 0) (nhds a)"
+      by (intro t1_space_nhds) simp_all
+    with f have "eventually (\<lambda>z. f z \<noteq> 0) F" using filterlim_iff by blast
+  }
+  hence "?P \<longleftrightarrow> ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
+    by (intro tendsto_cong refl) (simp_all add: powr_def mult_ac)
+  finally show ?thesis .
+qed
+
+lemma tendsto_powr_complex_0:
+  fixes f g :: "'a \<Rightarrow> complex"
+  assumes f: "(f \<longlongrightarrow> 0) F" and g: "(g \<longlongrightarrow> b) F" and b: "Re b > 0"
+  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> 0) F"
+proof (rule tendsto_norm_zero_cancel)
+  define h where
+    "h = (\<lambda>z. if f z = 0 then 0 else exp (Re (g z) * ln (cmod (f z)) + abs (Im (g z)) * pi))"
+  {
+    fix z :: 'a assume z: "f z \<noteq> 0"
+    define c where "c = abs (Im (g z)) * pi"
+    from mpi_less_Im_Ln[OF z] Im_Ln_le_pi[OF z]
+      have "abs (Im (Ln (f z))) \<le> pi" by simp
+    from mult_left_mono[OF this, of "abs (Im (g z))"]
+      have "abs (Im (g z) * Im (ln (f z))) \<le> c" by (simp add: abs_mult c_def)
+    hence "-Im (g z) * Im (ln (f z)) \<le> c" by simp
+    hence "norm (f z powr g z) \<le> h z" by (simp add: powr_def field_simps h_def c_def)
+  }
+  hence le: "norm (f z powr g z) \<le> h z" for z by (cases "f x = 0") (simp_all add: h_def)
+
+  have g': "(g \<longlongrightarrow> b) (inf F (principal {z. f z \<noteq> 0}))"
+    by (rule tendsto_mono[OF _ g]) simp_all
+  have "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) (inf F (principal {z. f z \<noteq> 0}))"
+    by (subst tendsto_norm_zero_iff, rule tendsto_mono[OF _ f]) simp_all
+  moreover {
+    have "filterlim (\<lambda>x. norm (f x)) (principal {0<..}) (principal {z. f z \<noteq> 0})"
+      by (auto simp: filterlim_def)
+    hence "filterlim (\<lambda>x. norm (f x)) (principal {0<..})
+             (inf F (principal {z. f z \<noteq> 0}))"
+      by (rule filterlim_mono) simp_all
+  }
+  ultimately have norm: "filterlim (\<lambda>x. norm (f x)) (at_right 0) (inf F (principal {z. f z \<noteq> 0}))"
+    by (simp add: filterlim_inf at_within_def)
+
+  have A: "LIM x inf F (principal {z. f z \<noteq> 0}). Re (g x) * -ln (cmod (f x)) :> at_top"
+    by (rule filterlim_tendsto_pos_mult_at_top tendsto_intros g' b
+          filterlim_compose[OF filterlim_uminus_at_top_at_bot] filterlim_compose[OF ln_at_0] norm)+
+  have B: "LIM x inf F (principal {z. f z \<noteq> 0}).
+          -\<bar>Im (g x)\<bar> * pi + -(Re (g x) * ln (cmod (f x))) :> at_top"
+    by (rule filterlim_tendsto_add_at_top tendsto_intros g')+ (insert A, simp_all)
+  have C: "(h \<longlongrightarrow> 0) F" unfolding h_def
+    by (intro filterlim_If tendsto_const filterlim_compose[OF exp_at_bot])
+       (insert B, auto simp: filterlim_uminus_at_bot algebra_simps)
+  show "((\<lambda>x. norm (f x powr g x)) \<longlongrightarrow> 0) F"
+    by (rule Lim_null_comparison[OF always_eventually C]) (insert le, auto)
+qed
+
+lemma tendsto_powr_complex' [tendsto_intros]:
+  fixes f g :: "_ \<Rightarrow> complex"
+  assumes fz: "a \<notin> \<real>\<^sub>\<le>\<^sub>0 \<or> (a = 0 \<and> Re b > 0)"
+  assumes fg: "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
+  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
+proof (cases "a = 0")
+  case True
+  with assms show ?thesis by (auto intro!: tendsto_powr_complex_0)
+next
+  case False
+  with assms show ?thesis by (auto intro!: tendsto_powr_complex elim!: nonpos_Reals_cases)
+qed
+
+lemma continuous_powr_complex:
+  assumes "f (netlimit F) \<notin> \<real>\<^sub>\<le>\<^sub>0" "continuous F f" "continuous F g"
+  shows   "continuous F (\<lambda>z. f z powr g z :: complex)"
+  using assms unfolding continuous_def by (intro tendsto_powr_complex) simp_all
+
+lemma isCont_powr_complex [continuous_intros]:
+  assumes "f z \<notin> \<real>\<^sub>\<le>\<^sub>0" "isCont f z" "isCont g z"
+  shows   "isCont (\<lambda>z. f z powr g z :: complex) z"
+  using assms unfolding isCont_def by (intro tendsto_powr_complex) simp_all
+
+lemma continuous_on_powr_complex [continuous_intros]:
+  assumes "A \<subseteq> {z. Re (f z) \<ge> 0 \<or> Im (f z) \<noteq> 0}"
+  assumes "\<And>z. z \<in> A \<Longrightarrow> f z = 0 \<Longrightarrow> Re (g z) > 0"
+  assumes "continuous_on A f" "continuous_on A g"
+  shows   "continuous_on A (\<lambda>z. f z powr g z)"
+  unfolding continuous_on_def
+proof
+  fix z assume z: "z \<in> A"
+  show "((\<lambda>z. f z powr g z) \<longlongrightarrow> f z powr g z) (at z within A)"
+  proof (cases "f z = 0")
+    case False
+    from assms(1,2) z have "Re (f z) \<ge> 0 \<or> Im (f z) \<noteq> 0" "f z = 0 \<longrightarrow> Re (g z) > 0" by auto
+    with assms(3,4) z show ?thesis
+      by (intro tendsto_powr_complex')
+         (auto elim!: nonpos_Reals_cases simp: complex_eq_iff continuous_on_def)
+  next
+    case True
+    with assms z show ?thesis
+      by (auto intro!: tendsto_powr_complex_0 simp: continuous_on_def)
+  qed
+qed
 
 
 subsection\<open>Some Limits involving Logarithms\<close>
diff -r a97a3a95be93 -r 52792bb9126e src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jun 13 08:33:29 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jun 13 15:23:12 2016 +0200
@@ -38,6 +38,27 @@
 lemma plus_one_in_nonpos_Ints_imp: "z + 1 \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0"
   using nonpos_Ints_diff_Nats[of "z+1" "1"] by simp_all
 
+lemma of_int_in_nonpos_Ints_iff:
+  "(of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> 0"
+  by (auto simp: nonpos_Ints_def)
+
+lemma one_plus_of_int_in_nonpos_Ints_iff:
+  "(1 + of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> -1"
+proof -
+  have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp
+  also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n + 1 \<le> 0" by (subst of_int_in_nonpos_Ints_iff) simp_all
+  also have "\<dots> \<longleftrightarrow> n \<le> -1" by presburger
+  finally show ?thesis .
+qed
+
+lemma one_minus_of_nat_in_nonpos_Ints_iff:
+  "(1 - of_nat n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0"
+proof -
+  have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp
+  also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger
+  finally show ?thesis .
+qed
+
 lemma fraction_not_in_ints:
   assumes "\<not>(n dvd m)" "n \<noteq> 0"
   shows   "of_int m / of_int n \<notin> (\<int> :: 'a :: {division_ring,ring_char_0} set)"
@@ -1046,17 +1067,19 @@
 
 lemma Gamma_1 [simp]: "Gamma 1 = 1" unfolding Gamma_def by simp
 
-lemma Gamma_fact: "Gamma (of_nat (Suc n)) = fact n"
-  by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff)
+lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
+  by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff 
+        of_nat_Suc [symmetric] del: of_nat_Suc)
 
 lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)"
-  by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc, subst Gamma_fact) (rule refl)
+  by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc, 
+      subst of_nat_Suc, subst Gamma_fact) (rule refl)
 
 lemma Gamma_of_int: "Gamma (of_int n) = (if n > 0 then fact (nat (n - 1)) else 0)"
 proof (cases "n > 0")
   case True
   hence "Gamma (of_int n) = Gamma (of_nat (Suc (nat (n - 1))))" by (subst of_nat_Suc) simp_all
-  with True show ?thesis by (subst (asm) Gamma_fact) simp
+  with True show ?thesis by (subst (asm) of_nat_Suc, subst (asm) Gamma_fact) simp
 qed (simp_all add: Gamma_eq_zero_iff nonpos_Ints_of_int)
 
 lemma rGamma_of_int: "rGamma (of_int n) = (if n > 0 then inverse (fact (nat (n - 1))) else 0)"
@@ -1656,6 +1679,15 @@
                (at x within A)" unfolding Beta_altdef
   by (rule DERIV_cong, (rule derivative_intros assms)+) (simp add: algebra_simps)
 
+lemma Beta_pole1: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Beta x y = 0"
+  by (auto simp add: Beta_def elim!: nonpos_Ints_cases')
+
+lemma Beta_pole2: "y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Beta x y = 0"
+  by (auto simp add: Beta_def elim!: nonpos_Ints_cases')
+  
+lemma Beta_zero: "x + y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Beta x y = 0"
+  by (auto simp add: Beta_def elim!: nonpos_Ints_cases')
+  
 lemma has_field_derivative_Beta2 [derivative_intros]:
   assumes "y \<notin> \<int>\<^sub>\<le>\<^sub>0" "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "((\<lambda>y. Beta x y) has_field_derivative (Beta x y * (Digamma y - Digamma (x + y))))
@@ -1676,7 +1708,7 @@
 qed
 
 lemma Beta_plus1_left:
-  assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
+  assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "(x + y) * Beta (x + 1) y = x * Beta x y"
 proof -
   have "(x + y) * Beta (x + 1) y = Gamma (x + 1) * Gamma y * ((x + y) * rGamma ((x + y) + 1))"
@@ -1687,12 +1719,12 @@
 qed
 
 lemma Beta_plus1_right:
-  assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
+  assumes "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "(x + y) * Beta x (y + 1) = y * Beta x y"
-  using Beta_plus1_left[of y x] assms by (simp add: Beta_commute add.commute)
+  using Beta_plus1_left[of y x] assms by (simp_all add: Beta_commute add.commute)
 
 lemma Gamma_Gamma_Beta:
-  assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0" "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0"
+  assumes "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "Gamma x * Gamma y = Beta x y * Gamma (x + y)"
   unfolding Beta_altdef using assms Gamma_eq_zero_iff[of "x+y"]
   by (simp add: rGamma_inverse_Gamma)
@@ -2459,7 +2491,7 @@
 
 subsubsection \<open>Binomial coefficient form\<close>
 
-lemma Gamma_binomial:
+lemma Gamma_gbinomial:
   "(\<lambda>n. ((z + of_nat n) gchoose n) * exp (-z * of_real (ln (of_nat n)))) \<longlonglongrightarrow> rGamma (z+1)"
 proof (cases "z = 0")
   case False
@@ -2484,14 +2516,25 @@
   qed
 qed (simp_all add: binomial_gbinomial [symmetric])
 
+lemma gbinomial_minus': "(a + of_nat b) gchoose b = (- 1) ^ b * (- (a + 1) gchoose b)"
+  by (subst gbinomial_minus) (simp add: power_mult_distrib [symmetric])
+
+lemma gbinomial_asymptotic:
+  fixes z :: "'a :: Gamma"
+  shows "(\<lambda>n. (z gchoose n) / ((-1)^n / exp ((z+1) * of_real (ln (real n))))) \<longlonglongrightarrow> 
+           inverse (Gamma (- z))"
+  unfolding rGamma_inverse_Gamma [symmetric] using Gamma_gbinomial[of "-z-1"] 
+  by (subst (asm) gbinomial_minus')
+     (simp add: add_ac mult_ac divide_inverse power_inverse [symmetric])
+
 lemma fact_binomial_limit:
   "(\<lambda>n. of_nat ((k + n) choose n) / of_nat (n ^ k) :: 'a :: Gamma) \<longlonglongrightarrow> 1 / fact k"
 proof (rule Lim_transform_eventually)
   have "(\<lambda>n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n))))
             \<longlonglongrightarrow> 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \<longlonglongrightarrow> _")
-    using Gamma_binomial[of "of_nat k :: 'a"]
+    using Gamma_gbinomial[of "of_nat k :: 'a"]
     by (simp add: binomial_gbinomial add_ac Gamma_def divide_simps exp_of_real [symmetric] exp_minus)
-  also have "Gamma (of_nat (Suc k)) = fact k" by (rule Gamma_fact)
+  also have "Gamma (of_nat (Suc k)) = fact k" by (simp add: Gamma_fact)
   finally show "?f \<longlonglongrightarrow> 1 / fact k" .
 
   show "eventually (\<lambda>n. ?f n = of_nat ((k + n) choose n) / of_nat (n ^ k)) sequentially"
@@ -2504,10 +2547,62 @@
   qed
 qed
 
-lemma binomial_asymptotic:
+lemma binomial_asymptotic':
   "(\<lambda>n. of_nat ((k + n) choose n) / (of_nat (n ^ k) / fact k) :: 'a :: Gamma) \<longlonglongrightarrow> 1"
   using tendsto_mult[OF fact_binomial_limit[of k] tendsto_const[of "fact k :: 'a"]] by simp
 
+lemma gbinomial_Beta:
+  assumes "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0"
+  shows   "((z::'a::Gamma) gchoose n) = inverse ((z + 1) * Beta (z - of_nat n + 1) (of_nat n + 1))"
+using assms
+proof (induction n arbitrary: z)
+  case 0
+  hence "z + 2 \<notin> \<int>\<^sub>\<le>\<^sub>0"
+    using plus_one_in_nonpos_Ints_imp[of "z+1"] by (auto simp: add.commute)
+  with 0 show ?case
+    by (auto simp: Beta_def Gamma_eq_zero_iff Gamma_plus1 [symmetric] add.commute)
+next
+  case (Suc n z)
+  show ?case
+  proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
+    case True
+    with Suc.prems have "z = 0"
+      by (auto elim!: nonpos_Ints_cases simp: algebra_simps one_plus_of_int_in_nonpos_Ints_iff)
+    show ?thesis
+    proof (cases "n = 0")
+      case True
+      with \<open>z = 0\<close> show ?thesis
+        by (simp add: Beta_def Gamma_eq_zero_iff Gamma_plus1 [symmetric])
+    next
+      case False
+      with \<open>z = 0\<close> show ?thesis
+        by (simp_all add: Beta_pole1 one_minus_of_nat_in_nonpos_Ints_iff gbinomial_1)
+    qed
+  next
+    case False
+    have "(z gchoose (Suc n)) = ((z - 1 + 1) gchoose (Suc n))" by simp
+    also have "\<dots> = (z - 1 gchoose n) * ((z - 1) + 1) / of_nat (Suc n)"
+      by (subst gbinomial_factors) (simp add: field_simps)
+    also from False have "\<dots> = inverse (of_nat (Suc n) * Beta (z - of_nat n) (of_nat (Suc n)))" 
+      (is "_ = inverse ?x") by (subst Suc.IH) (simp_all add: field_simps Beta_pole1)
+    also have "of_nat (Suc n) \<notin> (\<int>\<^sub>\<le>\<^sub>0 :: 'a set)" by (subst of_nat_in_nonpos_Ints_iff) simp_all
+    hence "?x = (z + 1) * Beta (z - of_nat (Suc n) + 1) (of_nat (Suc n) + 1)"
+      by (subst Beta_plus1_right [symmetric]) simp_all
+    finally show ?thesis .
+  qed
+qed
+
+lemma gbinomial_Gamma:
+  assumes "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0"
+  shows   "(z gchoose n) = Gamma (z + 1) / (fact n * Gamma (z - of_nat n + 1))"
+proof -
+  have "(z gchoose n) = Gamma (z + 2) / (z + 1) / (fact n * Gamma (z - of_nat n + 1))"
+    by (subst gbinomial_Beta[OF assms]) (simp_all add: Beta_def Gamma_fact [symmetric] add_ac)
+  also from assms have "Gamma (z + 2) / (z + 1) = Gamma (z + 1)"
+    using Gamma_plus1[of "z+1"] by (auto simp add: divide_simps mult_ac add_ac)
+  finally show ?thesis .
+qed
+
 
 subsection \<open>The Weierstraß product formula for the sine\<close>
 
@@ -2650,5 +2745,4 @@
     by (auto simp add: sums_iff power_divide inverse_eq_divide)
 qed
 
-
 end
diff -r a97a3a95be93 -r 52792bb9126e src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 13 08:33:29 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 13 15:23:12 2016 +0200
@@ -2820,6 +2820,72 @@
   shows "blinfun_apply (integral s f) x = integral s (\<lambda>y. blinfun_apply (f y) x)"
   by (metis (no_types, lifting) assms blinfun.prod_left.rep_eq integral_blinfun_apply integral_cong)
 
+lemma has_integral_componentwise_iff:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  shows "(f has_integral y) A \<longleftrightarrow> (\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
+proof safe
+  fix b :: 'b assume "(f has_integral y) A"
+  from has_integral_linear[OF this(1) bounded_linear_component, of b]
+    show "((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A" by (simp add: o_def)
+next
+  assume "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
+  hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral ((y \<bullet> b) *\<^sub>R b)) A"
+    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
+  hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. (y \<bullet> b) *\<^sub>R b)) A"
+    by (intro has_integral_setsum) (simp_all add: o_def)
+  thus "(f has_integral y) A" by (simp add: euclidean_representation)
+qed
+
+lemma has_integral_componentwise:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  shows "(\<And>b. b \<in> Basis \<Longrightarrow> ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A) \<Longrightarrow> (f has_integral y) A"
+  by (subst has_integral_componentwise_iff) blast
+
+lemma integrable_componentwise_iff:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  shows "f integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)"
+proof
+  assume "f integrable_on A"
+  then obtain y where "(f has_integral y) A" by (auto simp: integrable_on_def)
+  hence "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
+    by (subst (asm) has_integral_componentwise_iff)
+  thus "(\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)" by (auto simp: integrable_on_def)
+next
+  assume "(\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)"
+  then obtain y where "\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral y b) A"
+    unfolding integrable_on_def by (subst (asm) bchoice_iff) blast
+  hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral (y b *\<^sub>R b)) A"
+    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
+  hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. y b *\<^sub>R b)) A"
+    by (intro has_integral_setsum) (simp_all add: o_def)
+  thus "f integrable_on A" by (auto simp: integrable_on_def o_def euclidean_representation)
+qed
+
+lemma integrable_componentwise:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  shows "(\<And>b. b \<in> Basis \<Longrightarrow> (\<lambda>x. f x \<bullet> b) integrable_on A) \<Longrightarrow> f integrable_on A"
+  by (subst integrable_componentwise_iff) blast
+
+lemma integral_componentwise:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  assumes "f integrable_on A"
+  shows "integral A f = (\<Sum>b\<in>Basis. integral A (\<lambda>x. (f x \<bullet> b) *\<^sub>R b))"
+proof -
+  from assms have integrable: "\<forall>b\<in>Basis. (\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. (f x \<bullet> b)) integrable_on A"
+    by (subst (asm) integrable_componentwise_iff, intro integrable_linear ballI)
+       (simp_all add: bounded_linear_scaleR_left)
+  have "integral A f = integral A (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b)"
+    by (simp add: euclidean_representation)
+  also from integrable have "\<dots> = (\<Sum>a\<in>Basis. integral A (\<lambda>x. (f x \<bullet> a) *\<^sub>R a))"
+    by (subst integral_setsum) (simp_all add: o_def)
+  finally show ?thesis .
+qed
+
+lemma integrable_component:
+  "f integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (y :: 'b :: euclidean_space)) integrable_on A"
+  by (drule integrable_linear[OF _ bounded_linear_component[of y]]) (simp add: o_def)
+
+
 
 subsection \<open>Cauchy-type criterion for integrability.\<close>
 
@@ -11943,16 +12009,16 @@
 
 subsection \<open>Dominated convergence\<close>
 
-(* GENERALIZE the following theorems *)
-
-lemma dominated_convergence:
+context
+begin
+
+private lemma dominated_convergence_real:
   fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
   assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
     and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
     and "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
-  shows "g integrable_on s"
-    and "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-proof -
+  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+proof
   have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
   proof (safe intro!: bdd_belowI)
     fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
@@ -12223,8 +12289,53 @@
   qed
 qed
 
+lemma dominated_convergence:
+  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
+    and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
+    and conv: "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+  shows "g integrable_on s"
+    and "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+proof -
+  {
+    fix b :: 'm assume b: "b \<in> Basis"
+    have A: "(\<lambda>x. g x \<bullet> b) integrable_on s \<and>
+               (\<lambda>k. integral s (\<lambda>x. f k x \<bullet> b)) \<longlonglongrightarrow> integral s (\<lambda>x. g x \<bullet> b)"
+    proof (rule dominated_convergence_real)
+      fix k :: nat
+      from f show "(\<lambda>x. f k x \<bullet> b) integrable_on s" by (rule integrable_component)
+    next
+      from h show "h integrable_on s" .
+    next
+      fix k :: nat
+      show "\<forall>x\<in>s. norm (f k x \<bullet> b) \<le> h x"
+      proof
+        fix x assume x: "x \<in> s"
+        have "norm (f k x \<bullet> b) \<le> norm (f k x)" by (simp add: Basis_le_norm b)
+        also have "\<dots> \<le> h x" using le[of k] x by simp
+        finally show "norm (f k x \<bullet> b) \<le> h x" .
+      qed
+    next
+      from conv show "\<forall>x\<in>s. (\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
+        by (auto intro!: tendsto_inner)
+    qed
+    have B: "integral s ((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f k x \<bullet> b)) = integral s (\<lambda>x. f k x \<bullet> b) *\<^sub>R b"
+      for k by (rule integral_linear)
+               (simp_all add: f integrable_component bounded_linear_scaleR_left)
+    have C: "integral s ((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. g x \<bullet> b)) = integral s (\<lambda>x. g x \<bullet> b) *\<^sub>R b"
+      using A by (intro integral_linear)
+                 (simp_all add: integrable_component bounded_linear_scaleR_left)
+    note A B C
+  } note A = this
+
+  show "g integrable_on s" by (rule integrable_componentwise) (insert A, blast)
+  with A f show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+    by (subst (1 2) integral_componentwise)
+       (auto intro!: tendsto_setsum tendsto_scaleR simp: o_def)
+qed
+
 lemma has_integral_dominated_convergence:
-  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
+  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
     "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
     and x: "y \<longlonglongrightarrow> x"
@@ -12245,7 +12356,84 @@
     by simp
 qed
 
-subsection\<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
+end
+
+
+subsection \<open>Integration by parts\<close>
+
+lemma integration_by_parts_interior_strong:
+  assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
+  assumes s: "finite s" and le: "a \<le> b"
+  assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
+  assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
+                 "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
+  assumes int: "((\<lambda>x. prod (f x) (g' x)) has_integral 
+                  (prod (f b) (g b) - prod (f a) (g a) - y)) {a..b}"
+  shows   "((\<lambda>x. prod (f' x) (g x)) has_integral y) {a..b}"
+proof -
+  interpret bounded_bilinear prod by fact
+  have "((\<lambda>x. prod (f x) (g' x) + prod (f' x) (g x)) has_integral
+          (prod (f b) (g b) - prod (f a) (g a))) {a..b}"
+    using deriv by (intro fundamental_theorem_of_calculus_interior_strong[OF s le])
+                   (auto intro!: continuous_intros continuous_on has_vector_derivative)
+  from has_integral_sub[OF this int] show ?thesis by (simp add: algebra_simps)
+qed
+
+lemma integration_by_parts_interior:
+  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+          "continuous_on {a..b} f" "continuous_on {a..b} g"
+  assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
+          "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
+  assumes "((\<lambda>x. prod (f x) (g' x)) has_integral (prod (f b) (g b) - prod (f a) (g a) - y)) {a..b}"
+  shows   "((\<lambda>x. prod (f' x) (g x)) has_integral y) {a..b}"
+  by (rule integration_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
+
+lemma integration_by_parts:
+  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+          "continuous_on {a..b} f" "continuous_on {a..b} g"
+  assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
+          "\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
+  assumes "((\<lambda>x. prod (f x) (g' x)) has_integral (prod (f b) (g b) - prod (f a) (g a) - y)) {a..b}"
+  shows   "((\<lambda>x. prod (f' x) (g x)) has_integral y) {a..b}"
+  by (rule integration_by_parts_interior[of _ _ _ f g f' g']) (insert assms, simp_all)
+
+lemma integrable_by_parts_interior_strong:
+  assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
+  assumes s: "finite s" and le: "a \<le> b"
+  assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
+  assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
+                 "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
+  assumes int: "(\<lambda>x. prod (f x) (g' x)) integrable_on {a..b}"
+  shows   "(\<lambda>x. prod (f' x) (g x)) integrable_on {a..b}"
+proof -
+  from int obtain I where "((\<lambda>x. prod (f x) (g' x)) has_integral I) {a..b}"
+    unfolding integrable_on_def by blast
+  hence "((\<lambda>x. prod (f x) (g' x)) has_integral (prod (f b) (g b) - prod (f a) (g a) -
+           (prod (f b) (g b) - prod (f a) (g a) - I))) {a..b}" by simp
+  from integration_by_parts_interior_strong[OF assms(1-7) this]
+    show ?thesis unfolding integrable_on_def by blast
+qed
+
+lemma integrable_by_parts_interior:
+  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+          "continuous_on {a..b} f" "continuous_on {a..b} g"
+  assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
+          "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
+  assumes "(\<lambda>x. prod (f x) (g' x)) integrable_on {a..b}"
+  shows   "(\<lambda>x. prod (f' x) (g x)) integrable_on {a..b}"
+  by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
+
+lemma integrable_by_parts:
+  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+          "continuous_on {a..b} f" "continuous_on {a..b} g"
+  assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
+          "\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
+  assumes "(\<lambda>x. prod (f x) (g' x)) integrable_on {a..b}"
+  shows   "(\<lambda>x. prod (f' x) (g x)) integrable_on {a..b}"
+  by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
+
+
+subsection \<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
 
 lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
   by auto
diff -r a97a3a95be93 -r 52792bb9126e src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Jun 13 08:33:29 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Jun 13 15:23:12 2016 +0200
@@ -429,6 +429,10 @@
   "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
   by (subst eventually_nhds) blast
 
+lemma eventually_nhds_x_imp_x:
+  "eventually P (nhds x) \<Longrightarrow> P x"
+  by (subst (asm) eventually_nhds) blast
+
 lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   unfolding trivial_limit_def eventually_nhds by simp
 
@@ -501,6 +505,34 @@
     unfolding nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def ..
 qed
 
+lemma filterlim_at_within_If:
+  assumes "filterlim f G (at x within (A \<inter> {x. P x}))"
+  assumes "filterlim g G (at x within (A \<inter> {x. \<not>P x}))"
+  shows   "filterlim (\<lambda>x. if P x then f x else g x) G (at x within A)"
+proof (rule filterlim_If)
+  note assms(1)
+  also have "at x within (A \<inter> {x. P x}) = inf (nhds x) (principal (A \<inter> Collect P - {x}))"
+    by (simp add: at_within_def)
+  also have "A \<inter> Collect P - {x} = (A - {x}) \<inter> Collect P" by blast
+  also have "inf (nhds x) (principal \<dots>) = inf (at x within A) (principal (Collect P))"
+    by (simp add: at_within_def inf_assoc)
+  finally show "filterlim f G (inf (at x within A) (principal (Collect P)))" .
+next
+  note assms(2)
+  also have "at x within (A \<inter> {x. \<not>P x}) = inf (nhds x) (principal (A \<inter> {x. \<not>P x} - {x}))"
+    by (simp add: at_within_def)
+  also have "A \<inter> {x. \<not>P x} - {x} = (A - {x}) \<inter> {x. \<not>P x}" by blast
+  also have "inf (nhds x) (principal \<dots>) = inf (at x within A) (principal {x. \<not>P x})"
+    by (simp add: at_within_def inf_assoc)
+  finally show "filterlim g G (inf (at x within A) (principal {x. \<not>P x}))" .
+qed
+
+lemma filterlim_at_If:
+  assumes "filterlim f G (at x within {x. P x})"
+  assumes "filterlim g G (at x within {x. \<not>P x})"
+  shows   "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
+  using assms by (intro filterlim_at_within_If) simp_all
+
 lemma (in linorder_topology) at_within_order: "UNIV \<noteq> {x} \<Longrightarrow>
   at x within s = inf (INF a:{x <..}. principal ({..< a} \<inter> s - {x}))
                       (INF a:{..< x}. principal ({a <..} \<inter> s - {x}))"
@@ -1695,6 +1727,18 @@
 lemma isCont_def: "isCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow> f a"
   by (rule continuous_at)
 
+lemma isCont_cong:
+  assumes "eventually (\<lambda>x. f x = g x) (nhds x)"
+  shows   "isCont f x \<longleftrightarrow> isCont g x"
+proof -
+  from assms have [simp]: "f x = g x" by (rule eventually_nhds_x_imp_x)
+  from assms have "eventually (\<lambda>x. f x = g x) (at x)"
+    by (auto simp: eventually_at_filter elim!: eventually_mono)
+  with assms have "isCont f x \<longleftrightarrow> isCont g x" unfolding isCont_def
+    by (intro filterlim_cong) (auto elim!: eventually_mono)
+  with assms show ?thesis by simp
+qed
+
 lemma continuous_at_imp_continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
   by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
 
diff -r a97a3a95be93 -r 52792bb9126e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Jun 13 08:33:29 2016 +0200
+++ b/src/HOL/Transcendental.thy	Mon Jun 13 15:23:12 2016 +0200
@@ -2059,6 +2059,34 @@
   qed
 qed
 
+lemma ln_x_over_x_tendsto_0:
+  "((\<lambda>x::real. ln x / x) \<longlongrightarrow> 0) at_top"
+proof (rule lhospital_at_top_at_top[where f' = inverse and g' = "\<lambda>_. 1"])
+  from eventually_gt_at_top[of "0::real"]
+    show "\<forall>\<^sub>F x in at_top. (ln has_real_derivative inverse x) (at x)"
+     by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)
+qed (insert tendsto_inverse_0,
+     auto simp: filterlim_ident dest!: tendsto_mono[OF at_top_le_at_infinity])
+
+lemma exp_ge_one_plus_x_over_n_power_n:
+  assumes "x \<ge> - real n" "n > 0"
+  shows   "(1 + x / of_nat n) ^ n \<le> exp x"
+proof (cases "x = -of_nat n")
+  case False
+  from assms False have "(1 + x / of_nat n) ^ n = exp (of_nat n * ln (1 + x / of_nat n))"
+    by (subst exp_of_nat_mult, subst exp_ln) (simp_all add: field_simps)
+  also from assms False have "ln (1 + x / real n) \<le> x / real n"
+    by (intro ln_add_one_self_le_self2) (simp_all add: field_simps)
+  with assms have "exp (of_nat n * ln (1 + x / of_nat n)) \<le> exp x"
+    by (simp add: field_simps)
+  finally show ?thesis .
+qed (simp_all add: zero_power)
+
+lemma exp_ge_one_minus_x_over_n_power_n:
+  assumes "x \<le> real n" "n > 0"
+  shows   "(1 - x / of_nat n) ^ n \<le> exp (-x)"
+  using exp_ge_one_plus_x_over_n_power_n[of n "-x"] assms by simp
+
 lemma exp_at_bot: "(exp \<longlongrightarrow> (0::real)) at_bot"
   unfolding tendsto_Zfun_iff
 proof (rule ZfunI, simp add: eventually_at_bot_dense)
@@ -2564,7 +2592,7 @@
   finally show ?thesis .
 qed
 
-lemma tendsto_powr [tendsto_intros]:
+lemma tendsto_powr:
   fixes a::real
   assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F" and a: "a \<noteq> 0"
   shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
@@ -2574,6 +2602,38 @@
     by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
 qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
 
+lemma tendsto_powr'[tendsto_intros]:
+  fixes a::real
+  assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F" 
+      and a: "a \<noteq> 0 \<or> (b > 0 \<and> eventually (\<lambda>x. f x \<ge> 0) F)"
+  shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
+proof -
+  from a consider "a \<noteq> 0" | "a = 0" "b > 0" "eventually (\<lambda>x. f x \<ge> 0) F" by auto
+  thus ?thesis
+  proof cases
+    assume "a \<noteq> 0"
+    from f g this show ?thesis by (rule tendsto_powr)
+  next
+    assume a: "a = 0" and b: "b > 0" and f_nonneg: "eventually (\<lambda>x. f x \<ge> 0) F"
+    hence "((\<lambda>x. if f x = 0 then 0 else exp (g x * ln (f x))) \<longlongrightarrow> 0) F"
+    proof (intro filterlim_If)
+      have "filterlim f (principal {0<..}) (inf F (principal {z. f z \<noteq> 0}))"
+        using f_nonneg by (auto simp add: filterlim_iff eventually_inf_principal 
+                             eventually_principal elim: eventually_mono)
+      moreover have "filterlim f (nhds a) (inf F (principal {z. f z \<noteq> 0}))"
+        by (rule tendsto_mono[OF _ f]) simp_all
+      ultimately have f: "filterlim f (at_right 0) (inf F (principal {x. f x \<noteq> 0}))"
+        by (simp add: at_within_def filterlim_inf a)
+      have g: "(g \<longlongrightarrow> b) (inf F (principal {z. f z \<noteq> 0}))"
+        by (rule tendsto_mono[OF _ g]) simp_all
+      show "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> 0) (inf F (principal {x. f x \<noteq> 0}))"
+        by (rule filterlim_compose[OF exp_at_bot] filterlim_tendsto_pos_mult_at_bot
+                 filterlim_compose[OF ln_at_0] f g b)+
+    qed simp_all
+    with a show ?thesis by (simp add: powr_def)
+  qed
+qed
+
 lemma continuous_powr:
   assumes "continuous F f"
     and "continuous F g"
@@ -2597,27 +2657,12 @@
   assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> (0::real)"
   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
-
+  
 lemma tendsto_powr2:
   fixes a::real
   assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F" and f_nonneg: "\<forall>\<^sub>F x in F. 0 \<le> f x" and b: "0 < b"
   shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
-  unfolding powr_def
-proof (rule filterlim_If)
-  from f show "((\<lambda>x. 0) \<longlongrightarrow> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
-    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
-next
-  { assume "a = 0"
-    with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0"
-      by (auto simp add: filterlim_at eventually_inf_principal le_less
-               elim: eventually_mono intro: tendsto_mono inf_le1)
-    then have "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> 0) (inf F (principal {x. f x \<noteq> 0}))"
-      by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
-                       filterlim_tendsto_pos_mult_at_bot[OF _ \<open>0 < b\<close>]
-               intro: tendsto_mono inf_le1 g) }
-  then show "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \<noteq> 0}))"
-    using f g by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
-qed
+  using tendsto_powr'[of f a F g b] assms by auto
 
 lemma DERIV_powr:
   fixes r::real
@@ -2661,6 +2706,27 @@
   shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> 0) F"
   using tendsto_powr2[OF assms] by simp
 
+lemma continuous_on_powr':
+  assumes "continuous_on s f" "continuous_on s g" and
+    "\<forall>x\<in>s. f x \<ge> (0::real) \<and> (f x = 0 \<longrightarrow> g x > 0)"
+  shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
+  unfolding continuous_on_def
+proof
+  fix x assume x: "x \<in> s"
+  from assms x show "((\<lambda>x. f x powr g x) \<longlongrightarrow> f x powr g x) (at x within s)"
+  proof (cases "f x = 0")
+    case True
+    from assms(3) have "eventually (\<lambda>x. f x \<ge> 0) (at x within s)"
+      by (auto simp: at_within_def eventually_inf_principal)
+    with True x assms show ?thesis
+      by (auto intro!: tendsto_zero_powrI[of f _ g "g x"] simp: continuous_on_def)
+  next
+    case False
+    with assms x show ?thesis
+      by (auto intro!: tendsto_powr' simp: continuous_on_def)
+  qed
+qed
+
 lemma tendsto_neg_powr:
   assumes "s < 0"
     and f: "LIM x F. f x :> at_top"