products/sources/formale Sprachen/C/Lyx/lib/templates/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Modeler.kaputt.dfm   Sprache: Unknown

(*
  Title:    HOL/Analysis/Infinite_Set_Sum.thy
  Author:   Manuel Eberl, TU München

  A theory of sums over possible infinite sets. (Only works for absolute summability)
*)
section \<open>Sums over Infinite Sets\<close>

theory Infinite_Set_Sum
  imports Set_Integral
begin

(* TODO Move *)
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\<^sub>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\<^sub>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\<^sub>M A (\i. count_space (B i))) \ =
               (\<Prod>i\<in>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\<^sub>M A (\i. count_space (B i))) {f} =
                  emeasure (count_space (Pi\<^sub>E A B)) {f}" .
qed (simp_all add: countable_PiE assms)



definition\<^marker>\<open>tag important\<close> 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\<^marker>\<open>tag important\<close> 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\\<^sub>a_\_./ _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
  "\\<^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 \<comment> \<open>Beware of argument permutation!\<close>
  "\\<^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
  "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}"
  ("(2\\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
translations
  "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}"

print_translation \<open>
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>\<open>_qinfsetsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
          end
    | sum_tr' _ = raise Match;
in [(\<^const_syntax>\<open>infsetsum\<close>, K sum_tr')] end
\<close>


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 *\<^sub>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..
  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 *\<^sub>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 *\<^sub>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' = (\<lambda>x. if x \<in> 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. \\<^sub>ay\B. f x y) = (\\<^sub>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) = (\\<^sub>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) = (\\<^sub>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 *\<^sub>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 *\<^sub>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 \<open>A \<subseteq> B\<close> 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 \<open>B \<subseteq> A\<close> 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' = (\<Union>i\<in>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 *\<^sub>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 \\<^sub>M count_space B') (\(x, y). indicator (B x) y *\<^sub>R f (x, y))"
    by (intro Bochner_Integration.integrable_cong)
       (auto simp: pair_measure_countable indicator_def split: if_splits)
  finally have integrable: \<dots> .

  have "infsetsum (\x. infsetsum (\y. f (x, y)) (B x)) A =
          (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
    unfolding infsetsum_def by simp
  also have "\ = (\x. \y. indicator (B x) y *\<^sub>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) \
         (\<Sum>\<^sub>ay\<in>B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *\<^sub>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 *\<^sub>R f (x, y) \(count_space A \\<^sub>M count_space B'))"
    by (subst integral_fst [OF integrable]) auto
  also have "\ = (\z. indicator (Sigma A B) z *\<^sub>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 \
             (\<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 "(\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 \\<^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))))"
      unfolding set_integrable_def by (rule integrable_fst')
    also have "?this \ 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 "\ \ 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 \<dots> .
  }
  {
    assume *: "\x\A. (\y. f (x, y)) abs_summable_on B x"
    assume "(\x. \\<^sub>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) *\<^sub>R norm (f (x, y)) \count_space B')
                        abs_summable_on A" (is "_ \<longleftrightarrow> ?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 **: \<dots> .

    have "integrable (count_space A \\<^sub>M count_space B') (\z. indicator (Sigma A B) z *\<^sub>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')
                      (\<lambda>y. indicator (B x) y *\<^sub>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 *\<^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)
    moreover have "count_space A \\<^sub>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' = (\<lambda>x. if x \<in> 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) =
          (\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>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 *\<^sub>R c) A = infsetsum f A *\<^sub>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 *\<^sub>R f x) A = c *\<^sub>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


(* TODO Generalise with bounded_linear *)

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

end

[ zur Elbe Produktseite wechseln0.65Quellennavigators  Analyse erneut starten  ]