Theory HOL-Analysis.Infinite_Set_Sum
section ‹Sums over Infinite Sets›
theory Infinite_Set_Sum
imports Set_Integral Infinite_Sum
begin
text ‹Conflicting notation from \<^theory>‹HOL-Analysis.Infinite_Sum››
no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
lemma sets_eq_countable:
assumes "countable A" "space M = A" "⋀x. x ∈ A ⟹ {x} ∈ sets M"
shows "sets M = Pow A"
proof (intro equalityI subsetI)
fix X assume "X ∈ Pow A"
hence "(⋃x∈X. {x}) ∈ sets M"
by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3))
also have "(⋃x∈X. {x}) = X" by auto
finally show "X ∈ sets M" .
next
fix X assume "X ∈ sets M"
from sets.sets_into_space[OF this] and assms
show "X ∈ Pow A" by simp
qed
lemma measure_eqI_countable':
assumes spaces: "space M = A" "space N = A"
assumes sets: "⋀x. x ∈ A ⟹ {x} ∈ sets M" "⋀x. x ∈ A ⟹ {x} ∈ sets N"
assumes A: "countable A"
assumes eq: "⋀a. a ∈ A ⟹ emeasure M {a} = emeasure N {a}"
shows "M = N"
proof (rule measure_eqI_countable)
show "sets M = Pow A"
by (intro sets_eq_countable assms)
show "sets N = Pow A"
by (intro sets_eq_countable assms)
qed fact+
lemma count_space_PiM_finite:
fixes B :: "'a ⇒ 'b set"
assumes "finite A" "⋀i. countable (B i)"
shows "PiM A (λi. count_space (B i)) = count_space (PiE A B)"
proof (rule measure_eqI_countable')
show "space (PiM A (λi. count_space (B i))) = PiE A B"
by (simp add: space_PiM)
show "space (count_space (PiE A B)) = PiE A B" by simp
next
fix f assume f: "f ∈ PiE A B"
hence "PiE A (λx. {f x}) ∈ sets (Pi⇩M A (λi. count_space (B i)))"
by (intro sets_PiM_I_finite assms) auto
also from f have "PiE A (λx. {f x}) = {f}"
by (intro PiE_singleton) (auto simp: PiE_def)
finally show "{f} ∈ sets (Pi⇩M A (λi. count_space (B i)))" .
next
interpret product_sigma_finite "(λi. count_space (B i))"
by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms)
thm sigma_finite_measure_count_space
fix f assume f: "f ∈ PiE A B"
hence "{f} = PiE A (λx. {f x})"
by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
also have "emeasure (Pi⇩M A (λi. count_space (B i))) … =
(∏i∈A. emeasure (count_space (B i)) {f i})"
using f assms by (subst emeasure_PiM) auto
also have "… = (∏i∈A. 1)"
by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto)
also have "… = emeasure (count_space (PiE A B)) {f}"
using f by (subst emeasure_count_space_finite) auto
finally show "emeasure (Pi⇩M A (λi. count_space (B i))) {f} =
emeasure (count_space (Pi⇩E A B)) {f}" .
qed (simp_all add: countable_PiE assms)
definition abs_summable_on ::
"('a ⇒ 'b :: {banach, second_countable_topology}) ⇒ 'a set ⇒ bool"
(infix "abs'_summable'_on" 50)
where
"f abs_summable_on A ⟷ integrable (count_space A) f"
definition infsetsum ::
"('a ⇒ 'b :: {banach, second_countable_topology}) ⇒ 'a set ⇒ 'b"
where
"infsetsum f A = lebesgue_integral (count_space A) f"
syntax (ASCII)
"_infsetsum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::{banach, second_countable_topology}"
("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
syntax
"_infsetsum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::{banach, second_countable_topology}"
("(2∑⇩a_∈_./ _)" [0, 51, 10] 10)
translations
"∑⇩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∑⇩a_./ _)" [0, 10] 10)
translations
"∑⇩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
"_qinfsetsum" :: "pttrn ⇒ bool ⇒ 'a ⇒ 'a::{banach, second_countable_topology}"
("(2∑⇩a_ | (_)./ _)" [0, 0, 10] 10)
translations
"∑⇩ax|P. t" => "CONST infsetsum (λx. t) {x. P}"
print_translation ‹
let
fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>‹Collect›, _) $ Abs (y, Ty, P)] =
if x <> y then raise Match
else
let
val x' = Syntax_Trans.mark_bound_body (x, Tx);
val t' = subst_bound (x', t);
val P' = subst_bound (x', P);
in
Syntax.const \<^syntax_const>‹_qinfsetsum› $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
end
| sum_tr' _ = raise Match;
in [(\<^const_syntax>‹infsetsum›, K sum_tr')] end
›
lemma restrict_count_space_subset:
"A ⊆ B ⟹ restrict_space (count_space B) A = count_space A"
by (subst restrict_count_space) (simp_all add: Int_absorb2)
lemma abs_summable_on_restrict:
fixes f :: "'a ⇒ 'b :: {banach, second_countable_topology}"
assumes "A ⊆ B"
shows "f abs_summable_on A ⟷ (λx. indicator A x *⇩R f x) abs_summable_on B"
proof -
have "count_space A = restrict_space (count_space B) A"
by (rule restrict_count_space_subset [symmetric]) fact+
also have "integrable … f ⟷ set_integrable (count_space B) A f"
by (simp add: integrable_restrict_space set_integrable_def)
finally show ?thesis
unfolding abs_summable_on_def set_integrable_def .
qed
lemma abs_summable_on_altdef: "f abs_summable_on A ⟷ set_integrable (count_space UNIV) A f"
unfolding abs_summable_on_def set_integrable_def
by (metis (no_types) inf_top.right_neutral integrable_restrict_space restrict_count_space sets_UNIV)
lemma abs_summable_on_altdef':
"A ⊆ B ⟹ f abs_summable_on A ⟷ set_integrable (count_space B) A f"
unfolding abs_summable_on_def set_integrable_def
by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset sets_count_space space_count_space)
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_complex_of_real [simp]: "(λn. complex_of_real (f n)) abs_summable_on A ⟷ f abs_summable_on A"
by (simp add: abs_summable_on_def complex_of_real_integrable_eq)
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
lemma abs_summable_on_cong_neutral:
assumes "⋀x. x ∈ A - B ⟹ f x = 0"
assumes "⋀x. x ∈ B - A ⟹ g x = 0"
assumes "⋀x. x ∈ A ∩ B ⟹ f x = g x"
shows "f abs_summable_on A ⟷ g abs_summable_on B"
unfolding abs_summable_on_altdef set_integrable_def using assms
by (intro Bochner_Integration.integrable_cong refl)
(auto simp: indicator_def split: if_splits)
lemma abs_summable_on_restrict':
fixes f :: "'a ⇒ 'b :: {banach, second_countable_topology}"
assumes "A ⊆ B"
shows "f abs_summable_on A ⟷ (λx. if x ∈ A then f x else 0) abs_summable_on B"
by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto)
lemma abs_summable_on_nat_iff:
"f abs_summable_on (A :: nat set) ⟷ summable (λn. if n ∈ A then norm (f n) else 0)"
proof -
have "f abs_summable_on A ⟷ summable (λx. norm (if x ∈ A then f x else 0))"
by (subst abs_summable_on_restrict'[of _ UNIV])
(simp_all add: abs_summable_on_def integrable_count_space_nat_iff)
also have "(λx. norm (if x ∈ A then f x else 0)) = (λx. if x ∈ A then norm (f x) else 0)"
by auto
finally show ?thesis .
qed
lemma abs_summable_on_nat_iff':
"f abs_summable_on (UNIV :: nat set) ⟷ summable (λn. norm (f n))"
by (subst abs_summable_on_nat_iff) auto
lemma nat_abs_summable_on_comparison_test:
fixes f :: "nat ⇒ 'a :: {banach, second_countable_topology}"
assumes "g abs_summable_on I"
assumes "⋀n. ⟦n≥N; n ∈ I⟧ ⟹ norm (f n) ≤ g n"
shows "f abs_summable_on I"
using assms by (fastforce simp add: abs_summable_on_nat_iff intro: summable_comparison_test')
lemma abs_summable_comparison_test_ev:
assumes "g abs_summable_on I"
assumes "eventually (λx. x ∈ I ⟶ norm (f x) ≤ g x) sequentially"
shows "f abs_summable_on I"
by (metis (no_types, lifting) nat_abs_summable_on_comparison_test eventually_at_top_linorder assms)
lemma abs_summable_on_Cauchy:
"f abs_summable_on (UNIV :: nat set) ⟷ (∀e>0. ∃N. ∀m≥N. ∀n. (∑x = m..<n. norm (f x)) < e)"
by (simp add: abs_summable_on_nat_iff' summable_Cauchy sum_nonneg)
lemma abs_summable_on_finite [simp]: "finite A ⟹ f abs_summable_on A"
unfolding abs_summable_on_def by (rule integrable_count_space)
lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}"
by simp
lemma abs_summable_on_subset:
assumes "f abs_summable_on B" and "A ⊆ B"
shows "f abs_summable_on A"
unfolding abs_summable_on_altdef
by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef)
lemma abs_summable_on_union [intro]:
assumes "f abs_summable_on A" and "f abs_summable_on B"
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_sum:
assumes "⋀x. x ∈ A ⟹ f x abs_summable_on B"
shows "(λy. ∑x∈A. f x y) abs_summable_on B"
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)
lemma abs_summable_Re: "f abs_summable_on A ⟹ (λx. Re (f x)) abs_summable_on A"
by (simp add: abs_summable_on_def)
lemma abs_summable_Im: "f abs_summable_on A ⟹ (λx. Im (f x)) abs_summable_on A"
by (simp add: abs_summable_on_def)
lemma abs_summable_on_finite_diff:
assumes "f abs_summable_on A" "A ⊆ B" "finite (B - A)"
shows "f abs_summable_on B"
proof -
have "f abs_summable_on (A ∪ (B - A))"
by (intro abs_summable_on_union assms abs_summable_on_finite)
also from assms have "A ∪ (B - A) = B" by blast
finally show ?thesis .
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"
proof -
have *: "count_space B = distr (count_space A) (count_space B) g"
by (rule distr_bij_count_space [symmetric]) fact
show ?thesis unfolding abs_summable_on_def
by (subst *, subst integrable_distr_eq[of _ _ "count_space B"])
(insert assms, auto simp: bij_betw_def)
qed
lemma abs_summable_on_reindex:
assumes "(λx. f (g x)) abs_summable_on A"
shows "f abs_summable_on (g ` A)"
proof -
define g' where "g' = inv_into A g"
from assms have "(λx. f (g x)) abs_summable_on (g' ` g ` A)"
by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into)
also have "?this ⟷ (λx. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def
by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto
also have "… ⟷ f abs_summable_on (g ` A)"
by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f)
finally show ?thesis .
qed
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_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)"
proof -
from assms(2) have "f abs_summable_on (Sigma {x} B)"
by (intro abs_summable_on_subset [OF assms(1)]) auto
also have "?this ⟷ (λz. f (x, snd z)) abs_summable_on (Sigma {x} B)"
by (rule abs_summable_on_cong) auto
finally have "(λy. f (x, y)) abs_summable_on (snd ` Sigma {x} B)"
by (rule abs_summable_on_reindex)
also have "snd ` Sigma {x} B = B x"
using assms by (auto simp: image_iff)
finally show ?thesis .
qed
lemma abs_summable_on_Times_swap:
"f abs_summable_on A × B ⟷ (λ(x,y). f (y,x)) abs_summable_on B × A"
proof -
have bij: "bij_betw (λ(x,y). (y,x)) (B × A) (A × B)"
by (auto simp: bij_betw_def inj_on_def)
show ?thesis
by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric])
(simp_all add: case_prod_unfold)
qed
lemma abs_summable_on_0 [simp, intro]: "(λ_. 0) abs_summable_on A"
by (simp add: abs_summable_on_def)
lemma abs_summable_on_uminus [intro]:
"f abs_summable_on A ⟹ (λx. -f x) abs_summable_on A"
unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus)
lemma abs_summable_on_add [intro]:
assumes "f abs_summable_on A" and "g abs_summable_on A"
shows "(λx. f x + g x) abs_summable_on A"
using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add)
lemma abs_summable_on_diff [intro]:
assumes "f abs_summable_on A" and "g abs_summable_on A"
shows "(λx. f x - g x) abs_summable_on A"
using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff)
lemma abs_summable_on_scaleR_left [intro]:
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "(λx. f x *⇩R c) abs_summable_on A"
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left)
lemma abs_summable_on_scaleR_right [intro]:
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "(λx. c *⇩R f x) abs_summable_on A"
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right)
lemma abs_summable_on_cmult_right [intro]:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_algebra, second_countable_topology}"
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "(λx. c * f x) abs_summable_on A"
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right)
lemma abs_summable_on_cmult_left [intro]:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_algebra, second_countable_topology}"
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "(λx. f x * c) abs_summable_on A"
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)
lemma abs_summable_on_prod_PiE:
fixes f :: "'a ⇒ 'b ⇒ 'c :: {real_normed_field,banach,second_countable_topology}"
assumes finite: "finite A" and countable: "⋀x. x ∈ A ⟹ countable (B x)"
assumes summable: "⋀x. x ∈ A ⟹ f x abs_summable_on B x"
shows "(λg. ∏x∈A. f x (g x)) abs_summable_on PiE A B"
proof -
define B' where "B' = (λx. if x ∈ A then B x else {})"
from assms have [simp]: "countable (B' x)" for x
by (auto simp: B'_def)
then interpret product_sigma_finite "count_space ∘ B'"
unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
from assms have "integrable (PiM A (count_space ∘ B')) (λg. ∏x∈A. f x (g x))"
by (intro product_integrable_prod) (auto simp: abs_summable_on_def B'_def)
also have "PiM A (count_space ∘ B') = count_space (PiE A B')"
unfolding o_def using finite by (intro count_space_PiM_finite) simp_all
also have "PiE A B' = PiE A B" by (intro PiE_cong) (simp_all add: B'_def)
finally show ?thesis by (simp add: abs_summable_on_def)
qed
lemma not_summable_infsetsum_eq:
"¬f abs_summable_on A ⟹ infsetsum f A = 0"
by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq)
lemma infsetsum_altdef:
"infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
unfolding set_lebesgue_integral_def
by (subst integral_restrict_space [symmetric])
(auto simp: restrict_count_space_subset infsetsum_def)
lemma infsetsum_altdef':
"A ⊆ B ⟹ infsetsum f A = set_lebesgue_integral (count_space B) A f"
unfolding set_lebesgue_integral_def
by (subst integral_restrict_space [symmetric])
(auto simp: restrict_count_space_subset infsetsum_def)
lemma nn_integral_conv_infsetsum:
assumes "f abs_summable_on A" "⋀x. x ∈ A ⟹ f x ≥ 0"
shows "nn_integral (count_space A) f = ennreal (infsetsum f A)"
using assms unfolding infsetsum_def abs_summable_on_def
by (subst nn_integral_eq_integral) auto
lemma infsetsum_conv_nn_integral:
assumes "nn_integral (count_space A) f ≠ ∞" "⋀x. x ∈ A ⟹ f x ≥ 0"
shows "infsetsum f A = enn2real (nn_integral (count_space A) f)"
unfolding infsetsum_def using assms
by (subst integral_eq_nn_integral) auto
lemma infsetsum_cong [cong]:
"(⋀x. x ∈ A ⟹ f x = g x) ⟹ A = B ⟹ infsetsum f A = infsetsum g B"
unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto
lemma infsetsum_0 [simp]: "infsetsum (λ_. 0) A = 0"
by (simp add: infsetsum_def)
lemma infsetsum_all_0: "(⋀x. x ∈ A ⟹ f x = 0) ⟹ infsetsum f A = 0"
by simp
lemma infsetsum_nonneg: "(⋀x. x ∈ A ⟹ f x ≥ (0::real)) ⟹ infsetsum f A ≥ 0"
unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto
lemma sum_infsetsum:
assumes "⋀x. x ∈ A ⟹ f x abs_summable_on B"
shows "(∑x∈A. ∑⇩ay∈B. f x y) = (∑⇩ay∈B. ∑x∈A. f x y)"
using assms by (simp add: infsetsum_def abs_summable_on_def Bochner_Integration.integral_sum)
lemma Re_infsetsum: "f abs_summable_on A ⟹ Re (infsetsum f A) = (∑⇩ax∈A. Re (f x))"
by (simp add: infsetsum_def abs_summable_on_def)
lemma Im_infsetsum: "f abs_summable_on A ⟹ Im (infsetsum f A) = (∑⇩ax∈A. Im (f x))"
by (simp add: infsetsum_def abs_summable_on_def)
lemma infsetsum_of_real:
shows "infsetsum (λx. of_real (f x)
:: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A =
of_real (infsetsum f A)"
unfolding infsetsum_def
by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto
lemma infsetsum_finite [simp]: "finite A ⟹ infsetsum f A = (∑x∈A. f x)"
by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
lemma infsetsum_nat:
assumes "f abs_summable_on A"
shows "infsetsum f A = (∑n. if n ∈ A then f n else 0)"
proof -
from assms have "infsetsum f A = (∑n. indicator A n *⇩R f n)"
unfolding infsetsum_altdef abs_summable_on_altdef set_lebesgue_integral_def set_integrable_def
by (subst integral_count_space_nat) auto
also have "(λn. indicator A n *⇩R f n) = (λn. if n ∈ A then f n else 0)"
by auto
finally show ?thesis .
qed
lemma infsetsum_nat':
assumes "f abs_summable_on UNIV"
shows "infsetsum f UNIV = (∑n. f n)"
using assms by (subst infsetsum_nat) auto
lemma sums_infsetsum_nat:
assumes "f abs_summable_on A"
shows "(λn. if n ∈ A then f n else 0) sums infsetsum f A"
proof -
from assms have "summable (λn. if n ∈ A then norm (f n) else 0)"
by (simp add: abs_summable_on_nat_iff)
also have "(λn. if n ∈ A then norm (f n) else 0) = (λn. norm (if n ∈ A then f n else 0))"
by auto
finally have "summable (λn. if n ∈ A then f n else 0)"
by (rule summable_norm_cancel)
with assms show ?thesis
by (auto simp: sums_iff infsetsum_nat)
qed
lemma sums_infsetsum_nat':
assumes "f abs_summable_on UNIV"
shows "f sums infsetsum f UNIV"
using sums_infsetsum_nat [OF assms] by simp
lemma infsetsum_Un_disjoint:
assumes "f abs_summable_on A" "f abs_summable_on B" "A ∩ B = {}"
shows "infsetsum f (A ∪ B) = infsetsum f A + infsetsum f B"
using assms unfolding infsetsum_altdef abs_summable_on_altdef
by (subst set_integral_Un) auto
lemma infsetsum_Diff:
assumes "f abs_summable_on B" "A ⊆ B"
shows "infsetsum f (B - A) = infsetsum f B - infsetsum f A"
proof -
have "infsetsum f ((B - A) ∪ A) = infsetsum f (B - A) + infsetsum f A"
using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto
also from assms(2) have "(B - A) ∪ A = B"
by auto
ultimately show ?thesis
by (simp add: algebra_simps)
qed
lemma infsetsum_Un_Int:
assumes "f abs_summable_on (A ∪ B)"
shows "infsetsum f (A ∪ B) = infsetsum f A + infsetsum f B - infsetsum f (A ∩ B)"
proof -
have "A ∪ B = A ∪ (B - A ∩ B)"
by auto
also have "infsetsum f … = infsetsum f A + infsetsum f (B - A ∩ B)"
by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto
also have "infsetsum f (B - A ∩ B) = infsetsum f B - infsetsum f (A ∩ B)"
by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto
finally show ?thesis
by (simp add: algebra_simps)
qed
lemma infsetsum_reindex_bij_betw:
assumes "bij_betw g A B"
shows "infsetsum (λx. f (g x)) A = infsetsum f B"
proof -
have *: "count_space B = distr (count_space A) (count_space B) g"
by (rule distr_bij_count_space [symmetric]) fact
show ?thesis unfolding infsetsum_def
by (subst *, subst integral_distr[of _ _ "count_space B"])
(insert assms, auto simp: bij_betw_def)
qed
theorem infsetsum_reindex:
assumes "inj_on g A"
shows "infsetsum f (g ` A) = infsetsum (λx. f (g x)) A"
by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
lemma infsetsum_cong_neutral:
assumes "⋀x. x ∈ A - B ⟹ f x = 0"
assumes "⋀x. x ∈ B - A ⟹ g x = 0"
assumes "⋀x. x ∈ A ∩ B ⟹ f x = g x"
shows "infsetsum f A = infsetsum g B"
unfolding infsetsum_altdef set_lebesgue_integral_def using assms
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 set_lebesgue_integral_def abs_summable_on_altdef set_integrable_def
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 ≤ infsetsum g B"
using ‹A ⊆ B› by (intro infsetsum_mono_neutral assms) auto
lemma infsetsum_mono_neutral_right:
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 "B ⊆ A"
assumes "⋀x. x ∈ A - B ⟹ f x ≤ 0"
shows "infsetsum f A ≤ infsetsum g B"
using ‹B ⊆ A› by (intro infsetsum_mono_neutral assms) auto
lemma infsetsum_mono:
fixes f g :: "'a ⇒ real"
assumes "f abs_summable_on A" and "g abs_summable_on A"
assumes "⋀x. x ∈ A ⟹ f x ≤ g x"
shows "infsetsum f A ≤ infsetsum g A"
by (intro infsetsum_mono_neutral assms) auto
lemma norm_infsetsum_bound:
"norm (infsetsum f A) ≤ infsetsum (λx. norm (f x)) A"
unfolding abs_summable_on_def infsetsum_def
by (rule Bochner_Integration.integral_norm_bound)
theorem infsetsum_Sigma:
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
assumes [simp]: "countable A" and "⋀i. countable (B i)"
assumes summable: "f abs_summable_on (Sigma A B)"
shows "infsetsum f (Sigma A B) = infsetsum (λx. infsetsum (λy. f (x, y)) (B x)) A"
proof -
define B' where "B' = (⋃i∈A. B i)"
have [simp]: "countable B'"
unfolding B'_def by (intro countable_UN assms)
interpret pair_sigma_finite "count_space A" "count_space B'"
by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
have "integrable (count_space (A × B')) (λz. indicator (Sigma A B) z *⇩R f z)"
using summable
by (metis (mono_tags, lifting) abs_summable_on_altdef abs_summable_on_def integrable_cong integrable_mult_indicator set_integrable_def sets_UNIV)
also have "?this ⟷ integrable (count_space A ⨂⇩M count_space B') (λ(x, y). indicator (B x) y *⇩R f (x, y))"
by (intro Bochner_Integration.integrable_cong)
(auto simp: pair_measure_countable indicator_def split: if_splits)
finally have integrable: … .
have "infsetsum (λx. infsetsum (λy. f (x, y)) (B x)) A =
(∫x. infsetsum (λy. f (x, y)) (B x) ∂count_space A)"
unfolding infsetsum_def by simp
also have "… = (∫x. ∫y. indicator (B x) y *⇩R f (x, y) ∂count_space B' ∂count_space A)"
proof (rule Bochner_Integration.integral_cong [OF refl])
show "⋀x. x ∈ space (count_space A) ⟹
(∑⇩ay∈B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *⇩R f (x, y)"
using infsetsum_altdef'[of _ B']
unfolding set_lebesgue_integral_def B'_def
by auto
qed
also have "… = (∫(x,y). indicator (B x) y *⇩R f (x, y) ∂(count_space A ⨂⇩M count_space B'))"
by (subst integral_fst [OF integrable]) auto
also have "… = (∫z. indicator (Sigma A B) z *⇩R f z ∂count_space (A × B'))"
by (intro Bochner_Integration.integral_cong)
(auto simp: pair_measure_countable indicator_def split: if_splits)
also have "… = infsetsum f (Sigma A B)"
unfolding set_lebesgue_integral_def [symmetric]
by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
finally show ?thesis ..
qed
lemma infsetsum_Sigma':
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
assumes [simp]: "countable A" and "⋀i. countable (B i)"
assumes summable: "(λ(x,y). f x y) abs_summable_on (Sigma A B)"
shows "infsetsum (λx. infsetsum (λy. f x y) (B x)) A = infsetsum (λ(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"
assumes summable: "f abs_summable_on (A × B)"
shows "infsetsum f (A × B) = infsetsum (λx. infsetsum (λy. f (x, y)) B) A"
using assms by (subst infsetsum_Sigma) auto
lemma infsetsum_Times':
fixes A :: "'a set" and B :: "'b set"
fixes f :: "'a ⇒ 'b ⇒ 'c :: {banach, second_countable_topology}"
assumes [simp]: "countable A" and [simp]: "countable B"
assumes summable: "(λ(x,y). f x y) abs_summable_on (A × B)"
shows "infsetsum (λx. infsetsum (λy. f x y) B) A = infsetsum (λ(x,y). f x y) (A × B)"
using assms by (subst infsetsum_Times) auto
lemma infsetsum_swap:
fixes A :: "'a set" and B :: "'b set"
fixes f :: "'a ⇒ 'b ⇒ 'c :: {banach, second_countable_topology}"
assumes [simp]: "countable A" and [simp]: "countable B"
assumes summable: "(λ(x,y). f x y) abs_summable_on A × B"
shows "infsetsum (λx. infsetsum (λy. f x y) B) A = infsetsum (λy. infsetsum (λx. f x y) A) B"
proof -
from summable have summable': "(λ(x,y). f y x) abs_summable_on B × A"
by (subst abs_summable_on_Times_swap) auto
have bij: "bij_betw (λ(x, y). (y, x)) (B × A) (A × B)"
by (auto simp: bij_betw_def inj_on_def)
have "infsetsum (λx. infsetsum (λy. f x y) B) A = infsetsum (λ(x,y). f x y) (A × B)"
using summable by (subst infsetsum_Times) auto
also have "… = infsetsum (λ(x,y). f y x) (B × A)"
by (subst infsetsum_reindex_bij_betw[OF bij, of "λ(x,y). f x y", symmetric])
(simp_all add: case_prod_unfold)
also have "… = infsetsum (λy. infsetsum (λx. f x y) A) B"
using summable' by (subst infsetsum_Times) auto
finally show ?thesis .
qed
theorem abs_summable_on_Sigma_iff:
assumes [simp]: "countable A" and "⋀x. x ∈ A ⟹ countable (B x)"
shows "f abs_summable_on Sigma A B ⟷
(∀x∈A. (λy. f (x, y)) abs_summable_on B x) ∧
((λx. infsetsum (λy. norm (f (x, y))) (B x)) abs_summable_on A)"
proof safe
define B' where "B' = (⋃x∈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 "(λy. f (x, y)) abs_summable_on B x" if "x ∈ A" for x
using that by (rule abs_summable_on_Sigma_project2)
have "set_integrable (count_space (A × B')) (Sigma A B) (λ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 × B') = count_space A ⨂⇩M count_space B'"
by (simp add: pair_measure_countable)
finally have "integrable (count_space A)
(λx. lebesgue_integral (count_space B')
(λy. indicator (Sigma A B) (x, y) *⇩R norm (f (x, y))))"
unfolding set_integrable_def by (rule integrable_fst')
also have "?this ⟷ integrable (count_space A)
(λx. lebesgue_integral (count_space B')
(λy. indicator (B x) y *⇩R norm (f (x, y))))"
by (intro integrable_cong refl) (simp_all add: indicator_def)
also have "… ⟷ integrable (count_space A) (λx. infsetsum (λy. norm (f (x, y))) (B x))"
unfolding set_lebesgue_integral_def [symmetric]
by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
also have "… ⟷ (λx. infsetsum (λy. norm (f (x, y))) (B x)) abs_summable_on A"
by (simp add: abs_summable_on_def)
finally show … .
}
{
assume *: "∀x∈A. (λy. f (x, y)) abs_summable_on B x"
assume "(λx. ∑⇩ay∈B x. norm (f (x, y))) abs_summable_on A"
also have "?this ⟷ (λx. ∫y∈B x. norm (f (x, y)) ∂count_space B') abs_summable_on A"
by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
also have "… ⟷ (λx. ∫y. indicator (Sigma A B) (x, y) *⇩R norm (f (x, y)) ∂count_space B')
abs_summable_on A" (is "_ ⟷ ?h abs_summable_on _")
unfolding set_lebesgue_integral_def
by (intro abs_summable_on_cong) (auto simp: indicator_def)
also have "… ⟷ integrable (count_space A) ?h"
by (simp add: abs_summable_on_def)
finally have **: … .
have "integrable (count_space A ⨂⇩M count_space B') (λz. indicator (Sigma A B) z *⇩R f z)"
proof (rule Fubini_integrable, goal_cases)
case 3
{
fix x assume x: "x ∈ A"
with * have "(λy. f (x, y)) abs_summable_on B x"
by blast
also have "?this ⟷ integrable (count_space B')
(λy. indicator (B x) y *⇩R f (x, y))"
unfolding set_integrable_def [symmetric]
using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
also have "(λy. indicator (B x) y *⇩R f (x, y)) =
(λy. indicator (Sigma A B) (x, y) *⇩R f (x, y))"
using x by (auto simp: indicator_def)
finally have "integrable (count_space B')
(λy. indicator (Sigma A B) (x, y) *⇩R f (x, y))" .
}
thus ?case by (auto simp: AE_count_space)
qed (insert **, auto simp: pair_measure_countable)
moreover have "count_space A ⨂⇩M count_space B' = count_space (A × B')"
by (simp add: pair_measure_countable)
moreover have "set_integrable (count_space (A × B')) (Sigma A B) f ⟷
f abs_summable_on Sigma A B"
by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
ultimately show "f abs_summable_on Sigma A B"
by (simp add: set_integrable_def)
}
qed
lemma abs_summable_on_Sigma_project1:
assumes "(λ(x,y). f x y) abs_summable_on Sigma A B"
assumes [simp]: "countable A" and "⋀x. x ∈ A ⟹ countable (B x)"
shows "(λx. infsetsum (λ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 "(λ(x,y). f x y) abs_summable_on Sigma A B"
assumes [simp]: "countable A" and "⋀x. x ∈ A ⟹ countable (B x)"
shows "(λx. infsetsum (λ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)
theorem infsetsum_prod_PiE:
fixes f :: "'a ⇒ 'b ⇒ 'c :: {real_normed_field,banach,second_countable_topology}"
assumes finite: "finite A" and countable: "⋀x. x ∈ A ⟹ countable (B x)"
assumes summable: "⋀x. x ∈ A ⟹ f x abs_summable_on B x"
shows "infsetsum (λg. ∏x∈A. f x (g x)) (PiE A B) = (∏x∈A. infsetsum (f x) (B x))"
proof -
define B' where "B' = (λx. if x ∈ A then B x else {})"
from assms have [simp]: "countable (B' x)" for x
by (auto simp: B'_def)
then interpret product_sigma_finite "count_space ∘ B'"
unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
have "infsetsum (λg. ∏x∈A. f x (g x)) (PiE A B) =
(∫g. (∏x∈A. f x (g x)) ∂count_space (PiE A B))"
by (simp add: infsetsum_def)
also have "PiE A B = PiE A B'"
by (intro PiE_cong) (simp_all add: B'_def)
hence "count_space (PiE A B) = count_space (PiE A B')"
by simp
also have "… = PiM A (count_space ∘ B')"
unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
also have "(∫g. (∏x∈A. f x (g x)) ∂…) = (∏x∈A. infsetsum (f x) (B' x))"
by (subst product_integral_prod)
(insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def)
also have "… = (∏x∈A. infsetsum (f x) (B x))"
by (intro prod.cong refl) (simp_all add: B'_def)
finally show ?thesis .
qed
lemma infsetsum_uminus: "infsetsum (λx. -f x) A = -infsetsum f A"
unfolding infsetsum_def abs_summable_on_def
by (rule Bochner_Integration.integral_minus)
lemma infsetsum_add:
assumes "f abs_summable_on A" and "g abs_summable_on A"
shows "infsetsum (λx. f x + g x) A = infsetsum f A + infsetsum g A"
using assms unfolding infsetsum_def abs_summable_on_def
by (rule Bochner_Integration.integral_add)
lemma infsetsum_diff:
assumes "f abs_summable_on A" and "g abs_summable_on A"
shows "infsetsum (λx. f x - g x) A = infsetsum f A - infsetsum g A"
using assms unfolding infsetsum_def abs_summable_on_def
by (rule Bochner_Integration.integral_diff)
lemma infsetsum_scaleR_left:
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "infsetsum (λx. f x *⇩R c) A = infsetsum f A *⇩R c"
using assms unfolding infsetsum_def abs_summable_on_def
by (rule Bochner_Integration.integral_scaleR_left)
lemma infsetsum_scaleR_right:
"infsetsum (λx. c *⇩R f x) A = c *⇩R infsetsum f A"
unfolding infsetsum_def abs_summable_on_def
by (subst Bochner_Integration.integral_scaleR_right) auto
lemma infsetsum_cmult_left:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_algebra, second_countable_topology}"
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "infsetsum (λx. f x * c) A = infsetsum f A * c"
using assms unfolding infsetsum_def abs_summable_on_def
by (rule Bochner_Integration.integral_mult_left)
lemma infsetsum_cmult_right:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_algebra, second_countable_topology}"
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "infsetsum (λx. c * f x) A = c * infsetsum f A"
using assms unfolding infsetsum_def abs_summable_on_def
by (rule Bochner_Integration.integral_mult_right)
lemma infsetsum_cdiv:
fixes f :: "'a ⇒ 'b :: {banach, real_normed_field, second_countable_topology}"
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows "infsetsum (λx. f x / c) A = infsetsum f A / c"
using assms unfolding infsetsum_def abs_summable_on_def by auto
lemma
fixes f :: "'a ⇒ '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: "(λ(x,y). f x * g y) abs_summable_on A × B"
and infsetsum_product: "infsetsum (λ(x,y). f x * g y) (A × B) =
infsetsum f A * infsetsum g B"
proof -
from assms show "(λ(x,y). f x * g y) abs_summable_on A × 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 (λ(x,y). f x * g y) (A × B) = infsetsum f A * infsetsum g B"
by (subst infsetsum_Sigma)
(auto simp: infsetsum_cmult_left infsetsum_cmult_right)
qed
lemma abs_summable_finite_sumsI:
assumes "⋀F. finite F ⟹ F⊆S ⟹ sum (λx. norm (f x)) F ≤ B"
shows "f abs_summable_on S"
proof -
have main: "f abs_summable_on S ∧ infsetsum (λx. norm (f x)) S ≤ B" if ‹B ≥ 0› and ‹S ≠ {}›
proof -
define M normf where "M = count_space S" and "normf x = ennreal (norm (f x))" for x
have "sum normf F ≤ ennreal B"
if "finite F" and "F ⊆ S" and
"⋀F. finite F ⟹ F ⊆ S ⟹ (∑i∈F. ennreal (norm (f i))) ≤ ennreal B" and
"ennreal 0 ≤ ennreal B" for F
using that unfolding normf_def[symmetric] by simp
hence normf_B: "finite F ⟹ F⊆S ⟹ sum normf F ≤ ennreal B" for F
using assms[THEN ennreal_leI]
by auto
have "integral⇧S M g ≤ B" if "simple_function M g" and "g ≤ normf" for g
proof -
define gS where "gS = g ` S"
have "finite gS"
using that unfolding gS_def M_def simple_function_count_space by simp
have "gS ≠ {}" unfolding gS_def using ‹S ≠ {}› by auto
define part where "part r = g -` {r} ∩ S" for r
have r_finite: "r < ∞" if "r : gS" for r
using ‹g ≤ normf› that unfolding gS_def le_fun_def normf_def apply auto
using ennreal_less_top neq_top_trans top.not_eq_extremum by blast
define B' where "B' r = (SUP F∈{F. finite F ∧ F⊆part r}. sum normf F)" for r
have B'fin: "B' r < ∞" for r
proof -
have "B' r ≤ (SUP F∈{F. finite F ∧ F⊆part r}. sum normf F)"
unfolding B'_def
by (metis (mono_tags, lifting) SUP_least SUP_upper)
also have "… ≤ B"
using normf_B unfolding part_def
by (metis (no_types, lifting) Int_subset_iff SUP_least mem_Collect_eq)
also have "… < ∞"
by simp
finally show ?thesis by simp
qed
have sumB': "sum B' gS ≤ ennreal B + ε" if "ε>0" for ε
proof -
define N εN where "N = card gS" and "εN = ε / N"
have "N > 0"
unfolding N_def using ‹gS≠{}› ‹finite gS›
by (simp add: card_gt_0_iff)
from εN_def that have "εN > 0"
by (simp add: ennreal_of_nat_eq_real_of_nat ennreal_zero_less_divide)
have c1: "∃y. B' r ≤ sum normf y + εN ∧ finite y ∧ y ⊆ part r"
if "B' r = 0" for r
using that by auto
have c2: "∃y. B' r ≤ sum normf y + εN ∧ finite y ∧ y ⊆ part r" if "B' r ≠ 0" for r
proof-
have "B' r - εN < B' r"
using B'fin ‹0 < εN› ennreal_between that by fastforce
have "B' r - εN < Sup (sum normf ` {F. finite F ∧ F ⊆ part r}) ⟹
∃F. B' r - εN ≤ sum normf F ∧ finite F ∧ F ⊆ part r"
by (metis (no_types, lifting) leD le_cases less_SUP_iff mem_Collect_eq)
hence "B' r - εN < B' r ⟹ ∃F. B' r - εN ≤ sum normf F ∧ finite F ∧ F ⊆ part r"
by (subst (asm) (2) B'_def)
then obtain F where "B' r - εN ≤ sum normf F" and "finite F" and "F ⊆ part r"
using ‹B' r - εN < B' r› by auto
thus "∃F. B' r ≤ sum normf F + εN ∧ finite F ∧ F ⊆ part r"
by (metis add.commute ennreal_minus_le_iff)
qed
have "∀x. ∃y. B' x ≤ sum normf y + εN ∧
finite y ∧ y ⊆ part x"
using c1 c2
by blast
hence "∃F. ∀x. B' x ≤ sum normf (F x) + εN ∧ finite (F x) ∧ F x ⊆ part x"
by metis
then obtain F where F: "sum normf (F r) + εN ≥ B' r" and Ffin: "finite (F r)" and Fpartr: "F r ⊆ part r" for r
using atomize_elim by auto
have w1: "finite gS"
by (simp add: ‹finite gS›)
have w2: "∀i∈gS. finite (F i)"
by (simp add: Ffin)
have False
if "⋀r. F r ⊆ g -` {r} ∧ F r ⊆ S"
and "i ∈ gS" and "j ∈ gS" and "i ≠ j" and "x ∈ F i" and "x ∈ F j"
for i j x
by (metis subsetD that(1) that(4) that(5) that(6) vimage_singleton_eq)
hence w3: "∀i∈gS. ∀j∈gS. i ≠ j ⟶ F i ∩ F j = {}"
using Fpartr[unfolded part_def] by auto
have w4: "sum normf (⋃ (F ` gS)) + ε = sum normf (⋃ (F ` gS)) + ε"
by simp
have "sum B' gS ≤ (∑r∈gS. sum normf (F r) + εN)"
using F by (simp add: sum_mono)
also have "… = (∑r∈gS. sum normf (F r)) + (∑r∈gS. εN)"
by (simp add: sum.distrib)
also have "… = (∑r∈gS. sum normf (F r)) + (card gS * εN)"
by auto
also have "… = (∑r∈gS. sum normf (F r)) + ε"
unfolding εN_def N_def[symmetric] using ‹N>0›
by (simp add: ennreal_times_divide mult.commute mult_divide_eq_ennreal)
also have "… = sum normf (⋃ (F ` gS)) + ε"
using w1 w2 w3 w4
by (subst sum.UNION_disjoint[symmetric])
also have "… ≤ B + ε"
using ‹finite gS› normf_B add_right_mono Ffin Fpartr unfolding part_def
by (simp add: ‹gS ≠ {}› cSUP_least)
finally show ?thesis
by auto
qed
hence sumB': "sum B' gS ≤ B"
using ennreal_le_epsilon ennreal_less_zero_iff by blast
have "∀r. ∃y. r ∈ gS ⟶ B' r = ennreal y"
using B'fin less_top_ennreal by auto
hence "∃B''. ∀r. r ∈ gS ⟶ B' r = ennreal (B'' r)"
by (rule_tac choice)
then obtain B'' where B'': "B' r = ennreal (B'' r)" if "r ∈ gS" for r
by atomize_elim
have cases[case_names zero finite infinite]: "P" if "r=0 ⟹ P" and "finite (part r) ⟹ P"
and "infinite (part r) ⟹ r≠0 ⟹ P" for P r
using that by metis
have emeasure_B': "r * emeasure M (part r) ≤ B' r" if "r : gS" for r
proof (cases rule:cases[of r])
case zero
thus ?thesis by simp
next
case finite
have s1: "sum g F ≤ sum normf F"
if "F ∈ {F. finite F ∧ F ⊆ part r}"
for F
using ‹g ≤ normf›
by (simp add: le_fun_def sum_mono)
have "r * of_nat (card (part r)) = r * (∑x∈part r. 1)" by simp
also have "… = (∑x∈part r. r)"
using mult.commute by auto
also have "… = (∑x∈part r. g x)"
unfolding part_def by auto
also have "… ≤ (SUP F∈{F. finite F ∧ F⊆part r}. sum g F)"
using finite
by (simp add: Sup_upper)
also have "… ≤ B' r"
unfolding B'_def
using s1 SUP_subset_mono by blast
finally have "r * of_nat (card (part r)) ≤ B' r" by assumption
thus ?thesis
unfolding M_def
using part_def finite by auto
next
case infinite
from r_finite[OF ‹r : gS›] obtain r' where r': "r = ennreal r'"
using ennreal_cases by auto
with infinite have "r' > 0"
using ennreal_less_zero_iff not_gr_zero by blast
obtain N::nat where N:"N > B / r'" and "real N > 0" apply atomize_elim
using reals_Archimedean2
by (metis less_trans linorder_neqE_linordered_idom)
obtain F where "finite F" and "card F = N" and "F ⊆ part r"
using infinite(1) infinite_arbitrarily_large by blast
from ‹F ⊆ part r› have "F ⊆ S" unfolding part_def by simp
have "B < r * N"
unfolding r' ennreal_of_nat_eq_real_of_nat
using N ‹0 < r'› ‹B ≥ 0› r'
by (metis enn2real_ennreal enn2real_less_iff ennreal_less_top ennreal_mult' less_le mult_less_cancel_left_pos nonzero_mult_div_cancel_left times_divide_eq_right)
also have "r * N = (∑x∈F. r)"
using ‹card F = N› by (simp add: mult.commute)
also have "(∑x∈F. r) = (∑x∈F. g x)"
using ‹F ⊆ part r› part_def sum.cong subsetD by fastforce
also have "(∑x∈F. g x) ≤ (∑x∈F. ennreal (norm (f x)))"
by (metis (mono_tags, lifting) ‹g ≤ normf› ‹normf ≡ λx. ennreal (norm (f x))› le_fun_def
sum_mono)
also have "(∑x∈F. ennreal (norm (f x))) ≤ B"
using ‹F ⊆ S› ‹finite F› ‹normf ≡ λx. ennreal (norm (f x))› normf_B by blast
finally have "B < B" by auto
thus ?thesis by simp
qed
have "integral⇧S M g = (∑r ∈ gS. r * emeasure M (part r))"
unfolding simple_integral_def gS_def M_def part_def by simp
also have "… ≤ (∑r ∈ gS. B' r)"
by (simp add: emeasure_B' sum_mono)
also have "… ≤ B"
using sumB' by blast
finally show ?thesis by assumption
qed
hence int_leq_B: "integral⇧N M normf ≤ B"
unfolding nn_integral_def by (metis (no_types, lifting) SUP_least mem_Collect_eq)
hence "integral⇧N M normf < ∞"
using le_less_trans by fastforce
hence "integrable M f"
unfolding M_def normf_def by (rule integrableI_bounded[rotated], simp)
hence v1: "f abs_summable_on S"
unfolding abs_summable_on_def M_def by simp
have "(λx. norm (f x)) abs_summable_on S"
using v1 Infinite_Set_Sum.abs_summable_on_norm_iff[where A = S and f = f]
by auto
moreover have "0 ≤ norm (f x)"
if "x ∈ S" for x
by simp
moreover have "(∫⇧+ x. ennreal (norm (f x)) ∂count_space S) ≤ ennreal B"
using M_def ‹normf ≡ λx. ennreal (norm (f x))› int_leq_B by auto
ultimately have "ennreal (∑⇩ax∈S. norm (f x)) ≤ ennreal B"
by (simp add: nn_integral_conv_infsetsum)
hence v2: "(∑⇩ax∈S. norm (f x)) ≤ B"
by (subst ennreal_le_iff[symmetric], simp add: assms ‹B ≥ 0›)
show ?thesis
using v1 v2 by auto
qed
then show "f abs_summable_on S"
by (metis abs_summable_on_finite assms empty_subsetI finite.emptyI sum_clauses(1))
qed
lemma infsetsum_nonneg_is_SUPREMUM_ennreal:
fixes f :: "'a ⇒ real"
assumes summable: "f abs_summable_on A"
and fnn: "⋀x. x∈A ⟹ f x ≥ 0"
shows "ennreal (infsetsum f A) = (SUP F∈{F. finite F ∧ F ⊆ A}. (ennreal (sum f F)))"
proof -
have sum_F_A: "sum f F ≤ infsetsum f A"
if "F ∈ {F. finite F ∧ F ⊆ A}"
for F
proof-
from that have "finite F" and "F ⊆ A" by auto
from ‹finite F› have "sum f F = infsetsum f F" by auto
also have "… ≤ infsetsum f A"
proof (rule infsetsum_mono_neutral_left)
show "f abs_summable_on F"
by (simp add: ‹finite F›)
show "f abs_summable_on A"
by (simp add: local.summable)
show "f x ≤ f x"
if "x ∈ F"
for x :: 'a
by simp
show "F ⊆ A"
by (simp add: ‹F ⊆ A›)
show "0 ≤ f x"
if "x ∈ A - F"
for x :: 'a
using that fnn by auto
qed
finally show ?thesis by assumption
qed
hence geq: "ennreal (infsetsum f A) ≥ (SUP F∈{G. finite G ∧ G ⊆ A}. (ennreal (sum f F)))"
by (meson SUP_least ennreal_leI)
define fe where "fe x = ennreal (f x)" for x
have sum_f_int: "infsetsum f A = ∫⇧+ x. fe x ∂(count_space A)"
unfolding infsetsum_def fe_def
proof (rule nn_integral_eq_integral [symmetric])
show "integrable (count_space A) f"
using abs_summable_on_def local.summable by blast
show "AE x in count_space A. 0 ≤ f x"
using fnn by auto
qed
also have "… = (SUP g ∈ {g. finite (g`A) ∧ g ≤ fe}. integral⇧S (count_space A) g)"
unfolding nn_integral_def simple_function_count_space by simp
also have "… ≤ (SUP F∈{F. finite F ∧ F ⊆ A}. (ennreal (sum f F)))"
proof (rule Sup_least)
fix x assume "x ∈ integral⇧S (count_space A) ` {g. finite (g ` A) ∧ g ≤ fe}"
then obtain g where xg: "x = integral⇧S (count_space A) g" and fin_gA: "finite (g`A)"
and g_fe: "g ≤ fe" by auto
define F where "F = {z:A. g z ≠ 0}"
hence "F ⊆ A" by simp
have fin: "finite {z:A. g z = t}" if "t ≠ 0" for t
proof (rule ccontr)
assume inf: "infinite {z:A. g z = t}"
hence tgA: "t ∈ g ` A"
by (metis (mono_tags, lifting) image_eqI not_finite_existsD)
have "x = (∑x ∈ g ` A. x * emeasure (count_space A) (g -` {x} ∩ A))"
unfolding xg simple_integral_def space_count_space by simp
also have "… ≥ (∑x ∈ {t}. x * emeasure (count_space A) (g -` {x} ∩ A))" (is "_ ≥ …")
proof (rule sum_mono2)
show "finite (g ` A)"
by (simp add: fin_gA)
show "{t} ⊆ g ` A"
by (simp add: tgA)
show "0 ≤ b * emeasure (count_space A) (g -` {b} ∩ A)"
if "b ∈ g ` A - {t}"
for b :: ennreal
using that
by simp
qed
also have "… = t * emeasure (count_space A) (g -` {t} ∩ A)"
by auto
also have "… = t * ∞"
proof (subst emeasure_count_space_infinite)
show "g -` {t} ∩ A ⊆ A"
by simp
have "{a ∈ A. g a = t} = {a ∈ g -` {t}. a ∈ A}"
by auto
thus "infinite (g -` {t} ∩ A)"
by (metis (full_types) Int_def inf)
show "t * ∞ = t * ∞"
by simp
qed
also have "… = ∞" using ‹t ≠ 0›
by (simp add: ennreal_mult_eq_top_iff)
finally have x_inf: "x = ∞"
using neq_top_trans by auto
have "x = integral⇧S (count_space A) g" by (fact xg)
also have "… = integral⇧N (count_space A) g"
by (simp add: fin_gA nn_integral_eq_simple_integral)
also have "… ≤ integral⇧N (count_space A) fe"
using g_fe
by (simp add: le_funD nn_integral_mono)
also have "… < ∞"
by (metis sum_f_int ennreal_less_top infinity_ennreal_def)
finally have x_fin: "x < ∞" by simp
from x_inf x_fin show False by simp
qed
have F: "F = (⋃t∈g`A-{0}. {z∈A. g z = t})"
unfolding F_def by auto
hence "finite F"
unfolding F using fin_gA fin by auto
have "x = integral⇧N (count_space A) g"
unfolding xg
by (simp add: fin_gA nn_integral_eq_simple_integral)
also have "… = set_nn_integral (count_space UNIV) A g"
by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
also have "… = set_nn_integral (count_space UNIV) F g"
proof -
have "∀a. g a * (if a ∈ {a ∈ A. g a ≠ 0} then 1 else 0) = g a * (if a ∈ A then 1 else 0)"
by auto
hence "(∫⇧+ a. g a * (if a ∈ A then 1 else 0) ∂count_space UNIV)
= (∫⇧+ a. g a * (if a ∈ {a ∈ A. g a ≠ 0} then 1 else 0) ∂count_space UNIV)"
by presburger
thus ?thesis unfolding F_def indicator_def
using mult.right_neutral mult_zero_right nn_integral_cong
by (simp add: of_bool_def)
qed
also have "… = integral⇧N (count_space F) g"
by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
also have "… = sum g F"
using ‹finite F› by (rule nn_integral_count_space_finite)
also have "sum g F ≤ sum fe F"
using g_fe unfolding le_fun_def
by (simp add: sum_mono)
also have "… ≤ (SUP F ∈ {G. finite G ∧ G ⊆ A}. (sum fe F))"
using ‹finite F› ‹F⊆A›
by (simp add: SUP_upper)
also have "… = (SUP F ∈ {F. finite F ∧ F ⊆ A}. (ennreal (sum f F)))"
proof (rule SUP_cong [OF refl])
have "finite x ⟹ x ⊆ A ⟹ (∑x∈x. ennreal (f x)) = ennreal (sum f x)"
for x
by (metis fnn subsetCE sum_ennreal)
thus "sum fe x = ennreal (sum f x)"
if "x ∈ {G. finite G ∧ G ⊆ A}"
for x :: "'a set"
using that unfolding fe_def by auto
qed
finally show "x ≤ …" by simp
qed
finally have leq: "ennreal (infsetsum f A) ≤ (SUP F∈{F. finite F ∧ F ⊆ A}. (ennreal (sum f F)))"
by assumption
from leq geq show ?thesis by simp
qed
lemma infsetsum_nonneg_is_SUPREMUM_ereal:
fixes f :: "'a ⇒ real"
assumes summable: "f abs_summable_on A"
and fnn: "⋀x. x∈A ⟹ f x ≥ 0"
shows "ereal (infsetsum f A) = (SUP F∈{F. finite F ∧ F ⊆ A}. (ereal (sum f F)))"
proof -
have "ereal (infsetsum f A) = enn2ereal (ennreal (infsetsum f A))"
by (simp add: fnn infsetsum_nonneg)
also have "… = enn2ereal (SUP F∈{F. finite F ∧ F ⊆ A}. ennreal (sum f F))"
apply (subst infsetsum_nonneg_is_SUPREMUM_ennreal)
using fnn by (auto simp add: local.summable)
also have "… = (SUP F∈{F. finite F ∧ F ⊆ A}. (ereal (sum f F)))"
proof (simp add: image_def Sup_ennreal.rep_eq)
have "0 ≤ Sup {y. ∃x. (∃xa. finite xa ∧ xa ⊆ A ∧ x = ennreal (sum f xa)) ∧
y = enn2ereal x}"
by (metis (mono_tags, lifting) Sup_upper empty_subsetI ennreal_0 finite.emptyI
mem_Collect_eq sum.empty zero_ennreal.rep_eq)
moreover have "(∃x. (∃y. finite y ∧ y ⊆ A ∧ x = ennreal (sum f y)) ∧ y = enn2ereal x) =
(∃x. finite x ∧ x ⊆ A ∧ y = ereal (sum f x))" for y
proof -
have "(∃x. (∃y. finite y ∧ y ⊆ A ∧ x = ennreal (sum f y)) ∧ y = enn2ereal x) ⟷
(∃X x. finite X ∧ X ⊆ A ∧ x = ennreal (sum f X) ∧ y = enn2ereal x)"
by blast
also have "… ⟷ (∃X. finite X ∧ X ⊆ A ∧ y = ereal (sum f X))"
by (rule arg_cong[of _ _ Ex])
(auto simp: fun_eq_iff intro!: enn2ereal_ennreal sum_nonneg enn2ereal_ennreal[symmetric] fnn)
finally show ?thesis .
qed
hence "Sup {y. ∃x. (∃y. finite y ∧ y ⊆ A ∧ x = ennreal (sum f y)) ∧ y = enn2ereal x} =
Sup {y. ∃x. finite x ∧ x ⊆ A ∧ y = ereal (sum f x)}"
by simp
ultimately show "max 0 (Sup {y. ∃x. (∃xa. finite xa ∧ xa ⊆ A ∧ x
= ennreal (sum f xa)) ∧ y = enn2ereal x})
= Sup {y. ∃x. finite x ∧ x ⊆ A ∧ y = ereal (sum f x)}"
by linarith
qed
finally show ?thesis
by simp
qed
text ‹The following theorem relates \<^const>‹Infinite_Set_Sum.abs_summable_on› with \<^const>‹Infinite_Sum.abs_summable_on›.
Note that while this theorem expresses an equivalence, the notion on the lhs is more general
nonetheless because it applies to a wider range of types. (The rhs requires second-countable
Banach spaces while the lhs is well-defined on arbitrary real vector spaces.)›
lemma abs_summable_equivalent: ‹Infinite_Sum.abs_summable_on f A ⟷ f abs_summable_on A›
proof (rule iffI)
define n where ‹n x = norm (f x)› for x
assume ‹n summable_on A›
then have ‹sum n F ≤ infsum n A› if ‹finite F› and ‹F⊆A› for F
using that by (auto simp flip: infsum_finite simp: n_def[abs_def] intro!: infsum_mono_neutral)
then show ‹f abs_summable_on A›
by (auto intro!: abs_summable_finite_sumsI simp: n_def)
next
define n where ‹n x = norm (f x)› for x
assume ‹f abs_summable_on A›
then have ‹n abs_summable_on A›
by (simp add: ‹f abs_summable_on A› n_def)
then have ‹sum n F ≤ infsetsum n A› if ‹finite F› and ‹F⊆A› for F
using that by (auto simp flip: infsetsum_finite simp: n_def[abs_def] intro!: infsetsum_mono_neutral)
then show ‹n summable_on A›
apply (rule_tac nonneg_bdd_above_summable_on)
by (auto simp add: n_def bdd_above_def)
qed
lemma infsetsum_infsum:
assumes "f abs_summable_on A"
shows "infsetsum f A = infsum f A"
proof -
have conv_sum_norm[simp]: "(λx. norm (f x)) summable_on A"
using abs_summable_equivalent assms by blast
have "norm (infsetsum f A - infsum f A) ≤ ε" if "ε>0" for ε
proof -
define δ where "δ = ε/2"
with that have [simp]: "δ > 0" by simp
obtain F1 where F1A: "F1 ⊆ A" and finF1: "finite F1" and leq_eps: "infsetsum (λx. norm (f x)) (A-F1) ≤ δ"
proof -
have sum_SUP: "ereal (infsetsum (λx. norm (f x)) A) = (SUP F∈{F. finite F ∧ F ⊆ A}. ereal (sum (λx. norm (f x)) F))"
(is "_ = ?SUP")
apply (rule infsetsum_nonneg_is_SUPREMUM_ereal)
using assms by auto
have "(SUP F∈{F. finite F ∧ F ⊆ A}. ereal (∑x∈F. norm (f x))) - ereal δ
< (SUP i∈{F. finite F ∧ F ⊆ A}. ereal (∑x∈i. norm (f x)))"
using ‹δ>0›
by (metis diff_strict_left_mono diff_zero ereal_less_eq(3) ereal_minus(1) not_le sum_SUP)
then obtain F where "F∈{F. finite F ∧ F ⊆ A}" and "ereal (sum (λx. norm (f x)) F) > ?SUP - ereal (δ)"
by (meson less_SUP_iff)
hence "sum (λx. norm (f x)) F > infsetsum (λx. norm (f x)) A - (δ)"
unfolding sum_SUP[symmetric] by auto
hence "δ > infsetsum (λx. norm (f x)) (A-F)"
proof (subst infsetsum_Diff)
show "(λx. norm (f x)) abs_summable_on A"
if "(∑⇩ax∈A. norm (f x)) - δ < (∑x∈F. norm (f x))"
using that
by (simp add: assms)
show "F ⊆ A"
if "(∑⇩ax∈A. norm (f x)) - δ < (∑x∈F. norm (f x))"
using that ‹F ∈ {F. finite F ∧ F ⊆ A}› by blast
show "(∑⇩ax∈A. norm (f x)) - (∑⇩ax∈F. norm (f x)) < δ"
if "(∑⇩ax∈A. norm (f x)) - δ < (∑x∈F. norm (f x))"
using that ‹F ∈ {F. finite F ∧ F ⊆ A}› by auto
qed
thus ?thesis using that
apply atomize_elim
using ‹F ∈ {F. finite F ∧ F ⊆ A}› less_imp_le by blast
qed
obtain F2 where F2A: "F2 ⊆ A" and finF2: "finite F2"
and dist: "dist (sum (λx. norm (f x)) F2) (infsum (λx. norm (f x)) A) ≤ δ"
apply atomize_elim
by (metis ‹0 < δ› conv_sum_norm infsum_finite_approximation)
have leq_eps': "infsum (λx. norm (f x)) (A-F2) ≤ δ"
apply (subst infsum_Diff)
using finF2 F2A dist by (auto simp: dist_norm)
define F where "F = F1 ∪ F2"
have FA: "F ⊆ A" and finF: "finite F"
unfolding F_def using F1A F2A finF1 finF2 by auto
have "(∑⇩ax∈A - (F1 ∪ F2). norm (f x)) ≤ (∑⇩ax∈A - F1. norm (f x))"
apply (rule infsetsum_mono_neutral_left)
using abs_summable_on_subset assms by fastforce+
hence leq_eps: "infsetsum (λx. norm (f x)) (A-F) ≤ δ"
unfolding F_def
using leq_eps by linarith
have "infsum (λx. norm (f x)) (A - (F1 ∪ F2))
≤ infsum (λx. norm (f x)) (A - F2)"
apply (rule infsum_mono_neutral)
using finF by (auto simp add: finF2 summable_on_cofin_subset F_def)
hence leq_eps': "infsum (λx. norm (f x)) (A-F) ≤ δ"
unfolding F_def
by (rule order.trans[OF _ leq_eps'])
have "norm (infsetsum f A - infsetsum f F) = norm (infsetsum f (A-F))"
apply (subst infsetsum_Diff [symmetric])
by (auto simp: FA assms)
also have "… ≤ infsetsum (λx. norm (f x)) (A-F)"
using norm_infsetsum_bound by blast
also have "… ≤ δ"
using leq_eps by simp
finally have diff1: "norm (infsetsum f A - infsetsum f F) ≤ δ"
by assumption
have "norm (infsum f A - infsum f F) = norm (infsum f (A-F))"
apply (subst infsum_Diff [symmetric])
by (auto simp: assms abs_summable_summable finF FA)
also have "… ≤ infsum (λx. norm (f x)) (A-F)"
by (simp add: finF summable_on_cofin_subset norm_infsum_bound)
also have "… ≤ δ"
using leq_eps' by simp
finally have diff2: "norm (infsum f A - infsum f F) ≤ δ"
by assumption
have x1: "infsetsum f F = infsum f F"
using finF by simp
have "norm (infsetsum f A - infsum f A) ≤ norm (infsetsum f A - infsetsum f F) + norm (infsum f A - infsum f F)"
apply (rule_tac norm_diff_triangle_le)
apply auto
by (simp_all add: x1 norm_minus_commute)
also have "… ≤ ε"
using diff1 diff2 δ_def by linarith
finally show ?thesis
by assumption
qed
hence "norm (infsetsum f A - infsum f A) = 0"
by (meson antisym_conv1 dense_ge norm_not_less_zero)
thus ?thesis
by auto
qed
end