# 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 \ \ \ 0 < Re w \ 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 \ \ \ 0 \ Re w \ 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 \ a) F" "a \ \\<^sub>\\<^sub>0" + shows "((\z. ln (f z :: complex)) \ 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 :: "_ \ complex" + assumes a: "a \ \\<^sub>\\<^sub>0" + assumes f: "(f \ a) F" and g: "(g \ b) F" + shows "((\z. f z powr g z) \ a powr b) F" +proof - + from a have [simp]: "a \ 0" by auto + from f g a have "((\z. exp (g z * ln (f z))) \ a powr b) F" (is ?P) + by (auto intro!: tendsto_intros simp: powr_def) + also { + have "eventually (\z. z \ 0) (nhds a)" + by (intro t1_space_nhds) simp_all + with f have "eventually (\z. f z \ 0) F" using filterlim_iff by blast + } + hence "?P \ ((\z. f z powr g z) \ 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 \ complex" + assumes f: "(f \ 0) F" and g: "(g \ b) F" and b: "Re b > 0" + shows "((\z. f z powr g z) \ 0) F" +proof (rule tendsto_norm_zero_cancel) + define h where + "h = (\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 \ 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))) \ pi" by simp + from mult_left_mono[OF this, of "abs (Im (g z))"] + have "abs (Im (g z) * Im (ln (f z))) \ c" by (simp add: abs_mult c_def) + hence "-Im (g z) * Im (ln (f z)) \ c" by simp + hence "norm (f z powr g z) \ h z" by (simp add: powr_def field_simps h_def c_def) + } + hence le: "norm (f z powr g z) \ h z" for z by (cases "f x = 0") (simp_all add: h_def) + + have g': "(g \ b) (inf F (principal {z. f z \ 0}))" + by (rule tendsto_mono[OF _ g]) simp_all + have "((\x. norm (f x)) \ 0) (inf F (principal {z. f z \ 0}))" + by (subst tendsto_norm_zero_iff, rule tendsto_mono[OF _ f]) simp_all + moreover { + have "filterlim (\x. norm (f x)) (principal {0<..}) (principal {z. f z \ 0})" + by (auto simp: filterlim_def) + hence "filterlim (\x. norm (f x)) (principal {0<..}) + (inf F (principal {z. f z \ 0}))" + by (rule filterlim_mono) simp_all + } + ultimately have norm: "filterlim (\x. norm (f x)) (at_right 0) (inf F (principal {z. f z \ 0}))" + by (simp add: filterlim_inf at_within_def) + + have A: "LIM x inf F (principal {z. f z \ 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 \ 0}). + -\Im (g x)\ * 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 \ 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 "((\x. norm (f x powr g x)) \ 0) F" + by (rule Lim_null_comparison[OF always_eventually C]) (insert le, auto) +qed + +lemma tendsto_powr_complex' [tendsto_intros]: + fixes f g :: "_ \ complex" + assumes fz: "a \ \\<^sub>\\<^sub>0 \ (a = 0 \ Re b > 0)" + assumes fg: "(f \ a) F" "(g \ b) F" + shows "((\z. f z powr g z) \ 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) \ \\<^sub>\\<^sub>0" "continuous F f" "continuous F g" + shows "continuous F (\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 \ \\<^sub>\\<^sub>0" "isCont f z" "isCont g z" + shows "isCont (\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 \ {z. Re (f z) \ 0 \ Im (f z) \ 0}" + assumes "\z. z \ A \ f z = 0 \ Re (g z) > 0" + assumes "continuous_on A f" "continuous_on A g" + shows "continuous_on A (\z. f z powr g z)" + unfolding continuous_on_def +proof + fix z assume z: "z \ A" + show "((\z. f z powr g z) \ 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) \ 0 \ Im (f z) \ 0" "f z = 0 \ 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\Some Limits involving Logarithms\ 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 \ \\<^sub>\\<^sub>0 \ z \ \\<^sub>\\<^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) \ \\<^sub>\\<^sub>0 \ n \ 0" + by (auto simp: nonpos_Ints_def) + +lemma one_plus_of_int_in_nonpos_Ints_iff: + "(1 + of_int n :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0 \ n \ -1" +proof - + have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp + also have "\ \ \\<^sub>\\<^sub>0 \ n + 1 \ 0" by (subst of_int_in_nonpos_Ints_iff) simp_all + also have "\ \ n \ -1" by presburger + finally show ?thesis . +qed + +lemma one_minus_of_nat_in_nonpos_Ints_iff: + "(1 - of_nat n :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0 \ n > 0" +proof - + have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp + also have "\ \ \\<^sub>\\<^sub>0 \ n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger + finally show ?thesis . +qed + lemma fraction_not_in_ints: assumes "\(n dvd m)" "n \ 0" shows "of_int m / of_int n \ (\ :: '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 \ \\<^sub>\\<^sub>0 \ Beta x y = 0" + by (auto simp add: Beta_def elim!: nonpos_Ints_cases') + +lemma Beta_pole2: "y \ \\<^sub>\\<^sub>0 \ Beta x y = 0" + by (auto simp add: Beta_def elim!: nonpos_Ints_cases') + +lemma Beta_zero: "x + y \ \\<^sub>\\<^sub>0 \ Beta x y = 0" + by (auto simp add: Beta_def elim!: nonpos_Ints_cases') + lemma has_field_derivative_Beta2 [derivative_intros]: assumes "y \ \\<^sub>\\<^sub>0" "x + y \ \\<^sub>\\<^sub>0" shows "((\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 \ \\<^sub>\\<^sub>0" "y \ \\<^sub>\\<^sub>0" + assumes "x \ \\<^sub>\\<^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 \ \\<^sub>\\<^sub>0" "y \ \\<^sub>\\<^sub>0" + assumes "y \ \\<^sub>\\<^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 \ \\<^sub>\\<^sub>0" "y \ \\<^sub>\\<^sub>0" "x + y \ \\<^sub>\\<^sub>0" + assumes "x + y \ \\<^sub>\\<^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 \Binomial coefficient form\ -lemma Gamma_binomial: +lemma Gamma_gbinomial: "(\n. ((z + of_nat n) gchoose n) * exp (-z * of_real (ln (of_nat n)))) \ 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 "(\n. (z gchoose n) / ((-1)^n / exp ((z+1) * of_real (ln (real n))))) \ + 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: "(\n. of_nat ((k + n) choose n) / of_nat (n ^ k) :: 'a :: Gamma) \ 1 / fact k" proof (rule Lim_transform_eventually) have "(\n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n)))) \ 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \ _") - 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 \ 1 / fact k" . show "eventually (\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': "(\n. of_nat ((k + n) choose n) / (of_nat (n ^ k) / fact k) :: 'a :: Gamma) \ 1" using tendsto_mult[OF fact_binomial_limit[of k] tendsto_const[of "fact k :: 'a"]] by simp +lemma gbinomial_Beta: + assumes "z + 1 \ \\<^sub>\\<^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 \ \\<^sub>\\<^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 \ \\<^sub>\\<^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 \z = 0\ show ?thesis + by (simp add: Beta_def Gamma_eq_zero_iff Gamma_plus1 [symmetric]) + next + case False + with \z = 0\ 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 "\ = (z - 1 gchoose n) * ((z - 1) + 1) / of_nat (Suc n)" + by (subst gbinomial_factors) (simp add: field_simps) + also from False have "\ = 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) \ (\\<^sub>\\<^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 \ \\<^sub>\\<^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 \The Weierstraß product formula for the sine\ @@ -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 (\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 \ 'b :: euclidean_space" + shows "(f has_integral y) A \ (\b\Basis. ((\x. f x \ b) has_integral (y \ 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 "((\x. f x \ b) has_integral (y \ b)) A" by (simp add: o_def) +next + assume "(\b\Basis. ((\x. f x \ b) has_integral (y \ b)) A)" + hence "\b\Basis. (((\x. x *\<^sub>R b) \ (\x. f x \ b)) has_integral ((y \ b) *\<^sub>R b)) A" + by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left) + hence "((\x. \b\Basis. (f x \ b) *\<^sub>R b) has_integral (\b\Basis. (y \ 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 \ 'b :: euclidean_space" + shows "(\b. b \ Basis \ ((\x. f x \ b) has_integral (y \ b)) A) \ (f has_integral y) A" + by (subst has_integral_componentwise_iff) blast + +lemma integrable_componentwise_iff: + fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" + shows "f integrable_on A \ (\b\Basis. (\x. f x \ 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 "(\b\Basis. ((\x. f x \ b) has_integral (y \ b)) A)" + by (subst (asm) has_integral_componentwise_iff) + thus "(\b\Basis. (\x. f x \ b) integrable_on A)" by (auto simp: integrable_on_def) +next + assume "(\b\Basis. (\x. f x \ b) integrable_on A)" + then obtain y where "\b\Basis. ((\x. f x \ b) has_integral y b) A" + unfolding integrable_on_def by (subst (asm) bchoice_iff) blast + hence "\b\Basis. (((\x. x *\<^sub>R b) \ (\x. f x \ b)) has_integral (y b *\<^sub>R b)) A" + by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left) + hence "((\x. \b\Basis. (f x \ b) *\<^sub>R b) has_integral (\b\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 \ 'b :: euclidean_space" + shows "(\b. b \ Basis \ (\x. f x \ b) integrable_on A) \ f integrable_on A" + by (subst integrable_componentwise_iff) blast + +lemma integral_componentwise: + fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" + assumes "f integrable_on A" + shows "integral A f = (\b\Basis. integral A (\x. (f x \ b) *\<^sub>R b))" +proof - + from assms have integrable: "\b\Basis. (\x. x *\<^sub>R b) \ (\x. (f x \ 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 (\x. \b\Basis. (f x \ b) *\<^sub>R b)" + by (simp add: euclidean_representation) + also from integrable have "\ = (\a\Basis. integral A (\x. (f x \ a) *\<^sub>R a))" + by (subst integral_setsum) (simp_all add: o_def) + finally show ?thesis . +qed + +lemma integrable_component: + "f integrable_on A \ (\x. f x \ (y :: 'b :: euclidean_space)) integrable_on A" + by (drule integrable_linear[OF _ bounded_linear_component[of y]]) (simp add: o_def) + + subsection \Cauchy-type criterion for integrability.\ @@ -11943,16 +12009,16 @@ subsection \Dominated convergence\ -(* GENERALIZE the following theorems *) - -lemma dominated_convergence: +context +begin + +private lemma dominated_convergence_real: fixes f :: "nat \ 'n::euclidean_space \ real" assumes "\k. (f k) integrable_on s" "h integrable_on s" and "\k. \x \ s. norm (f k x) \ h x" and "\x \ s. ((\k. f k x) \ g x) sequentially" - shows "g integrable_on s" - and "((\k. integral s (f k)) \ integral s g) sequentially" -proof - + shows "g integrable_on s \ ((\k. integral s (f k)) \ integral s g) sequentially" +proof have bdd_below[simp]: "\x P. x \ s \ bdd_below {f n x |n. P n}" proof (safe intro!: bdd_belowI) fix n x show "x \ s \ - h x \ f n x" @@ -12223,8 +12289,53 @@ qed qed +lemma dominated_convergence: + fixes f :: "nat \ 'n::euclidean_space \ 'm::euclidean_space" + assumes f: "\k. (f k) integrable_on s" and h: "h integrable_on s" + and le: "\k. \x \ s. norm (f k x) \ h x" + and conv: "\x \ s. ((\k. f k x) \ g x) sequentially" + shows "g integrable_on s" + and "((\k. integral s (f k)) \ integral s g) sequentially" +proof - + { + fix b :: 'm assume b: "b \ Basis" + have A: "(\x. g x \ b) integrable_on s \ + (\k. integral s (\x. f k x \ b)) \ integral s (\x. g x \ b)" + proof (rule dominated_convergence_real) + fix k :: nat + from f show "(\x. f k x \ b) integrable_on s" by (rule integrable_component) + next + from h show "h integrable_on s" . + next + fix k :: nat + show "\x\s. norm (f k x \ b) \ h x" + proof + fix x assume x: "x \ s" + have "norm (f k x \ b) \ norm (f k x)" by (simp add: Basis_le_norm b) + also have "\ \ h x" using le[of k] x by simp + finally show "norm (f k x \ b) \ h x" . + qed + next + from conv show "\x\s. (\k. f k x \ b) \ g x \ b" + by (auto intro!: tendsto_inner) + qed + have B: "integral s ((\x. x *\<^sub>R b) \ (\x. f k x \ b)) = integral s (\x. f k x \ b) *\<^sub>R b" + for k by (rule integral_linear) + (simp_all add: f integrable_component bounded_linear_scaleR_left) + have C: "integral s ((\x. x *\<^sub>R b) \ (\x. g x \ b)) = integral s (\x. g x \ 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 "((\k. integral s (f k)) \ 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 \ 'n::euclidean_space \ real" + fixes f :: "nat \ 'n::euclidean_space \ 'm::euclidean_space" assumes "\k. (f k has_integral y k) s" "h integrable_on s" "\k. \x\s. norm (f k x) \ h x" "\x\s. (\k. f k x) \ g x" and x: "y \ x" @@ -12245,7 +12356,84 @@ by simp qed -subsection\Compute a double integral using iterated integrals and switching the order of integration\ +end + + +subsection \Integration by parts\ + +lemma integration_by_parts_interior_strong: + assumes bilinear: "bounded_bilinear (prod :: _ \ _ \ 'b :: banach)" + assumes s: "finite s" and le: "a \ b" + assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g" + assumes deriv: "\x. x\{a<.. (f has_vector_derivative f' x) (at x)" + "\x. x\{a<.. (g has_vector_derivative g' x) (at x)" + assumes int: "((\x. prod (f x) (g' x)) has_integral + (prod (f b) (g b) - prod (f a) (g a) - y)) {a..b}" + shows "((\x. prod (f' x) (g x)) has_integral y) {a..b}" +proof - + interpret bounded_bilinear prod by fact + have "((\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 :: _ \ _ \ 'b :: banach)" "a \ b" + "continuous_on {a..b} f" "continuous_on {a..b} g" + assumes "\x. x\{a<.. (f has_vector_derivative f' x) (at x)" + "\x. x\{a<.. (g has_vector_derivative g' x) (at x)" + assumes "((\x. prod (f x) (g' x)) has_integral (prod (f b) (g b) - prod (f a) (g a) - y)) {a..b}" + shows "((\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 :: _ \ _ \ 'b :: banach)" "a \ b" + "continuous_on {a..b} f" "continuous_on {a..b} g" + assumes "\x. x\{a..b} \ (f has_vector_derivative f' x) (at x)" + "\x. x\{a..b} \ (g has_vector_derivative g' x) (at x)" + assumes "((\x. prod (f x) (g' x)) has_integral (prod (f b) (g b) - prod (f a) (g a) - y)) {a..b}" + shows "((\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 :: _ \ _ \ 'b :: banach)" + assumes s: "finite s" and le: "a \ b" + assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g" + assumes deriv: "\x. x\{a<.. (f has_vector_derivative f' x) (at x)" + "\x. x\{a<.. (g has_vector_derivative g' x) (at x)" + assumes int: "(\x. prod (f x) (g' x)) integrable_on {a..b}" + shows "(\x. prod (f' x) (g x)) integrable_on {a..b}" +proof - + from int obtain I where "((\x. prod (f x) (g' x)) has_integral I) {a..b}" + unfolding integrable_on_def by blast + hence "((\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 :: _ \ _ \ 'b :: banach)" "a \ b" + "continuous_on {a..b} f" "continuous_on {a..b} g" + assumes "\x. x\{a<.. (f has_vector_derivative f' x) (at x)" + "\x. x\{a<.. (g has_vector_derivative g' x) (at x)" + assumes "(\x. prod (f x) (g' x)) integrable_on {a..b}" + shows "(\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 :: _ \ _ \ 'b :: banach)" "a \ b" + "continuous_on {a..b} f" "continuous_on {a..b} g" + assumes "\x. x\{a..b} \ (f has_vector_derivative f' x) (at x)" + "\x. x\{a..b} \ (g has_vector_derivative g' x) (at x)" + assumes "(\x. prod (f x) (g' x)) integrable_on {a..b}" + shows "(\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 \Compute a double integral using iterated integrals and switching the order of integration\ lemma setcomp_dot1: "{z. P (z \ (i,0))} = {(x,y). P(x \ 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 \ x \ s \ eventually (\y. y \ s) (nhds x)" by (subst eventually_nhds) blast +lemma eventually_nhds_x_imp_x: + "eventually P (nhds x) \ P x" + by (subst (asm) eventually_nhds) blast + lemma nhds_neq_bot [simp]: "nhds a \ 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 \ {x. P x}))" + assumes "filterlim g G (at x within (A \ {x. \P x}))" + shows "filterlim (\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 \ {x. P x}) = inf (nhds x) (principal (A \ Collect P - {x}))" + by (simp add: at_within_def) + also have "A \ Collect P - {x} = (A - {x}) \ Collect P" by blast + also have "inf (nhds x) (principal \) = 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 \ {x. \P x}) = inf (nhds x) (principal (A \ {x. \P x} - {x}))" + by (simp add: at_within_def) + also have "A \ {x. \P x} - {x} = (A - {x}) \ {x. \P x}" by blast + also have "inf (nhds x) (principal \) = inf (at x within A) (principal {x. \P x})" + by (simp add: at_within_def inf_assoc) + finally show "filterlim g G (inf (at x within A) (principal {x. \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. \P x})" + shows "filterlim (\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 \ {x} \ at x within s = inf (INF a:{x <..}. principal ({..< a} \ s - {x})) (INF a:{..< x}. principal ({a <..} \ s - {x}))" @@ -1695,6 +1727,18 @@ lemma isCont_def: "isCont f a \ f \a\ f a" by (rule continuous_at) +lemma isCont_cong: + assumes "eventually (\x. f x = g x) (nhds x)" + shows "isCont f x \ isCont g x" +proof - + from assms have [simp]: "f x = g x" by (rule eventually_nhds_x_imp_x) + from assms have "eventually (\x. f x = g x) (at x)" + by (auto simp: eventually_at_filter elim!: eventually_mono) + with assms have "isCont f x \ 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 \ 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: + "((\x::real. ln x / x) \ 0) at_top" +proof (rule lhospital_at_top_at_top[where f' = inverse and g' = "\_. 1"]) + from eventually_gt_at_top[of "0::real"] + show "\\<^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 \ - real n" "n > 0" + shows "(1 + x / of_nat n) ^ n \ 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) \ 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)) \ 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 \ real n" "n > 0" + shows "(1 - x / of_nat n) ^ n \ exp (-x)" + using exp_ge_one_plus_x_over_n_power_n[of n "-x"] assms by simp + lemma exp_at_bot: "(exp \ (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 \ a) F" and g: "(g \ b) F" and a: "a \ 0" shows "((\x. f x powr g x) \ 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 \ a) F" and g: "(g \ b) F" + and a: "a \ 0 \ (b > 0 \ eventually (\x. f x \ 0) F)" + shows "((\x. f x powr g x) \ a powr b) F" +proof - + from a consider "a \ 0" | "a = 0" "b > 0" "eventually (\x. f x \ 0) F" by auto + thus ?thesis + proof cases + assume "a \ 0" + from f g this show ?thesis by (rule tendsto_powr) + next + assume a: "a = 0" and b: "b > 0" and f_nonneg: "eventually (\x. f x \ 0) F" + hence "((\x. if f x = 0 then 0 else exp (g x * ln (f x))) \ 0) F" + proof (intro filterlim_If) + have "filterlim f (principal {0<..}) (inf F (principal {z. f z \ 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 \ 0}))" + by (rule tendsto_mono[OF _ f]) simp_all + ultimately have f: "filterlim f (at_right 0) (inf F (principal {x. f x \ 0}))" + by (simp add: at_within_def filterlim_inf a) + have g: "(g \ b) (inf F (principal {z. f z \ 0}))" + by (rule tendsto_mono[OF _ g]) simp_all + show "((\x. exp (g x * ln (f x))) \ 0) (inf F (principal {x. f x \ 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 "\x\s. f x \ (0::real)" shows "continuous_on s (\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 \ a) F" and g: "(g \ b) F" and f_nonneg: "\\<^sub>F x in F. 0 \ f x" and b: "0 < b" shows "((\x. f x powr g x) \ a powr b) F" - unfolding powr_def -proof (rule filterlim_If) - from f show "((\x. 0) \ (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 \ 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 "((\x. exp (g x * ln (f x))) \ 0) (inf F (principal {x. f x \ 0}))" - by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0] - filterlim_tendsto_pos_mult_at_bot[OF _ \0 < b\] - intro: tendsto_mono inf_le1 g) } - then show "((\x. exp (g x * ln (f x))) \ (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \ 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 "((\x. f x powr g x) \ 0) F" using tendsto_powr2[OF assms] by simp +lemma continuous_on_powr': + assumes "continuous_on s f" "continuous_on s g" and + "\x\s. f x \ (0::real) \ (f x = 0 \ g x > 0)" + shows "continuous_on s (\x. (f x) powr (g x))" + unfolding continuous_on_def +proof + fix x assume x: "x \ s" + from assms x show "((\x. f x powr g x) \ f x powr g x) (at x within s)" + proof (cases "f x = 0") + case True + from assms(3) have "eventually (\x. f x \ 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"