--- 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>
--- 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
--- 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
--- 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)
--- 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"