# HG changeset patch # User nipkow # Date 1503937641 -7200 # Node ID 65c3c8fc83e4a7b9519dca1447c58824a3560579 # Parent 322120e880c592b244e4b152f7b36e5801a2ea2c# Parent 7ca69030a2af8b46851f88f1f3642634f1952d46 merged diff -r 7ca69030a2af -r 65c3c8fc83e4 src/HOL/Analysis/Gamma_Function.thy --- a/src/HOL/Analysis/Gamma_Function.thy Mon Aug 28 18:27:16 2017 +0200 +++ b/src/HOL/Analysis/Gamma_Function.thy Mon Aug 28 18:27:21 2017 +0200 @@ -2697,6 +2697,75 @@ subsubsection \Integral form\ +lemma integrable_on_powr_from_0': + assumes a: "a > (-1::real)" and c: "c \ 0" + shows "(\x. x powr a) integrable_on {0<..c}" +proof - + from c have *: "{0<..c} - {0..c} = {}" "{0..c} - {0<..c} = {0}" by auto + show ?thesis + by (rule integrable_spike_set [OF integrable_on_powr_from_0[OF a c]]) (simp_all add: *) +qed + +lemma absolutely_integrable_Gamma_integral: + assumes "Re z > 0" "a > 0" + shows "(\t. complex_of_real t powr (z - 1) / of_real (exp (a * t))) + absolutely_integrable_on {0<..}" (is "?f absolutely_integrable_on _") +proof - + have "((\x. (Re z - 1) * (ln x / x)) \ (Re z - 1) * 0) at_top" + by (intro tendsto_intros ln_x_over_x_tendsto_0) + hence "((\x. ((Re z - 1) * ln x) / x) \ 0) at_top" by simp + from order_tendstoD(2)[OF this, of "a/2"] and \a > 0\ + have "eventually (\x. (Re z - 1) * ln x / x < a/2) at_top" by simp + from eventually_conj[OF this eventually_gt_at_top[of 0]] + obtain x0 where "\x\x0. (Re z - 1) * ln x / x < a/2 \ x > 0" + by (auto simp: eventually_at_top_linorder) + hence "x0 > 0" by simp + have "x powr (Re z - 1) / exp (a * x) < exp (-(a/2) * x)" if "x \ x0" for x + proof - + from that and \\x\x0. _\ have x: "(Re z - 1) * ln x / x < a / 2" "x > 0" by auto + have "x powr (Re z - 1) = exp ((Re z - 1) * ln x)" + using \x > 0\ by (simp add: powr_def) + also from x have "(Re z - 1) * ln x < (a * x) / 2" by (simp add: field_simps) + finally show ?thesis by (simp add: field_simps exp_add [symmetric]) + qed + note x0 = \x0 > 0\ this + + have "?f absolutely_integrable_on ({0<..x0} \ {x0..})" + proof (rule set_integrable_Un) + show "?f absolutely_integrable_on {0<..x0}" + proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2]) + show "set_integrable lebesgue {0<..x0} (\x. x powr (Re z - 1))" using x0(1) assms + by (intro nonnegative_absolutely_integrable_1 integrable_on_powr_from_0') auto + show "set_borel_measurable lebesgue {0<..x0} + (\x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" + by (intro measurable_completion) + (auto intro!: borel_measurable_continuous_on_indicator continuous_intros) + fix x :: real + have "x powr (Re z - 1) / exp (a * x) \ x powr (Re z - 1) / 1" if "x \ 0" + using that assms by (intro divide_left_mono) auto + thus "norm (indicator {0<..x0} x *\<^sub>R ?f x) \ + norm (indicator {0<..x0} x *\<^sub>R x powr (Re z - 1))" + by (simp_all add: norm_divide norm_powr_real_powr indicator_def) + qed + next + show "?f absolutely_integrable_on {x0..}" + proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2]) + show "set_integrable lebesgue {x0..} (\x. exp (-(a/2) * x))" using assms + by (intro nonnegative_absolutely_integrable_1 integrable_on_exp_minus_to_infinity) auto + show "set_borel_measurable lebesgue {x0..} + (\x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" using x0(1) + by (intro measurable_completion) + (auto intro!: borel_measurable_continuous_on_indicator continuous_intros) + fix x :: real + show "norm (indicator {x0..} x *\<^sub>R ?f x) \ + norm (indicator {x0..} x *\<^sub>R exp (-(a/2) * x))" using x0 + by (auto simp: norm_divide norm_powr_real_powr indicator_def less_imp_le) + qed + qed auto + also have "{0<..x0} \ {x0..} = {0<..}" using x0(1) by auto + finally show ?thesis . +qed + lemma integrable_Gamma_integral_bound: fixes a c :: real assumes a: "a > -1" and c: "c \ 0" @@ -2898,6 +2967,25 @@ from has_integral_linear[OF this bounded_linear_Re] show ?thesis by (simp add: o_def) qed +lemma absolutely_integrable_Gamma_integral': + assumes "Re z > 0" + shows "(\t. complex_of_real t powr (z - 1) / of_real (exp t)) absolutely_integrable_on {0<..}" + using absolutely_integrable_Gamma_integral [OF assms zero_less_one] by simp + +lemma Gamma_integral_complex': + assumes z: "Re z > 0" + shows "((\t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0<..}" +proof - + have "((\t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}" + by (rule Gamma_integral_complex) fact+ + hence "((\t. if t \ {0<..} then of_real t powr (z - 1) / of_real (exp t) else 0) + has_integral Gamma z) {0..}" + by (rule has_integral_spike [of "{0}", rotated 2]) auto + also have "?this = ?thesis" + by (subst has_integral_restrict) auto + finally show ?thesis . +qed + subsection \The Weierstraß product formula for the sine\ diff -r 7ca69030a2af -r 65c3c8fc83e4 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Aug 28 18:27:16 2017 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Aug 28 18:27:21 2017 +0200 @@ -548,60 +548,52 @@ lemma has_integral_neg_iff: "((\x. - f x) has_integral k) S \ (f has_integral - k) S" using has_integral_neg[of f "- k"] has_integral_neg[of "\x. - f x" k] by auto +lemma has_integral_add_cbox: + fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" + assumes "(f has_integral k) (cbox a b)" "(g has_integral l) (cbox a b)" + shows "((\x. f x + g x) has_integral (k + l)) (cbox a b)" + using assms + unfolding has_integral_cbox + by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add) + lemma has_integral_add: fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" - assumes "(f has_integral k) S" - and "(g has_integral l) S" + assumes f: "(f has_integral k) S" and g: "(g has_integral l) S" shows "((\x. f x + g x) has_integral (k + l)) S" -proof - - have lem: "(f has_integral k) (cbox a b) \ (g has_integral l) (cbox a b) \ - ((\x. f x + g x) has_integral (k + l)) (cbox a b)" - for f :: "'n \ 'a" and g a b k l - unfolding has_integral_cbox - by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add) - { - presume "\ (\a b. S = cbox a b) \ ?thesis" - then show ?thesis - using assms lem by force - } - assume nonbox: "\ (\a b. S = cbox a b)" +proof (cases "\a b. S = cbox a b") + case True with has_integral_add_cbox assms show ?thesis + by blast +next + let ?S = "\f x. if x \ S then f x else 0" + case False then show ?thesis proof (subst has_integral_alt, clarsimp, goal_cases) case (1 e) - then have *: "e/2 > 0" + then have e2: "e/2 > 0" by auto - from has_integral_altD[OF assms(1) nonbox *] - obtain B1 where B1: - "0 < B1" - "\a b. ball 0 B1 \ cbox a b \ - \z. ((\x. if x \ S then f x else 0) has_integral z) (cbox a b) \ norm (z - k) < e/2" - by blast - from has_integral_altD[OF assms(2) nonbox *] - obtain B2 where B2: - "0 < B2" - "\a b. ball 0 B2 \ (cbox a b) \ - \z. ((\x. if x \ S then g x else 0) has_integral z) (cbox a b) \ norm (z - l) < e/2" - by blast + obtain Bf where "0 < Bf" + and Bf: "\a b. ball 0 Bf \ cbox a b \ + \z. (?S f has_integral z) (cbox a b) \ norm (z - k) < e/2" + using has_integral_altD[OF f False e2] by blast + obtain Bg where "0 < Bg" + and Bg: "\a b. ball 0 Bg \ (cbox a b) \ + \z. (?S g has_integral z) (cbox a b) \ norm (z - l) < e/2" + using has_integral_altD[OF g False e2] by blast show ?case - proof (rule_tac x="max B1 B2" in exI, clarsimp simp add: max.strict_coboundedI1 B1) + proof (rule_tac x="max Bf Bg" in exI, clarsimp simp add: max.strict_coboundedI1 \0 < Bf\) fix a b - assume "ball 0 (max B1 B2) \ cbox a (b::'n)" - then have *: "ball 0 B1 \ cbox a (b::'n)" "ball 0 B2 \ cbox a (b::'n)" + assume "ball 0 (max Bf Bg) \ cbox a (b::'n)" + then have fs: "ball 0 Bf \ cbox a (b::'n)" and gs: "ball 0 Bg \ cbox a (b::'n)" by auto - obtain w where w: - "((\x. if x \ S then f x else 0) has_integral w) (cbox a b)" - "norm (w - k) < e/2" - using B1(2)[OF *(1)] by blast - obtain z where z: - "((\x. if x \ S then g x else 0) has_integral z) (cbox a b)" - "norm (z - l) < e/2" - using B2(2)[OF *(2)] by blast - have *: "\x. (if x \ S then f x + g x else 0) = - (if x \ S then f x else 0) + (if x \ S then g x else 0)" + obtain w where w: "(?S f has_integral w) (cbox a b)" "norm (w - k) < e/2" + using Bf[OF fs] by blast + obtain z where z: "(?S g has_integral z) (cbox a b)" "norm (z - l) < e/2" + using Bg[OF gs] by blast + have *: "\x. (if x \ S then f x + g x else 0) = (?S f x) + (?S g x)" by auto - show "\z. ((\x. if x \ S then f x + g x else 0) has_integral z) (cbox a b) \ norm (z - (k + l)) < e" + show "\z. (?S(\x. f x + g x) has_integral z) (cbox a b) \ norm (z - (k + l)) < e" apply (rule_tac x="w + z" in exI) - apply (simp add: lem[OF w(1) z(1), unfolded *[symmetric]]) + apply (simp add: has_integral_add_cbox[OF w(1) z(1), unfolded *[symmetric]]) using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2) apply (auto simp add: field_simps) done @@ -2875,129 +2867,87 @@ subsection \Only need trivial subintervals if the interval itself is trivial.\ -lemma division_of_nontrivial: - fixes s :: "'a::euclidean_space set set" - assumes "s division_of (cbox a b)" - and "content (cbox a b) \ 0" - shows "{k. k \ s \ content k \ 0} division_of (cbox a b)" - using assms(1) - apply - -proof (induct "card s" arbitrary: s rule: nat_less_induct) - fix s::"'a set set" - assume assm: "s division_of (cbox a b)" - "\mx. m = card x \ - x division_of (cbox a b) \ {k \ x. content k \ 0} division_of (cbox a b)" - note s = division_ofD[OF assm(1)] - let ?thesis = "{k \ s. content k \ 0} division_of (cbox a b)" +proposition division_of_nontrivial: + fixes \ :: "'a::euclidean_space set set" + assumes sdiv: "\ division_of (cbox a b)" + and cont0: "content (cbox a b) \ 0" + shows "{k. k \ \ \ content k \ 0} division_of (cbox a b)" + using sdiv +proof (induction "card \" arbitrary: \ rule: less_induct) + case less + note \ = division_ofD[OF less.prems] { - presume *: "{k \ s. content k \ 0} \ s \ ?thesis" - show ?thesis - apply cases - defer - apply (rule *) - apply assumption - using assm(1) - apply auto - done + presume *: "{k \ \. content k \ 0} \ \ \ ?case" + then show ?case + using less.prems by fastforce } - assume noteq: "{k \ s. content k \ 0} \ s" - then obtain k c d where k: "k \ s" "content k = 0" "k = cbox c d" - using s(4) by blast - then have "card s > 0" - unfolding card_gt_0_iff using assm(1) by auto - then have card: "card (s - {k}) < card s" - using assm(1) k(1) - apply (subst card_Diff_singleton_if) - apply auto - done - have *: "closed (\(s - {k}))" - apply (rule closed_Union) - defer - apply rule - apply (drule DiffD1,drule s(4)) - using assm(1) - apply auto - done - have "k \ \(s - {k})" - apply safe - apply (rule *[unfolded closed_limpt,rule_format]) + assume noteq: "{k \ \. content k \ 0} \ \" + then obtain K c d where "K \ \" and contk: "content K = 0" and keq: "K = cbox c d" + using \(4) by blast + then have "card \ > 0" + unfolding card_gt_0_iff using less by auto + then have card: "card (\ - {K}) < card \" + using less \K \ \\ by (simp add: \(1)) + have closed: "closed (\(\ - {K}))" + using less.prems by auto + have "x islimpt \(\ - {K})" if "x \ K" for x unfolding islimpt_approachable - proof safe - fix x - fix e :: real - assume as: "x \ k" "e > 0" + proof (intro allI impI) + fix e::real + assume "e > 0" obtain i where i: "c\i = d\i" "i\Basis" - using k(2) s(3)[OF k(1)] unfolding box_ne_empty k - by (metis dual_order.antisym content_eq_0) + using contk \(3) [OF \K \ \\] unfolding box_ne_empty keq + by (meson content_eq_0 dual_order.antisym) then have xi: "x\i = d\i" - using as unfolding k mem_box by (metis antisym) + using \x \ K\ unfolding keq mem_box by (metis antisym) define y where "y = (\j\Basis. (if j = i then if c\i \ (a\i + b\i) / 2 then c\i + min e (b\i - c\i) / 2 else c\i - min e (c\i - a\i) / 2 else x\j) *\<^sub>R j)" - show "\x'\\(s - {k}). x' \ x \ dist x' x < e" - apply (rule_tac x=y in bexI) - proof + show "\x'\\(\ - {K}). x' \ x \ dist x' x < e" + proof (intro bexI conjI) have "d \ cbox c d" - using s(3)[OF k(1)] - unfolding k box_eq_empty mem_box - by (fastforce simp add: not_less) + using \(3)[OF \K \ \\] by (simp add: box_ne_empty(1) keq mem_box(2)) then have "d \ cbox a b" - using s(2)[OF k(1)] - unfolding k - by auto - note di = this[unfolded mem_box,THEN bspec[where x=i]] + using \(2)[OF \K \ \\] by (auto simp: keq) + then have di: "a \ i \ d \ i \ d \ i \ b \ i" + using \i \ Basis\ mem_box(2) by blast then have xyi: "y\i \ x\i" - unfolding y_def i xi - using as(2) assms(2)[unfolded content_eq_0] i(2) - by (auto elim!: ballE[of _ _ i]) + unfolding y_def i xi using \e > 0\ cont0 \i \ Basis\ + by (auto simp: content_eq_0 elim!: ballE[of _ _ i]) then show "y \ x" unfolding euclidean_eq_iff[where 'a='a] using i by auto - have *: "Basis = insert i (Basis - {i})" - using i by auto - have "norm (y-x) < e + sum (\i. 0) Basis" - apply (rule le_less_trans[OF norm_le_l1]) - apply (subst *) - apply (subst sum.insert) - prefer 3 - apply (rule add_less_le_mono) - proof - + have "norm (y-x) \ (\b\Basis. \(y - x) \ b\)" + by (rule norm_le_l1) + also have "... = \(y - x) \ i\ + (\b \ Basis - {i}. \(y - x) \ b\)" + by (meson finite_Basis i(2) sum.remove) + also have "... < e + sum (\i. 0) Basis" + proof (rule add_less_le_mono) show "\(y-x) \ i\ < e" - using di as(2) y_def i xi by (auto simp: inner_simps) + using di \e > 0\ y_def i xi by (auto simp: inner_simps) show "(\i\Basis - {i}. \(y-x) \ i\) \ (\i\Basis. 0)" unfolding y_def by (auto simp: inner_simps) - qed auto + qed + finally have "norm (y-x) < e + sum (\i. 0) Basis" . then show "dist y x < e" unfolding dist_norm by auto - have "y \ k" - unfolding k mem_box - apply rule - apply (erule_tac x=i in ballE) - using xyi k i xi - apply auto - done - moreover - have "y \ \s" - using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i - unfolding s mem_box y_def - by (auto simp: field_simps elim!: ballE[of _ _ i]) - ultimately - show "y \ \(s - {k})" by auto + have "y \ K" + unfolding keq mem_box using i(1) i(2) xi xyi by fastforce + moreover have "y \ \\" + using subsetD[OF \(2)[OF \K \ \\] \x \ K\] \e > 0\ di i + by (auto simp: \ mem_box y_def field_simps elim!: ballE[of _ _ i]) + ultimately show "y \ \(\ - {K})" by auto qed qed - then have "\(s - {k}) = cbox a b" - unfolding s(6)[symmetric] by auto - then have "{ka \ s - {k}. content ka \ 0} division_of (cbox a b)" - apply - - apply (rule assm(2)[rule_format,OF card refl]) - apply (rule division_ofI) - defer - apply (rule_tac[1-4] s) - using assm(1) - apply auto - done - moreover - have "{ka \ s - {k}. content ka \ 0} = {k \ s. content k \ 0}" - using k by auto - ultimately show ?thesis by auto + then have "K \ \(\ - {K})" + using closed closed_limpt by blast + then have "\(\ - {K}) = cbox a b" + unfolding \(6)[symmetric] by auto + then have "\ - {K} division_of cbox a b" + by (metis Diff_subset less.prems division_of_subset \(6)) + then have "{ka \ \ - {K}. content ka \ 0} division_of (cbox a b)" + using card less.hyps by blast + moreover have "{ka \ \ - {K}. content ka \ 0} = {K \ \. content K \ 0}" + using contk by auto + ultimately show ?case by auto qed @@ -3046,7 +2996,7 @@ assumes "f integrable_on {a..b}" and "{c..d} \ {a..b}" shows "f integrable_on {c..d}" - by (metis assms(1) assms(2) box_real(2) integrable_subinterval) + by (metis assms box_real(2) integrable_subinterval) subsection \Combining adjacent intervals in 1 dimension.\ @@ -4202,11 +4152,9 @@ unfolding *(1) apply (subst *(2)) apply (rule norm_triangle_lt add_strict_mono)+ - unfolding norm_minus_cancel - apply (rule d1_fin[unfolded **]) - apply (rule d2_fin) + apply (metis "**" d1_fin norm_minus_cancel) + using d2_fin apply blast using w *** - unfolding norm_scaleR apply (auto simp add: field_simps) done qed diff -r 7ca69030a2af -r 65c3c8fc83e4 src/HOL/Analysis/Infinite_Set_Sum.thy --- a/src/HOL/Analysis/Infinite_Set_Sum.thy Mon Aug 28 18:27:16 2017 +0200 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Mon Aug 28 18:27:21 2017 +0200 @@ -108,6 +108,15 @@ "\\<^sub>ai\A. b" \ "CONST infsetsum (\i. b) A" syntax (ASCII) + "_uinfsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" + ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) +syntax + "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" + ("(2\\<^sub>a_./ _)" [0, 10] 10) +translations \ \Beware of argument permutation!\ + "\\<^sub>ai. b" \ "CONST infsetsum (\i. b) (CONST UNIV)" + +syntax (ASCII) "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10) syntax @@ -159,6 +168,31 @@ "A \ B \ f abs_summable_on A \ set_integrable (count_space B) A f" by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def) +lemma abs_summable_on_norm_iff [simp]: + "(\x. norm (f x)) abs_summable_on A \ f abs_summable_on A" + by (simp add: abs_summable_on_def integrable_norm_iff) + +lemma abs_summable_on_normI: "f abs_summable_on A \ (\x. norm (f x)) abs_summable_on A" + by simp + +lemma abs_summable_on_comparison_test: + assumes "g abs_summable_on A" + assumes "\x. x \ A \ norm (f x) \ norm (g x)" + shows "f abs_summable_on A" + using assms Bochner_Integration.integrable_bound[of "count_space A" g f] + unfolding abs_summable_on_def by (auto simp: AE_count_space) + +lemma abs_summable_on_comparison_test': + assumes "g abs_summable_on A" + assumes "\x. x \ A \ norm (f x) \ g x" + shows "f abs_summable_on A" +proof (rule abs_summable_on_comparison_test[OF assms(1), of f]) + fix x assume "x \ A" + with assms(2) have "norm (f x) \ g x" . + also have "\ \ norm (g x)" by simp + finally show "norm (f x) \ norm (g x)" . +qed + lemma abs_summable_on_cong [cong]: "(\x. x \ A \ f x = g x) \ A = B \ (f abs_summable_on A) \ (g abs_summable_on B)" unfolding abs_summable_on_def by (intro integrable_cong) auto @@ -210,6 +244,18 @@ shows "f abs_summable_on (A \ B)" using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto +lemma abs_summable_on_insert_iff [simp]: + "f abs_summable_on insert x A \ f abs_summable_on A" +proof safe + assume "f abs_summable_on insert x A" + thus "f abs_summable_on A" + by (rule abs_summable_on_subset) auto +next + assume "f abs_summable_on A" + from abs_summable_on_union[OF this, of "{x}"] + show "f abs_summable_on insert x A" by simp +qed + lemma abs_summable_on_reindex_bij_betw: assumes "bij_betw g A B" shows "(\x. f (g x)) abs_summable_on A \ f abs_summable_on B" @@ -235,11 +281,11 @@ finally show ?thesis . qed -lemma abs_summable_reindex_iff: +lemma abs_summable_on_reindex_iff: "inj_on g A \ (\x. f (g x)) abs_summable_on A \ f abs_summable_on (g ` A)" by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw) -lemma abs_summable_on_Sigma_project: +lemma abs_summable_on_Sigma_project2: fixes A :: "'a set" and B :: "'a \ 'b set" assumes "f abs_summable_on (Sigma A B)" "x \ A" shows "(\y. f (x, y)) abs_summable_on (B x)" @@ -425,6 +471,46 @@ by (intro Bochner_Integration.integral_cong refl) (auto simp: indicator_def split: if_splits) +lemma infsetsum_mono_neutral: + fixes f g :: "'a \ real" + assumes "f abs_summable_on A" and "g abs_summable_on B" + assumes "\x. x \ A \ f x \ g x" + assumes "\x. x \ A - B \ f x \ 0" + assumes "\x. x \ B - A \ g x \ 0" + shows "infsetsum f A \ infsetsum g B" + using assms unfolding infsetsum_altdef abs_summable_on_altdef + by (intro Bochner_Integration.integral_mono) (auto simp: indicator_def) + +lemma infsetsum_mono_neutral_left: + fixes f g :: "'a \ real" + assumes "f abs_summable_on A" and "g abs_summable_on B" + assumes "\x. x \ A \ f x \ g x" + assumes "A \ B" + assumes "\x. x \ B - A \ g x \ 0" + shows "infsetsum f A \