--- 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 \<open>Integral form\<close>
+lemma integrable_on_powr_from_0':
+ assumes a: "a > (-1::real)" and c: "c \<ge> 0"
+ shows "(\<lambda>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 "(\<lambda>t. complex_of_real t powr (z - 1) / of_real (exp (a * t)))
+ absolutely_integrable_on {0<..}" (is "?f absolutely_integrable_on _")
+proof -
+ have "((\<lambda>x. (Re z - 1) * (ln x / x)) \<longlongrightarrow> (Re z - 1) * 0) at_top"
+ by (intro tendsto_intros ln_x_over_x_tendsto_0)
+ hence "((\<lambda>x. ((Re z - 1) * ln x) / x) \<longlongrightarrow> 0) at_top" by simp
+ from order_tendstoD(2)[OF this, of "a/2"] and \<open>a > 0\<close>
+ have "eventually (\<lambda>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 "\<forall>x\<ge>x0. (Re z - 1) * ln x / x < a/2 \<and> 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 \<ge> x0" for x
+ proof -
+ from that and \<open>\<forall>x\<ge>x0. _\<close> 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 \<open>x > 0\<close> 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 = \<open>x0 > 0\<close> this
+
+ have "?f absolutely_integrable_on ({0<..x0} \<union> {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} (\<lambda>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}
+ (\<lambda>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) \<le> x powr (Re z - 1) / 1" if "x \<ge> 0"
+ using that assms by (intro divide_left_mono) auto
+ thus "norm (indicator {0<..x0} x *\<^sub>R ?f x) \<le>
+ 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..} (\<lambda>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..}
+ (\<lambda>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) \<le>
+ 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} \<union> {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 \<ge> 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 "(\<lambda>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 "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0<..}"
+proof -
+ have "((\<lambda>t. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}"
+ by (rule Gamma_integral_complex) fact+
+ hence "((\<lambda>t. if t \<in> {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 \<open>The Weierstraß product formula for the sine\<close>
--- 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: "((\<lambda>x. - f x) has_integral k) S \<longleftrightarrow> (f has_integral - k) S"
using has_integral_neg[of f "- k"] has_integral_neg[of "\<lambda>x. - f x" k] by auto
+lemma has_integral_add_cbox:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
+ assumes "(f has_integral k) (cbox a b)" "(g has_integral l) (cbox a b)"
+ shows "((\<lambda>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 \<Rightarrow> '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 "((\<lambda>x. f x + g x) has_integral (k + l)) S"
-proof -
- have lem: "(f has_integral k) (cbox a b) \<Longrightarrow> (g has_integral l) (cbox a b) \<Longrightarrow>
- ((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
- for f :: "'n \<Rightarrow> '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 "\<not> (\<exists>a b. S = cbox a b) \<Longrightarrow> ?thesis"
- then show ?thesis
- using assms lem by force
- }
- assume nonbox: "\<not> (\<exists>a b. S = cbox a b)"
+proof (cases "\<exists>a b. S = cbox a b")
+ case True with has_integral_add_cbox assms show ?thesis
+ by blast
+next
+ let ?S = "\<lambda>f x. if x \<in> 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"
- "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
- \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - k) < e/2"
- by blast
- from has_integral_altD[OF assms(2) nonbox *]
- obtain B2 where B2:
- "0 < B2"
- "\<And>a b. ball 0 B2 \<subseteq> (cbox a b) \<Longrightarrow>
- \<exists>z. ((\<lambda>x. if x \<in> S then g x else 0) has_integral z) (cbox a b) \<and> norm (z - l) < e/2"
- by blast
+ obtain Bf where "0 < Bf"
+ and Bf: "\<And>a b. ball 0 Bf \<subseteq> cbox a b \<Longrightarrow>
+ \<exists>z. (?S f has_integral z) (cbox a b) \<and> norm (z - k) < e/2"
+ using has_integral_altD[OF f False e2] by blast
+ obtain Bg where "0 < Bg"
+ and Bg: "\<And>a b. ball 0 Bg \<subseteq> (cbox a b) \<Longrightarrow>
+ \<exists>z. (?S g has_integral z) (cbox a b) \<and> 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 \<open>0 < Bf\<close>)
fix a b
- assume "ball 0 (max B1 B2) \<subseteq> cbox a (b::'n)"
- then have *: "ball 0 B1 \<subseteq> cbox a (b::'n)" "ball 0 B2 \<subseteq> cbox a (b::'n)"
+ assume "ball 0 (max Bf Bg) \<subseteq> cbox a (b::'n)"
+ then have fs: "ball 0 Bf \<subseteq> cbox a (b::'n)" and gs: "ball 0 Bg \<subseteq> cbox a (b::'n)"
by auto
- obtain w where w:
- "((\<lambda>x. if x \<in> 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:
- "((\<lambda>x. if x \<in> 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 *: "\<And>x. (if x \<in> S then f x + g x else 0) =
- (if x \<in> S then f x else 0) + (if x \<in> 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 *: "\<And>x. (if x \<in> S then f x + g x else 0) = (?S f x) + (?S g x)"
by auto
- show "\<exists>z. ((\<lambda>x. if x \<in> S then f x + g x else 0) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
+ show "\<exists>z. (?S(\<lambda>x. f x + g x) has_integral z) (cbox a b) \<and> 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 \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
-lemma division_of_nontrivial:
- fixes s :: "'a::euclidean_space set set"
- assumes "s division_of (cbox a b)"
- and "content (cbox a b) \<noteq> 0"
- shows "{k. k \<in> s \<and> content k \<noteq> 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)"
- "\<forall>m<card s. \<forall>x. m = card x \<longrightarrow>
- x division_of (cbox a b) \<longrightarrow> {k \<in> x. content k \<noteq> 0} division_of (cbox a b)"
- note s = division_ofD[OF assm(1)]
- let ?thesis = "{k \<in> s. content k \<noteq> 0} division_of (cbox a b)"
+proposition division_of_nontrivial:
+ fixes \<D> :: "'a::euclidean_space set set"
+ assumes sdiv: "\<D> division_of (cbox a b)"
+ and cont0: "content (cbox a b) \<noteq> 0"
+ shows "{k. k \<in> \<D> \<and> content k \<noteq> 0} division_of (cbox a b)"
+ using sdiv
+proof (induction "card \<D>" arbitrary: \<D> rule: less_induct)
+ case less
+ note \<D> = division_ofD[OF less.prems]
{
- presume *: "{k \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?thesis"
- show ?thesis
- apply cases
- defer
- apply (rule *)
- apply assumption
- using assm(1)
- apply auto
- done
+ presume *: "{k \<in> \<D>. content k \<noteq> 0} \<noteq> \<D> \<Longrightarrow> ?case"
+ then show ?case
+ using less.prems by fastforce
}
- assume noteq: "{k \<in> s. content k \<noteq> 0} \<noteq> s"
- then obtain k c d where k: "k \<in> 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 (\<Union>(s - {k}))"
- apply (rule closed_Union)
- defer
- apply rule
- apply (drule DiffD1,drule s(4))
- using assm(1)
- apply auto
- done
- have "k \<subseteq> \<Union>(s - {k})"
- apply safe
- apply (rule *[unfolded closed_limpt,rule_format])
+ assume noteq: "{k \<in> \<D>. content k \<noteq> 0} \<noteq> \<D>"
+ then obtain K c d where "K \<in> \<D>" and contk: "content K = 0" and keq: "K = cbox c d"
+ using \<D>(4) by blast
+ then have "card \<D> > 0"
+ unfolding card_gt_0_iff using less by auto
+ then have card: "card (\<D> - {K}) < card \<D>"
+ using less \<open>K \<in> \<D>\<close> by (simp add: \<D>(1))
+ have closed: "closed (\<Union>(\<D> - {K}))"
+ using less.prems by auto
+ have "x islimpt \<Union>(\<D> - {K})" if "x \<in> K" for x
unfolding islimpt_approachable
- proof safe
- fix x
- fix e :: real
- assume as: "x \<in> k" "e > 0"
+ proof (intro allI impI)
+ fix e::real
+ assume "e > 0"
obtain i where i: "c\<bullet>i = d\<bullet>i" "i\<in>Basis"
- using k(2) s(3)[OF k(1)] unfolding box_ne_empty k
- by (metis dual_order.antisym content_eq_0)
+ using contk \<D>(3) [OF \<open>K \<in> \<D>\<close>] unfolding box_ne_empty keq
+ by (meson content_eq_0 dual_order.antisym)
then have xi: "x\<bullet>i = d\<bullet>i"
- using as unfolding k mem_box by (metis antisym)
+ using \<open>x \<in> K\<close> unfolding keq mem_box by (metis antisym)
define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j)"
- show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e"
- apply (rule_tac x=y in bexI)
- proof
+ show "\<exists>x'\<in>\<Union>(\<D> - {K}). x' \<noteq> x \<and> dist x' x < e"
+ proof (intro bexI conjI)
have "d \<in> cbox c d"
- using s(3)[OF k(1)]
- unfolding k box_eq_empty mem_box
- by (fastforce simp add: not_less)
+ using \<D>(3)[OF \<open>K \<in> \<D>\<close>] by (simp add: box_ne_empty(1) keq mem_box(2))
then have "d \<in> 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 \<D>(2)[OF \<open>K \<in> \<D>\<close>] by (auto simp: keq)
+ then have di: "a \<bullet> i \<le> d \<bullet> i \<and> d \<bullet> i \<le> b \<bullet> i"
+ using \<open>i \<in> Basis\<close> mem_box(2) by blast
then have xyi: "y\<bullet>i \<noteq> x\<bullet>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 \<open>e > 0\<close> cont0 \<open>i \<in> Basis\<close>
+ by (auto simp: content_eq_0 elim!: ballE[of _ _ i])
then show "y \<noteq> 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 (\<lambda>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) \<le> (\<Sum>b\<in>Basis. \<bar>(y - x) \<bullet> b\<bar>)"
+ by (rule norm_le_l1)
+ also have "... = \<bar>(y - x) \<bullet> i\<bar> + (\<Sum>b \<in> Basis - {i}. \<bar>(y - x) \<bullet> b\<bar>)"
+ by (meson finite_Basis i(2) sum.remove)
+ also have "... < e + sum (\<lambda>i. 0) Basis"
+ proof (rule add_less_le_mono)
show "\<bar>(y-x) \<bullet> i\<bar> < e"
- using di as(2) y_def i xi by (auto simp: inner_simps)
+ using di \<open>e > 0\<close> y_def i xi by (auto simp: inner_simps)
show "(\<Sum>i\<in>Basis - {i}. \<bar>(y-x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)"
unfolding y_def by (auto simp: inner_simps)
- qed auto
+ qed
+ finally have "norm (y-x) < e + sum (\<lambda>i. 0) Basis" .
then show "dist y x < e"
unfolding dist_norm by auto
- have "y \<notin> 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 \<in> \<Union>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 \<in> \<Union>(s - {k})" by auto
+ have "y \<notin> K"
+ unfolding keq mem_box using i(1) i(2) xi xyi by fastforce
+ moreover have "y \<in> \<Union>\<D>"
+ using subsetD[OF \<D>(2)[OF \<open>K \<in> \<D>\<close>] \<open>x \<in> K\<close>] \<open>e > 0\<close> di i
+ by (auto simp: \<D> mem_box y_def field_simps elim!: ballE[of _ _ i])
+ ultimately show "y \<in> \<Union>(\<D> - {K})" by auto
qed
qed
- then have "\<Union>(s - {k}) = cbox a b"
- unfolding s(6)[symmetric] by auto
- then have "{ka \<in> s - {k}. content ka \<noteq> 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 \<in> s - {k}. content ka \<noteq> 0} = {k \<in> s. content k \<noteq> 0}"
- using k by auto
- ultimately show ?thesis by auto
+ then have "K \<subseteq> \<Union>(\<D> - {K})"
+ using closed closed_limpt by blast
+ then have "\<Union>(\<D> - {K}) = cbox a b"
+ unfolding \<D>(6)[symmetric] by auto
+ then have "\<D> - {K} division_of cbox a b"
+ by (metis Diff_subset less.prems division_of_subset \<D>(6))
+ then have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} division_of (cbox a b)"
+ using card less.hyps by blast
+ moreover have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} = {K \<in> \<D>. content K \<noteq> 0}"
+ using contk by auto
+ ultimately show ?case by auto
qed
@@ -3046,7 +2996,7 @@
assumes "f integrable_on {a..b}"
and "{c..d} \<subseteq> {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 \<open>Combining adjacent intervals in 1 dimension.\<close>
@@ -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
--- 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 @@
"\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
syntax (ASCII)
+ "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
+ ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
+syntax
+ "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
+ ("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
+translations \<comment> \<open>Beware of argument permutation!\<close>
+ "\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
+
+syntax (ASCII)
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
syntax
@@ -159,6 +168,31 @@
"A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> 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]:
+ "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> 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 \<Longrightarrow> (\<lambda>x. norm (f x)) abs_summable_on A"
+ by simp
+
+lemma abs_summable_on_comparison_test:
+ assumes "g abs_summable_on A"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> 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 "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> g x"
+ shows "f abs_summable_on A"
+proof (rule abs_summable_on_comparison_test[OF assms(1), of f])
+ fix x assume "x \<in> A"
+ with assms(2) have "norm (f x) \<le> g x" .
+ also have "\<dots> \<le> norm (g x)" by simp
+ finally show "norm (f x) \<le> norm (g x)" .
+qed
+
lemma abs_summable_on_cong [cong]:
"(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> (f abs_summable_on A) \<longleftrightarrow> (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 \<union> 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 \<longleftrightarrow> 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 "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> 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 \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> 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 \<Rightarrow> 'b set"
assumes "f abs_summable_on (Sigma A B)" "x \<in> A"
shows "(\<lambda>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 \<Rightarrow> real"
+ assumes "f abs_summable_on A" and "g abs_summable_on B"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+ assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
+ assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
+ shows "infsetsum f A \<le> 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 \<Rightarrow> real"
+ assumes "f abs_summable_on A" and "g abs_summable_on B"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+ assumes "A \<subseteq> B"
+ assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
+ shows "infsetsum f A \<le> infsetsum g B"
+ using \<open>A \<subseteq> B\<close> by (intro infsetsum_mono_neutral assms) auto
+
+lemma infsetsum_mono_neutral_right:
+ fixes f g :: "'a \<Rightarrow> real"
+ assumes "f abs_summable_on A" and "g abs_summable_on B"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+ assumes "B \<subseteq> A"
+ assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
+ shows "infsetsum f A \<le> infsetsum g B"
+ using \<open>B \<subseteq> A\<close> by (intro infsetsum_mono_neutral assms) auto
+
+lemma infsetsum_mono:
+ fixes f g :: "'a \<Rightarrow> real"
+ assumes "f abs_summable_on A" and "g abs_summable_on A"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+ shows "infsetsum f A \<le> infsetsum g A"
+ by (intro infsetsum_mono_neutral assms) auto
+
+lemma norm_infsetsum_bound:
+ "norm (infsetsum f A) \<le> infsetsum (\<lambda>x. norm (f x)) A"
+ unfolding abs_summable_on_def infsetsum_def
+ by (rule Bochner_Integration.integral_norm_bound)
+
lemma infsetsum_Sigma:
fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
assumes [simp]: "countable A" and "\<And>i. countable (B i)"
@@ -460,6 +546,13 @@
finally show ?thesis ..
qed
+lemma infsetsum_Sigma':
+ fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+ assumes [simp]: "countable A" and "\<And>i. countable (B i)"
+ assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (Sigma A B)"
+ shows "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) A = infsetsum (\<lambda>(x,y). f x y) (Sigma A B)"
+ using assms by (subst infsetsum_Sigma) auto
+
lemma infsetsum_Times:
fixes A :: "'a set" and B :: "'b set"
assumes [simp]: "countable A" and "countable B"
@@ -496,6 +589,95 @@
finally show ?thesis .
qed
+lemma abs_summable_on_Sigma_iff:
+ assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+ shows "f abs_summable_on Sigma A B \<longleftrightarrow>
+ (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
+ ((\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
+proof safe
+ define B' where "B' = (\<Union>x\<in>A. B x)"
+ have [simp]: "countable B'"
+ unfolding B'_def using assms by auto
+ interpret pair_sigma_finite "count_space A" "count_space B'"
+ by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
+
+ {
+ assume *: "f abs_summable_on Sigma A B"
+ thus "(\<lambda>y. f (x, y)) abs_summable_on B x" if "x \<in> A" for x
+ using that by (rule abs_summable_on_Sigma_project2)
+
+ have "set_integrable (count_space (A \<times> B')) (Sigma A B) (\<lambda>z. norm (f z))"
+ using abs_summable_on_normI[OF *]
+ by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
+ also have "count_space (A \<times> B') = count_space A \<Otimes>\<^sub>M count_space B'"
+ by (simp add: pair_measure_countable)
+ finally have "integrable (count_space A)
+ (\<lambda>x. lebesgue_integral (count_space B')
+ (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
+ by (rule integrable_fst')
+ also have "?this \<longleftrightarrow> integrable (count_space A)
+ (\<lambda>x. lebesgue_integral (count_space B')
+ (\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
+ by (intro integrable_cong refl) (simp_all add: indicator_def)
+ also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
+ by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
+ also have "\<dots> \<longleftrightarrow> (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A"
+ by (simp add: abs_summable_on_def)
+ finally show \<dots> .
+ }
+
+ {
+ assume *: "\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x"
+ assume "(\<lambda>x. \<Sum>\<^sub>ay\<in>B x. norm (f (x, y))) abs_summable_on A"
+ also have "?this \<longleftrightarrow> (\<lambda>x. \<integral>y\<in>B x. norm (f (x, y)) \<partial>count_space B') abs_summable_on A"
+ by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
+ also have "\<dots> \<longleftrightarrow> (\<lambda>x. \<integral>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y)) \<partial>count_space B')
+ abs_summable_on A" (is "_ \<longleftrightarrow> ?h abs_summable_on _")
+ by (intro abs_summable_on_cong) (auto simp: indicator_def)
+ also have "\<dots> \<longleftrightarrow> integrable (count_space A) ?h"
+ by (simp add: abs_summable_on_def)
+ finally have **: \<dots> .
+
+ have "integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
+ proof (rule Fubini_integrable, goal_cases)
+ case 3
+ {
+ fix x assume x: "x \<in> A"
+ with * have "(\<lambda>y. f (x, y)) abs_summable_on B x"
+ by blast
+ also have "?this \<longleftrightarrow> integrable (count_space B')
+ (\<lambda>y. indicator (B x) y *\<^sub>R f (x, y))"
+ using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
+ also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) =
+ (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
+ using x by (auto simp: indicator_def)
+ finally have "integrable (count_space B')
+ (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))" .
+ }
+ thus ?case by (auto simp: AE_count_space)
+ qed (insert **, auto simp: pair_measure_countable)
+ also have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
+ by (simp add: pair_measure_countable)
+ also have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
+ f abs_summable_on Sigma A B"
+ by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
+ finally show \<dots> .
+ }
+qed
+
+lemma abs_summable_on_Sigma_project1:
+ assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
+ assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+ shows "(\<lambda>x. infsetsum (\<lambda>y. norm (f x y)) (B x)) abs_summable_on A"
+ using assms by (subst (asm) abs_summable_on_Sigma_iff) auto
+
+lemma abs_summable_on_Sigma_project1':
+ assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
+ assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+ shows "(\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) abs_summable_on A"
+ by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
+ norm_infsetsum_bound)
+
lemma infsetsum_prod_PiE:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
@@ -565,6 +747,29 @@
using assms unfolding infsetsum_def abs_summable_on_def
by (rule Bochner_Integration.integral_mult_right)
+lemma infsetsum_cdiv:
+ fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_field, second_countable_topology}"
+ assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+ shows "infsetsum (\<lambda>x. f x / c) A = infsetsum f A / c"
+ using assms unfolding infsetsum_def abs_summable_on_def by auto
+
+
(* TODO Generalise with bounded_linear *)
+lemma
+ fixes f :: "'a \<Rightarrow> 'c :: {banach, real_normed_field, second_countable_topology}"
+ assumes [simp]: "countable A" and [simp]: "countable B"
+ assumes "f abs_summable_on A" and "g abs_summable_on B"
+ shows abs_summable_on_product: "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
+ and infsetsum_product: "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) =
+ infsetsum f A * infsetsum g B"
+proof -
+ from assms show "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
+ by (subst abs_summable_on_Sigma_iff)
+ (auto intro!: abs_summable_on_cmult_right simp: norm_mult infsetsum_cmult_right)
+ with assms show "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) = infsetsum f A * infsetsum g B"
+ by (subst infsetsum_Sigma)
+ (auto simp: infsetsum_cmult_left infsetsum_cmult_right)
+qed
+
end