src/HOL/Analysis/Infinite_Set_Sum.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69517 dc20f278e8f3
child 69597 ff784d5a5bfb
permissions -rw-r--r--
capitalize proper names in lemma names
eberlm@66480
     1
(*  
eberlm@66480
     2
  Title:    HOL/Analysis/Infinite_Set_Sum.thy
eberlm@66480
     3
  Author:   Manuel Eberl, TU M√ľnchen
eberlm@66480
     4
eberlm@66480
     5
  A theory of sums over possible infinite sets. (Only works for absolute summability)
eberlm@66480
     6
*)
nipkow@69517
     7
section \<open>Sums over Infinite Sets\<close>
nipkow@69517
     8
eberlm@66480
     9
theory Infinite_Set_Sum
eberlm@66480
    10
  imports Set_Integral
eberlm@66480
    11
begin
eberlm@66480
    12
eberlm@66480
    13
(* TODO Move *)
eberlm@66480
    14
lemma sets_eq_countable:
eberlm@66480
    15
  assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M"
eberlm@66480
    16
  shows   "sets M = Pow A"
eberlm@66480
    17
proof (intro equalityI subsetI)
eberlm@66480
    18
  fix X assume "X \<in> Pow A"
eberlm@66480
    19
  hence "(\<Union>x\<in>X. {x}) \<in> sets M"
eberlm@66480
    20
    by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3))
eberlm@66480
    21
  also have "(\<Union>x\<in>X. {x}) = X" by auto
eberlm@66480
    22
  finally show "X \<in> sets M" .
eberlm@66480
    23
next
eberlm@66480
    24
  fix X assume "X \<in> sets M"
eberlm@66480
    25
  from sets.sets_into_space[OF this] and assms 
eberlm@66480
    26
    show "X \<in> Pow A" by simp
eberlm@66480
    27
qed
eberlm@66480
    28
eberlm@66480
    29
lemma measure_eqI_countable':
eberlm@66480
    30
  assumes spaces: "space M = A" "space N = A" 
eberlm@66480
    31
  assumes sets: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N"
eberlm@66480
    32
  assumes A: "countable A"
eberlm@66480
    33
  assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
eberlm@66480
    34
  shows "M = N"
eberlm@66480
    35
proof (rule measure_eqI_countable)
eberlm@66480
    36
  show "sets M = Pow A"
eberlm@66480
    37
    by (intro sets_eq_countable assms)
eberlm@66480
    38
  show "sets N = Pow A"
eberlm@66480
    39
    by (intro sets_eq_countable assms)
eberlm@66480
    40
qed fact+
eberlm@66480
    41
eberlm@66480
    42
lemma PiE_singleton: 
eberlm@66480
    43
  assumes "f \<in> extensional A"
eberlm@66480
    44
  shows   "PiE A (\<lambda>x. {f x}) = {f}"
eberlm@66480
    45
proof -
eberlm@66480
    46
  {
eberlm@66480
    47
    fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
eberlm@66480
    48
    hence "g x = f x" for x
eberlm@66480
    49
      using assms by (cases "x \<in> A") (auto simp: extensional_def)
eberlm@66480
    50
    hence "g = f" by (simp add: fun_eq_iff)
eberlm@66480
    51
  }
eberlm@66480
    52
  thus ?thesis using assms by (auto simp: extensional_def)
eberlm@66480
    53
qed
eberlm@66480
    54
eberlm@66480
    55
lemma count_space_PiM_finite:
eberlm@66480
    56
  fixes B :: "'a \<Rightarrow> 'b set"
eberlm@66480
    57
  assumes "finite A" "\<And>i. countable (B i)"
eberlm@66480
    58
  shows   "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)"
eberlm@66480
    59
proof (rule measure_eqI_countable')
eberlm@66480
    60
  show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" 
eberlm@66480
    61
    by (simp add: space_PiM)
eberlm@66480
    62
  show "space (count_space (PiE A B)) = PiE A B" by simp
eberlm@66480
    63
next
eberlm@66480
    64
  fix f assume f: "f \<in> PiE A B"
eberlm@66480
    65
  hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))"
eberlm@66480
    66
    by (intro sets_PiM_I_finite assms) auto
eberlm@66480
    67
  also from f have "PiE A (\<lambda>x. {f x}) = {f}" 
eberlm@66480
    68
    by (intro PiE_singleton) (auto simp: PiE_def)
eberlm@66480
    69
  finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" .
eberlm@66480
    70
next
eberlm@66480
    71
  interpret product_sigma_finite "(\<lambda>i. count_space (B i))"
eberlm@66480
    72
    by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms)
eberlm@66480
    73
  thm sigma_finite_measure_count_space
eberlm@66480
    74
  fix f assume f: "f \<in> PiE A B"
eberlm@66480
    75
  hence "{f} = PiE A (\<lambda>x. {f x})"
eberlm@66480
    76
    by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
eberlm@66480
    77
  also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = 
eberlm@66480
    78
               (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})"
eberlm@66480
    79
    using f assms by (subst emeasure_PiM) auto
eberlm@66480
    80
  also have "\<dots> = (\<Prod>i\<in>A. 1)"
eberlm@66480
    81
    by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto)
eberlm@66480
    82
  also have "\<dots> = emeasure (count_space (PiE A B)) {f}"
eberlm@66480
    83
    using f by (subst emeasure_count_space_finite) auto
eberlm@66480
    84
  finally show "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) {f} =
eberlm@66480
    85
                  emeasure (count_space (Pi\<^sub>E A B)) {f}" .
eberlm@66480
    86
qed (simp_all add: countable_PiE assms)
eberlm@66480
    87
eberlm@66480
    88
eberlm@66480
    89
eberlm@68651
    90
definition%important abs_summable_on ::
eberlm@66480
    91
    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
eberlm@66480
    92
    (infix "abs'_summable'_on" 50)
eberlm@66480
    93
 where
eberlm@66480
    94
   "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
eberlm@66480
    95
eberlm@66480
    96
eberlm@68651
    97
definition%important infsetsum ::
eberlm@66480
    98
    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b"
eberlm@66480
    99
 where
eberlm@66480
   100
   "infsetsum f A = lebesgue_integral (count_space A) f"
eberlm@66480
   101
eberlm@66480
   102
syntax (ASCII)
eberlm@66480
   103
  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
eberlm@66480
   104
  ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
eberlm@66480
   105
syntax
eberlm@66480
   106
  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
eberlm@66480
   107
  ("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
eberlm@66480
   108
translations \<comment> \<open>Beware of argument permutation!\<close>
eberlm@66480
   109
  "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
eberlm@66480
   110
eberlm@66480
   111
syntax (ASCII)
eberlm@66526
   112
  "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
eberlm@66526
   113
  ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
eberlm@66526
   114
syntax
eberlm@66526
   115
  "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
eberlm@66526
   116
  ("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
eberlm@66526
   117
translations \<comment> \<open>Beware of argument permutation!\<close>
eberlm@66526
   118
  "\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
eberlm@66526
   119
eberlm@66526
   120
syntax (ASCII)
eberlm@66480
   121
  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
eberlm@66480
   122
  ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
eberlm@66480
   123
syntax
eberlm@66480
   124
  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
eberlm@66480
   125
  ("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
eberlm@66480
   126
translations
eberlm@66480
   127
  "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
eberlm@66480
   128
eberlm@66480
   129
print_translation \<open>
eberlm@66480
   130
let
eberlm@66480
   131
  fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
eberlm@66480
   132
        if x <> y then raise Match
eberlm@66480
   133
        else
eberlm@66480
   134
          let
eberlm@66480
   135
            val x' = Syntax_Trans.mark_bound_body (x, Tx);
eberlm@66480
   136
            val t' = subst_bound (x', t);
eberlm@66480
   137
            val P' = subst_bound (x', P);
eberlm@66480
   138
          in
eberlm@66480
   139
            Syntax.const @{syntax_const "_qinfsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
eberlm@66480
   140
          end
eberlm@66480
   141
    | sum_tr' _ = raise Match;
eberlm@66480
   142
in [(@{const_syntax infsetsum}, K sum_tr')] end
eberlm@66480
   143
\<close>
eberlm@66480
   144
eberlm@66480
   145
eberlm@66480
   146
lemma restrict_count_space_subset:
eberlm@66480
   147
  "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
eberlm@66480
   148
  by (subst restrict_count_space) (simp_all add: Int_absorb2)
eberlm@66480
   149
eberlm@66480
   150
lemma abs_summable_on_restrict:
eberlm@66480
   151
  fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
eberlm@66480
   152
  assumes "A \<subseteq> B"
eberlm@66480
   153
  shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) abs_summable_on B"
eberlm@66480
   154
proof -
eberlm@66480
   155
  have "count_space A = restrict_space (count_space B) A"
eberlm@66480
   156
    by (rule restrict_count_space_subset [symmetric]) fact+
eberlm@66480
   157
  also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f"
lp15@67974
   158
    by (simp add: integrable_restrict_space set_integrable_def)
eberlm@66480
   159
  finally show ?thesis 
lp15@67974
   160
    unfolding abs_summable_on_def set_integrable_def .
eberlm@66480
   161
qed
eberlm@66480
   162
eberlm@66480
   163
lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f"
lp15@67974
   164
  unfolding abs_summable_on_def set_integrable_def
lp15@67974
   165
  by (metis (no_types) inf_top.right_neutral integrable_restrict_space restrict_count_space sets_UNIV)
eberlm@66480
   166
eberlm@66480
   167
lemma abs_summable_on_altdef': 
eberlm@66480
   168
  "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
lp15@67974
   169
  unfolding abs_summable_on_def set_integrable_def
lp15@67974
   170
  by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset set_integrable_def sets_count_space space_count_space)
eberlm@66480
   171
eberlm@66526
   172
lemma abs_summable_on_norm_iff [simp]: 
eberlm@66526
   173
  "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
eberlm@66526
   174
  by (simp add: abs_summable_on_def integrable_norm_iff)
eberlm@66526
   175
eberlm@66526
   176
lemma abs_summable_on_normI: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. norm (f x)) abs_summable_on A"
eberlm@66526
   177
  by simp
eberlm@66526
   178
lp15@67268
   179
lemma abs_summable_complex_of_real [simp]: "(\<lambda>n. complex_of_real (f n)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
lp15@67268
   180
  by (simp add: abs_summable_on_def complex_of_real_integrable_eq)
lp15@67268
   181
eberlm@66526
   182
lemma abs_summable_on_comparison_test:
eberlm@66526
   183
  assumes "g abs_summable_on A"
eberlm@66526
   184
  assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> norm (g x)"
eberlm@66526
   185
  shows   "f abs_summable_on A"
eberlm@66526
   186
  using assms Bochner_Integration.integrable_bound[of "count_space A" g f] 
eberlm@66526
   187
  unfolding abs_summable_on_def by (auto simp: AE_count_space)  
eberlm@66526
   188
eberlm@66526
   189
lemma abs_summable_on_comparison_test':
eberlm@66526
   190
  assumes "g abs_summable_on A"
eberlm@66526
   191
  assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> g x"
eberlm@66526
   192
  shows   "f abs_summable_on A"
eberlm@66526
   193
proof (rule abs_summable_on_comparison_test[OF assms(1), of f])
eberlm@66526
   194
  fix x assume "x \<in> A"
eberlm@66526
   195
  with assms(2) have "norm (f x) \<le> g x" .
eberlm@66526
   196
  also have "\<dots> \<le> norm (g x)" by simp
eberlm@66526
   197
  finally show "norm (f x) \<le> norm (g x)" .
eberlm@66526
   198
qed
eberlm@66526
   199
eberlm@66480
   200
lemma abs_summable_on_cong [cong]:
eberlm@66480
   201
  "(\<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)"
eberlm@66480
   202
  unfolding abs_summable_on_def by (intro integrable_cong) auto
eberlm@66480
   203
eberlm@66480
   204
lemma abs_summable_on_cong_neutral:
eberlm@66480
   205
  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
eberlm@66480
   206
  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
eberlm@66480
   207
  assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
eberlm@66480
   208
  shows   "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B"
lp15@67974
   209
  unfolding abs_summable_on_altdef set_integrable_def using assms
eberlm@66480
   210
  by (intro Bochner_Integration.integrable_cong refl)
eberlm@66480
   211
     (auto simp: indicator_def split: if_splits)
eberlm@66480
   212
eberlm@66480
   213
lemma abs_summable_on_restrict':
eberlm@66480
   214
  fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
eberlm@66480
   215
  assumes "A \<subseteq> B"
eberlm@66480
   216
  shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. if x \<in> A then f x else 0) abs_summable_on B"
eberlm@66480
   217
  by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto)
eberlm@66480
   218
eberlm@66480
   219
lemma abs_summable_on_nat_iff:
eberlm@66480
   220
  "f abs_summable_on (A :: nat set) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
eberlm@66480
   221
proof -
eberlm@66480
   222
  have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> A then f x else 0))"
eberlm@66480
   223
    by (subst abs_summable_on_restrict'[of _ UNIV]) 
eberlm@66480
   224
       (simp_all add: abs_summable_on_def integrable_count_space_nat_iff)
eberlm@66480
   225
  also have "(\<lambda>x. norm (if x \<in> A then f x else 0)) = (\<lambda>x. if x \<in> A then norm (f x) else 0)"
eberlm@66480
   226
    by auto
eberlm@66480
   227
  finally show ?thesis .
eberlm@66480
   228
qed
eberlm@66480
   229
eberlm@66480
   230
lemma abs_summable_on_nat_iff':
eberlm@66480
   231
  "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))"
eberlm@66480
   232
  by (subst abs_summable_on_nat_iff) auto
eberlm@66480
   233
lp15@67268
   234
lemma nat_abs_summable_on_comparison_test:
lp15@67268
   235
  fixes f :: "nat \<Rightarrow> 'a :: {banach, second_countable_topology}"
lp15@67268
   236
  assumes "g abs_summable_on I"
lp15@67268
   237
  assumes "\<And>n. \<lbrakk>n\<ge>N; n \<in> I\<rbrakk> \<Longrightarrow> norm (f n) \<le> g n"
lp15@67268
   238
  shows   "f abs_summable_on I"
lp15@67268
   239
  using assms by (fastforce simp add: abs_summable_on_nat_iff intro: summable_comparison_test')
lp15@67268
   240
lp15@67268
   241
lemma abs_summable_comparison_test_ev:
lp15@67268
   242
  assumes "g abs_summable_on I"
lp15@67268
   243
  assumes "eventually (\<lambda>x. x \<in> I \<longrightarrow> norm (f x) \<le> g x) sequentially"
lp15@67268
   244
  shows   "f abs_summable_on I"
lp15@67268
   245
  by (metis (no_types, lifting) nat_abs_summable_on_comparison_test eventually_at_top_linorder assms)
lp15@67268
   246
lp15@67268
   247
lemma abs_summable_on_Cauchy:
lp15@67268
   248
  "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. (\<Sum>x = m..<n. norm (f x)) < e)"
lp15@67268
   249
  by (simp add: abs_summable_on_nat_iff' summable_Cauchy sum_nonneg)
lp15@67268
   250
eberlm@66480
   251
lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   252
  unfolding abs_summable_on_def by (rule integrable_count_space)
eberlm@66480
   253
eberlm@66480
   254
lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}"
eberlm@66480
   255
  by simp
eberlm@66480
   256
eberlm@66480
   257
lemma abs_summable_on_subset:
eberlm@66480
   258
  assumes "f abs_summable_on B" and "A \<subseteq> B"
eberlm@66480
   259
  shows   "f abs_summable_on A"
eberlm@66480
   260
  unfolding abs_summable_on_altdef
eberlm@66480
   261
  by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef)
eberlm@66480
   262
eberlm@66480
   263
lemma abs_summable_on_union [intro]:
eberlm@66480
   264
  assumes "f abs_summable_on A" and "f abs_summable_on B"
eberlm@66480
   265
  shows   "f abs_summable_on (A \<union> B)"
eberlm@66480
   266
  using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto
eberlm@66480
   267
eberlm@66526
   268
lemma abs_summable_on_insert_iff [simp]:
eberlm@66526
   269
  "f abs_summable_on insert x A \<longleftrightarrow> f abs_summable_on A"
eberlm@66526
   270
proof safe
eberlm@66526
   271
  assume "f abs_summable_on insert x A"
eberlm@66526
   272
  thus "f abs_summable_on A"
eberlm@66526
   273
    by (rule abs_summable_on_subset) auto
eberlm@66526
   274
next
eberlm@66526
   275
  assume "f abs_summable_on A"
eberlm@66526
   276
  from abs_summable_on_union[OF this, of "{x}"]
eberlm@66526
   277
    show "f abs_summable_on insert x A" by simp
eberlm@66526
   278
qed
eberlm@66526
   279
eberlm@67167
   280
lemma abs_summable_sum: 
eberlm@67167
   281
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
eberlm@67167
   282
  shows   "(\<lambda>y. \<Sum>x\<in>A. f x y) abs_summable_on B"
eberlm@67167
   283
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)
eberlm@67167
   284
eberlm@67167
   285
lemma abs_summable_Re: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Re (f x)) abs_summable_on A"
eberlm@67167
   286
  by (simp add: abs_summable_on_def)
eberlm@67167
   287
eberlm@67167
   288
lemma abs_summable_Im: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Im (f x)) abs_summable_on A"
eberlm@67167
   289
  by (simp add: abs_summable_on_def)
eberlm@67167
   290
eberlm@67167
   291
lemma abs_summable_on_finite_diff:
eberlm@67167
   292
  assumes "f abs_summable_on A" "A \<subseteq> B" "finite (B - A)"
eberlm@67167
   293
  shows   "f abs_summable_on B"
eberlm@67167
   294
proof -
eberlm@67167
   295
  have "f abs_summable_on (A \<union> (B - A))"
eberlm@67167
   296
    by (intro abs_summable_on_union assms abs_summable_on_finite)
eberlm@67167
   297
  also from assms have "A \<union> (B - A) = B" by blast
eberlm@67167
   298
  finally show ?thesis .
eberlm@67167
   299
qed
eberlm@67167
   300
eberlm@66480
   301
lemma abs_summable_on_reindex_bij_betw:
eberlm@66480
   302
  assumes "bij_betw g A B"
eberlm@66480
   303
  shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
eberlm@66480
   304
proof -
eberlm@66480
   305
  have *: "count_space B = distr (count_space A) (count_space B) g"
eberlm@66480
   306
    by (rule distr_bij_count_space [symmetric]) fact
eberlm@66480
   307
  show ?thesis unfolding abs_summable_on_def
eberlm@66480
   308
    by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) 
eberlm@66480
   309
       (insert assms, auto simp: bij_betw_def)
eberlm@66480
   310
qed
eberlm@66480
   311
eberlm@66480
   312
lemma abs_summable_on_reindex:
eberlm@66480
   313
  assumes "(\<lambda>x. f (g x)) abs_summable_on A"
eberlm@66480
   314
  shows   "f abs_summable_on (g ` A)"
eberlm@66480
   315
proof -
eberlm@66480
   316
  define g' where "g' = inv_into A g"
eberlm@66480
   317
  from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" 
eberlm@66480
   318
    by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into)
eberlm@66480
   319
  also have "?this \<longleftrightarrow> (\<lambda>x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def
eberlm@66480
   320
    by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto
eberlm@66480
   321
  also have "\<dots> \<longleftrightarrow> f abs_summable_on (g ` A)"
eberlm@66480
   322
    by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f)
eberlm@66480
   323
  finally show ?thesis .
eberlm@66480
   324
qed
eberlm@66480
   325
eberlm@66526
   326
lemma abs_summable_on_reindex_iff: 
eberlm@66480
   327
  "inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)"
eberlm@66480
   328
  by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw)
eberlm@66480
   329
eberlm@66526
   330
lemma abs_summable_on_Sigma_project2:
eberlm@66480
   331
  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
eberlm@66480
   332
  assumes "f abs_summable_on (Sigma A B)" "x \<in> A"
eberlm@66480
   333
  shows   "(\<lambda>y. f (x, y)) abs_summable_on (B x)"
eberlm@66480
   334
proof -
eberlm@66480
   335
  from assms(2) have "f abs_summable_on (Sigma {x} B)"
eberlm@66480
   336
    by (intro abs_summable_on_subset [OF assms(1)]) auto
eberlm@66480
   337
  also have "?this \<longleftrightarrow> (\<lambda>z. f (x, snd z)) abs_summable_on (Sigma {x} B)"
eberlm@66480
   338
    by (rule abs_summable_on_cong) auto
eberlm@66480
   339
  finally have "(\<lambda>y. f (x, y)) abs_summable_on (snd ` Sigma {x} B)"
eberlm@66480
   340
    by (rule abs_summable_on_reindex)
eberlm@66480
   341
  also have "snd ` Sigma {x} B = B x"
eberlm@66480
   342
    using assms by (auto simp: image_iff)
eberlm@66480
   343
  finally show ?thesis .
eberlm@66480
   344
qed
eberlm@66480
   345
eberlm@66480
   346
lemma abs_summable_on_Times_swap:
eberlm@66480
   347
  "f abs_summable_on A \<times> B \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) abs_summable_on B \<times> A"
eberlm@66480
   348
proof -
eberlm@66480
   349
  have bij: "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)"
eberlm@66480
   350
    by (auto simp: bij_betw_def inj_on_def)
eberlm@66480
   351
  show ?thesis
eberlm@66480
   352
    by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric])
eberlm@66480
   353
       (simp_all add: case_prod_unfold)
eberlm@66480
   354
qed
eberlm@66480
   355
eberlm@66480
   356
lemma abs_summable_on_0 [simp, intro]: "(\<lambda>_. 0) abs_summable_on A"
eberlm@66480
   357
  by (simp add: abs_summable_on_def)
eberlm@66480
   358
eberlm@66480
   359
lemma abs_summable_on_uminus [intro]:
eberlm@66480
   360
  "f abs_summable_on A \<Longrightarrow> (\<lambda>x. -f x) abs_summable_on A"
eberlm@66480
   361
  unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus)
eberlm@66480
   362
eberlm@66480
   363
lemma abs_summable_on_add [intro]:
eberlm@66480
   364
  assumes "f abs_summable_on A" and "g abs_summable_on A"
eberlm@66480
   365
  shows   "(\<lambda>x. f x + g x) abs_summable_on A"
eberlm@66480
   366
  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add)
eberlm@66480
   367
eberlm@66480
   368
lemma abs_summable_on_diff [intro]:
eberlm@66480
   369
  assumes "f abs_summable_on A" and "g abs_summable_on A"
eberlm@66480
   370
  shows   "(\<lambda>x. f x - g x) abs_summable_on A"
eberlm@66480
   371
  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff)
eberlm@66480
   372
eberlm@66480
   373
lemma abs_summable_on_scaleR_left [intro]:
eberlm@66480
   374
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   375
  shows   "(\<lambda>x. f x *\<^sub>R c) abs_summable_on A"
eberlm@66480
   376
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left)
eberlm@66480
   377
eberlm@66480
   378
lemma abs_summable_on_scaleR_right [intro]:
eberlm@66480
   379
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   380
  shows   "(\<lambda>x. c *\<^sub>R f x) abs_summable_on A"
eberlm@66480
   381
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right)
eberlm@66480
   382
eberlm@66480
   383
lemma abs_summable_on_cmult_right [intro]:
eberlm@66480
   384
  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
eberlm@66480
   385
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   386
  shows   "(\<lambda>x. c * f x) abs_summable_on A"
eberlm@66480
   387
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right)
eberlm@66480
   388
eberlm@66480
   389
lemma abs_summable_on_cmult_left [intro]:
eberlm@66480
   390
  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
eberlm@66480
   391
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   392
  shows   "(\<lambda>x. f x * c) abs_summable_on A"
eberlm@66480
   393
  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)
eberlm@66480
   394
eberlm@66568
   395
lemma abs_summable_on_prod_PiE:
eberlm@66568
   396
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
eberlm@66568
   397
  assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
eberlm@66568
   398
  assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
eberlm@66568
   399
  shows   "(\<lambda>g. \<Prod>x\<in>A. f x (g x)) abs_summable_on PiE A B"
eberlm@66568
   400
proof -
eberlm@66568
   401
  define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
eberlm@66568
   402
  from assms have [simp]: "countable (B' x)" for x
eberlm@66568
   403
    by (auto simp: B'_def)
eberlm@66568
   404
  then interpret product_sigma_finite "count_space \<circ> B'"
eberlm@66568
   405
    unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
eberlm@66568
   406
  from assms have "integrable (PiM A (count_space \<circ> B')) (\<lambda>g. \<Prod>x\<in>A. f x (g x))"
eberlm@66568
   407
    by (intro product_integrable_prod) (auto simp: abs_summable_on_def B'_def)
eberlm@66568
   408
  also have "PiM A (count_space \<circ> B') = count_space (PiE A B')"
eberlm@66568
   409
    unfolding o_def using finite by (intro count_space_PiM_finite) simp_all
eberlm@66568
   410
  also have "PiE A B' = PiE A B" by (intro PiE_cong) (simp_all add: B'_def)
eberlm@66568
   411
  finally show ?thesis by (simp add: abs_summable_on_def)
eberlm@66568
   412
qed
eberlm@66568
   413
eberlm@66480
   414
eberlm@66480
   415
eberlm@66480
   416
lemma not_summable_infsetsum_eq:
eberlm@66480
   417
  "\<not>f abs_summable_on A \<Longrightarrow> infsetsum f A = 0"
eberlm@66480
   418
  by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq)
eberlm@66480
   419
eberlm@66480
   420
lemma infsetsum_altdef:
eberlm@66480
   421
  "infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
lp15@67974
   422
  unfolding set_lebesgue_integral_def
eberlm@66480
   423
  by (subst integral_restrict_space [symmetric])
eberlm@66480
   424
     (auto simp: restrict_count_space_subset infsetsum_def)
eberlm@66480
   425
eberlm@66480
   426
lemma infsetsum_altdef':
eberlm@66480
   427
  "A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f"
lp15@67974
   428
  unfolding set_lebesgue_integral_def
eberlm@66480
   429
  by (subst integral_restrict_space [symmetric])
eberlm@66480
   430
     (auto simp: restrict_count_space_subset infsetsum_def)
eberlm@66480
   431
eberlm@66568
   432
lemma nn_integral_conv_infsetsum:
eberlm@66568
   433
  assumes "f abs_summable_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
eberlm@66568
   434
  shows   "nn_integral (count_space A) f = ennreal (infsetsum f A)"
eberlm@66568
   435
  using assms unfolding infsetsum_def abs_summable_on_def
eberlm@66568
   436
  by (subst nn_integral_eq_integral) auto
eberlm@66568
   437
eberlm@66568
   438
lemma infsetsum_conv_nn_integral:
eberlm@66568
   439
  assumes "nn_integral (count_space A) f \<noteq> \<infinity>" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
eberlm@66568
   440
  shows   "infsetsum f A = enn2real (nn_integral (count_space A) f)"
eberlm@66568
   441
  unfolding infsetsum_def using assms
eberlm@66568
   442
  by (subst integral_eq_nn_integral) auto
eberlm@66568
   443
eberlm@66480
   444
lemma infsetsum_cong [cong]:
eberlm@66480
   445
  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B"
eberlm@66480
   446
  unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto
eberlm@66480
   447
eberlm@66480
   448
lemma infsetsum_0 [simp]: "infsetsum (\<lambda>_. 0) A = 0"
eberlm@66480
   449
  by (simp add: infsetsum_def)
eberlm@66480
   450
eberlm@66480
   451
lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0"
eberlm@66480
   452
  by simp
eberlm@66480
   453
eberlm@67167
   454
lemma infsetsum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> f x \<ge> (0::real)) \<Longrightarrow> infsetsum f A \<ge> 0"
eberlm@67167
   455
  unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto
eberlm@67167
   456
eberlm@67167
   457
lemma sum_infsetsum:
eberlm@67167
   458
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
eberlm@67167
   459
  shows   "(\<Sum>x\<in>A. \<Sum>\<^sub>ay\<in>B. f x y) = (\<Sum>\<^sub>ay\<in>B. \<Sum>x\<in>A. f x y)"
eberlm@67167
   460
  using assms by (simp add: infsetsum_def abs_summable_on_def Bochner_Integration.integral_sum)
eberlm@67167
   461
eberlm@67167
   462
lemma Re_infsetsum: "f abs_summable_on A \<Longrightarrow> Re (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Re (f x))"
eberlm@67167
   463
  by (simp add: infsetsum_def abs_summable_on_def)
eberlm@67167
   464
eberlm@67167
   465
lemma Im_infsetsum: "f abs_summable_on A \<Longrightarrow> Im (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Im (f x))"
eberlm@67167
   466
  by (simp add: infsetsum_def abs_summable_on_def)
eberlm@67167
   467
eberlm@67167
   468
lemma infsetsum_of_real: 
eberlm@67167
   469
  shows "infsetsum (\<lambda>x. of_real (f x) 
eberlm@67167
   470
           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = 
eberlm@67167
   471
             of_real (infsetsum f A)"
eberlm@67167
   472
  unfolding infsetsum_def
eberlm@67167
   473
  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto
eberlm@67167
   474
eberlm@66480
   475
lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
eberlm@66480
   476
  by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
eberlm@66480
   477
eberlm@66480
   478
lemma infsetsum_nat: 
eberlm@66480
   479
  assumes "f abs_summable_on A"
eberlm@66480
   480
  shows   "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)"
eberlm@66480
   481
proof -
eberlm@66480
   482
  from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)"
lp15@67974
   483
    unfolding infsetsum_altdef abs_summable_on_altdef set_lebesgue_integral_def set_integrable_def
lp15@67974
   484
 by (subst integral_count_space_nat) auto
eberlm@66480
   485
  also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)"
eberlm@66480
   486
    by auto
eberlm@66480
   487
  finally show ?thesis .
eberlm@66480
   488
qed
eberlm@66480
   489
eberlm@66480
   490
lemma infsetsum_nat': 
eberlm@66480
   491
  assumes "f abs_summable_on UNIV"
eberlm@66480
   492
  shows   "infsetsum f UNIV = (\<Sum>n. f n)"
eberlm@66480
   493
  using assms by (subst infsetsum_nat) auto
eberlm@66480
   494
eberlm@66480
   495
lemma sums_infsetsum_nat:
eberlm@66480
   496
  assumes "f abs_summable_on A"
eberlm@66480
   497
  shows   "(\<lambda>n. if n \<in> A then f n else 0) sums infsetsum f A"
eberlm@66480
   498
proof -
eberlm@66480
   499
  from assms have "summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
eberlm@66480
   500
    by (simp add: abs_summable_on_nat_iff)
eberlm@66480
   501
  also have "(\<lambda>n. if n \<in> A then norm (f n) else 0) = (\<lambda>n. norm (if n \<in> A then f n else 0))"
eberlm@66480
   502
    by auto
eberlm@66480
   503
  finally have "summable (\<lambda>n. if n \<in> A then f n else 0)"
eberlm@66480
   504
    by (rule summable_norm_cancel)
eberlm@66480
   505
  with assms show ?thesis
eberlm@66480
   506
    by (auto simp: sums_iff infsetsum_nat)
eberlm@66480
   507
qed
eberlm@66480
   508
eberlm@66480
   509
lemma sums_infsetsum_nat':
eberlm@66480
   510
  assumes "f abs_summable_on UNIV"
eberlm@66480
   511
  shows   "f sums infsetsum f UNIV"
eberlm@66480
   512
  using sums_infsetsum_nat [OF assms] by simp
eberlm@66480
   513
eberlm@66480
   514
lemma infsetsum_Un_disjoint:
eberlm@66480
   515
  assumes "f abs_summable_on A" "f abs_summable_on B" "A \<inter> B = {}"
eberlm@66480
   516
  shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B"
eberlm@66480
   517
  using assms unfolding infsetsum_altdef abs_summable_on_altdef
eberlm@66480
   518
  by (subst set_integral_Un) auto
eberlm@66480
   519
eberlm@66480
   520
lemma infsetsum_Diff:
eberlm@66480
   521
  assumes "f abs_summable_on B" "A \<subseteq> B"
eberlm@66480
   522
  shows   "infsetsum f (B - A) = infsetsum f B - infsetsum f A"
eberlm@66480
   523
proof -
eberlm@66480
   524
  have "infsetsum f ((B - A) \<union> A) = infsetsum f (B - A) + infsetsum f A"
eberlm@66480
   525
    using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto
eberlm@66480
   526
  also from assms(2) have "(B - A) \<union> A = B"
eberlm@66480
   527
    by auto
eberlm@66480
   528
  ultimately show ?thesis
eberlm@66480
   529
    by (simp add: algebra_simps)
eberlm@66480
   530
qed
eberlm@66480
   531
eberlm@66480
   532
lemma infsetsum_Un_Int:
eberlm@66480
   533
  assumes "f abs_summable_on (A \<union> B)"
eberlm@66480
   534
  shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B - infsetsum f (A \<inter> B)"
eberlm@66480
   535
proof -
eberlm@66480
   536
  have "A \<union> B = A \<union> (B - A \<inter> B)"
eberlm@66480
   537
    by auto
eberlm@66480
   538
  also have "infsetsum f \<dots> = infsetsum f A + infsetsum f (B - A \<inter> B)"
eberlm@66480
   539
    by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto
eberlm@66480
   540
  also have "infsetsum f (B - A \<inter> B) = infsetsum f B - infsetsum f (A \<inter> B)"
eberlm@66480
   541
    by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto
eberlm@66480
   542
  finally show ?thesis 
eberlm@66480
   543
    by (simp add: algebra_simps)
eberlm@66480
   544
qed
eberlm@66480
   545
eberlm@66480
   546
lemma infsetsum_reindex_bij_betw:
eberlm@66480
   547
  assumes "bij_betw g A B"
eberlm@66480
   548
  shows   "infsetsum (\<lambda>x. f (g x)) A = infsetsum f B"
eberlm@66480
   549
proof -
eberlm@66480
   550
  have *: "count_space B = distr (count_space A) (count_space B) g"
eberlm@66480
   551
    by (rule distr_bij_count_space [symmetric]) fact
eberlm@66480
   552
  show ?thesis unfolding infsetsum_def
eberlm@66480
   553
    by (subst *, subst integral_distr[of _ _ "count_space B"]) 
eberlm@66480
   554
       (insert assms, auto simp: bij_betw_def)    
eberlm@66480
   555
qed
eberlm@66480
   556
eberlm@68651
   557
theorem infsetsum_reindex:
eberlm@66480
   558
  assumes "inj_on g A"
eberlm@66480
   559
  shows   "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A"
eberlm@66480
   560
  by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
eberlm@66480
   561
eberlm@66480
   562
lemma infsetsum_cong_neutral:
eberlm@66480
   563
  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
eberlm@66480
   564
  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
eberlm@66480
   565
  assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
eberlm@66480
   566
  shows   "infsetsum f A = infsetsum g B"
lp15@67974
   567
  unfolding infsetsum_altdef set_lebesgue_integral_def using assms
eberlm@66480
   568
  by (intro Bochner_Integration.integral_cong refl)
eberlm@66480
   569
     (auto simp: indicator_def split: if_splits)
eberlm@66480
   570
eberlm@66526
   571
lemma infsetsum_mono_neutral:
eberlm@66526
   572
  fixes f g :: "'a \<Rightarrow> real"
eberlm@66526
   573
  assumes "f abs_summable_on A" and "g abs_summable_on B"
eberlm@66526
   574
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
eberlm@66526
   575
  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
eberlm@66526
   576
  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
eberlm@66526
   577
  shows   "infsetsum f A \<le> infsetsum g B"
lp15@67974
   578
  using assms unfolding infsetsum_altdef set_lebesgue_integral_def abs_summable_on_altdef set_integrable_def
eberlm@66526
   579
  by (intro Bochner_Integration.integral_mono) (auto simp: indicator_def)
eberlm@66526
   580
eberlm@66526
   581
lemma infsetsum_mono_neutral_left:
eberlm@66526
   582
  fixes f g :: "'a \<Rightarrow> real"
eberlm@66526
   583
  assumes "f abs_summable_on A" and "g abs_summable_on B"
eberlm@66526
   584
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
eberlm@66526
   585
  assumes "A \<subseteq> B"
eberlm@66526
   586
  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
eberlm@66526
   587
  shows   "infsetsum f A \<le> infsetsum g B"
eberlm@66526
   588
  using \<open>A \<subseteq> B\<close> by (intro infsetsum_mono_neutral assms) auto
eberlm@66526
   589
eberlm@66526
   590
lemma infsetsum_mono_neutral_right:
eberlm@66526
   591
  fixes f g :: "'a \<Rightarrow> real"
eberlm@66526
   592
  assumes "f abs_summable_on A" and "g abs_summable_on B"
eberlm@66526
   593
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
eberlm@66526
   594
  assumes "B \<subseteq> A"
eberlm@66526
   595
  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
eberlm@66526
   596
  shows   "infsetsum f A \<le> infsetsum g B"
eberlm@66526
   597
  using \<open>B \<subseteq> A\<close> by (intro infsetsum_mono_neutral assms) auto
eberlm@66526
   598
eberlm@66526
   599
lemma infsetsum_mono:
eberlm@66526
   600
  fixes f g :: "'a \<Rightarrow> real"
eberlm@66526
   601
  assumes "f abs_summable_on A" and "g abs_summable_on A"
eberlm@66526
   602
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
eberlm@66526
   603
  shows   "infsetsum f A \<le> infsetsum g A"
eberlm@66526
   604
  by (intro infsetsum_mono_neutral assms) auto
eberlm@66526
   605
eberlm@66526
   606
lemma norm_infsetsum_bound:
eberlm@66526
   607
  "norm (infsetsum f A) \<le> infsetsum (\<lambda>x. norm (f x)) A"
eberlm@66526
   608
  unfolding abs_summable_on_def infsetsum_def
eberlm@66526
   609
  by (rule Bochner_Integration.integral_norm_bound)
eberlm@66526
   610
eberlm@68651
   611
theorem infsetsum_Sigma:
eberlm@66480
   612
  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
eberlm@66480
   613
  assumes [simp]: "countable A" and "\<And>i. countable (B i)"
eberlm@66480
   614
  assumes summable: "f abs_summable_on (Sigma A B)"
eberlm@66480
   615
  shows   "infsetsum f (Sigma A B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A"
eberlm@66480
   616
proof -
eberlm@66480
   617
  define B' where "B' = (\<Union>i\<in>A. B i)"
eberlm@66480
   618
  have [simp]: "countable B'" 
eberlm@66480
   619
    unfolding B'_def by (intro countable_UN assms)
eberlm@66480
   620
  interpret pair_sigma_finite "count_space A" "count_space B'"
eberlm@66480
   621
    by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
eberlm@66480
   622
eberlm@66480
   623
  have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
lp15@67974
   624
    using summable
lp15@67974
   625
    by (metis (mono_tags, lifting) abs_summable_on_altdef abs_summable_on_def integrable_cong integrable_mult_indicator set_integrable_def sets_UNIV)
eberlm@66480
   626
  also have "?this \<longleftrightarrow> integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>(x, y). indicator (B x) y *\<^sub>R f (x, y))"
eberlm@66480
   627
    by (intro Bochner_Integration.integrable_cong)
eberlm@66480
   628
       (auto simp: pair_measure_countable indicator_def split: if_splits)
eberlm@66480
   629
  finally have integrable: \<dots> .
eberlm@66480
   630
  
eberlm@66480
   631
  have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A =
eberlm@66480
   632
          (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
eberlm@66480
   633
    unfolding infsetsum_def by simp
eberlm@66480
   634
  also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)"
lp15@67974
   635
  proof (rule Bochner_Integration.integral_cong [OF refl])
lp15@67974
   636
    show "\<And>x. x \<in> space (count_space A) \<Longrightarrow>
lp15@67974
   637
         (\<Sum>\<^sub>ay\<in>B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *\<^sub>R f (x, y)"
lp15@67974
   638
      using infsetsum_altdef'[of _ B'] 
lp15@67974
   639
      unfolding set_lebesgue_integral_def B'_def
lp15@67974
   640
      by auto 
lp15@67974
   641
  qed
eberlm@66480
   642
  also have "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^sub>M count_space B'))"
eberlm@66480
   643
    by (subst integral_fst [OF integrable]) auto
eberlm@66480
   644
  also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))"
eberlm@66480
   645
    by (intro Bochner_Integration.integral_cong)
eberlm@66480
   646
       (auto simp: pair_measure_countable indicator_def split: if_splits)
eberlm@66480
   647
  also have "\<dots> = infsetsum f (Sigma A B)"
lp15@67974
   648
    unfolding set_lebesgue_integral_def [symmetric]
eberlm@66480
   649
    by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
eberlm@66480
   650
  finally show ?thesis ..
eberlm@66480
   651
qed
eberlm@66480
   652
eberlm@66526
   653
lemma infsetsum_Sigma':
eberlm@66526
   654
  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
eberlm@66526
   655
  assumes [simp]: "countable A" and "\<And>i. countable (B i)"
eberlm@66526
   656
  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (Sigma A B)"
eberlm@66526
   657
  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) A = infsetsum (\<lambda>(x,y). f x y) (Sigma A B)"
eberlm@66526
   658
  using assms by (subst infsetsum_Sigma) auto
eberlm@66526
   659
eberlm@66480
   660
lemma infsetsum_Times:
eberlm@66480
   661
  fixes A :: "'a set" and B :: "'b set"
eberlm@66480
   662
  assumes [simp]: "countable A" and "countable B"
eberlm@66480
   663
  assumes summable: "f abs_summable_on (A \<times> B)"
eberlm@66480
   664
  shows   "infsetsum f (A \<times> B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) B) A"
eberlm@66480
   665
  using assms by (subst infsetsum_Sigma) auto
eberlm@66480
   666
eberlm@66480
   667
lemma infsetsum_Times':
eberlm@66480
   668
  fixes A :: "'a set" and B :: "'b set"
eberlm@66480
   669
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
eberlm@66480
   670
  assumes [simp]: "countable A" and [simp]: "countable B"
eberlm@66480
   671
  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (A \<times> B)"
eberlm@66480
   672
  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
eberlm@66480
   673
  using assms by (subst infsetsum_Times) auto
eberlm@66480
   674
eberlm@66480
   675
lemma infsetsum_swap:
eberlm@66480
   676
  fixes A :: "'a set" and B :: "'b set"
eberlm@66480
   677
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
eberlm@66480
   678
  assumes [simp]: "countable A" and [simp]: "countable B"
eberlm@66480
   679
  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on A \<times> B"
eberlm@66480
   680
  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
eberlm@66480
   681
proof -
eberlm@66480
   682
  from summable have summable': "(\<lambda>(x,y). f y x) abs_summable_on B \<times> A"
eberlm@66480
   683
    by (subst abs_summable_on_Times_swap) auto
eberlm@66480
   684
  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)"
eberlm@66480
   685
    by (auto simp: bij_betw_def inj_on_def)
eberlm@66480
   686
  have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
eberlm@66480
   687
    using summable by (subst infsetsum_Times) auto
eberlm@66480
   688
  also have "\<dots> = infsetsum (\<lambda>(x,y). f y x) (B \<times> A)"
eberlm@66480
   689
    by (subst infsetsum_reindex_bij_betw[OF bij, of "\<lambda>(x,y). f x y", symmetric])
eberlm@66480
   690
       (simp_all add: case_prod_unfold)
eberlm@66480
   691
  also have "\<dots> = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
eberlm@66480
   692
    using summable' by (subst infsetsum_Times) auto
eberlm@66480
   693
  finally show ?thesis .
eberlm@66480
   694
qed
eberlm@66480
   695
eberlm@68651
   696
theorem abs_summable_on_Sigma_iff:
eberlm@66526
   697
  assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
eberlm@66526
   698
  shows   "f abs_summable_on Sigma A B \<longleftrightarrow> 
eberlm@66526
   699
             (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
eberlm@66526
   700
             ((\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
eberlm@66526
   701
proof safe
eberlm@66526
   702
  define B' where "B' = (\<Union>x\<in>A. B x)"
eberlm@66526
   703
  have [simp]: "countable B'" 
eberlm@66526
   704
    unfolding B'_def using assms by auto
eberlm@66526
   705
  interpret pair_sigma_finite "count_space A" "count_space B'"
eberlm@66526
   706
    by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
eberlm@66526
   707
  {
eberlm@66526
   708
    assume *: "f abs_summable_on Sigma A B"
eberlm@66526
   709
    thus "(\<lambda>y. f (x, y)) abs_summable_on B x" if "x \<in> A" for x
eberlm@66526
   710
      using that by (rule abs_summable_on_Sigma_project2)
eberlm@66526
   711
eberlm@66526
   712
    have "set_integrable (count_space (A \<times> B')) (Sigma A B) (\<lambda>z. norm (f z))"
eberlm@66526
   713
      using abs_summable_on_normI[OF *]
eberlm@66526
   714
      by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
eberlm@66526
   715
    also have "count_space (A \<times> B') = count_space A \<Otimes>\<^sub>M count_space B'"
eberlm@66526
   716
      by (simp add: pair_measure_countable)
eberlm@66526
   717
    finally have "integrable (count_space A) 
eberlm@66526
   718
                    (\<lambda>x. lebesgue_integral (count_space B') 
eberlm@66526
   719
                      (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
lp15@67974
   720
      unfolding set_integrable_def by (rule integrable_fst')
eberlm@66526
   721
    also have "?this \<longleftrightarrow> integrable (count_space A)
eberlm@66526
   722
                    (\<lambda>x. lebesgue_integral (count_space B') 
eberlm@66526
   723
                      (\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
eberlm@66526
   724
      by (intro integrable_cong refl) (simp_all add: indicator_def)
eberlm@66526
   725
    also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
lp15@67974
   726
      unfolding set_lebesgue_integral_def [symmetric]
eberlm@66526
   727
      by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
eberlm@66526
   728
    also have "\<dots> \<longleftrightarrow> (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A"
eberlm@66526
   729
      by (simp add: abs_summable_on_def)
eberlm@66526
   730
    finally show \<dots> .
eberlm@66526
   731
  }
eberlm@66526
   732
  {
eberlm@66526
   733
    assume *: "\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x"
eberlm@66526
   734
    assume "(\<lambda>x. \<Sum>\<^sub>ay\<in>B x. norm (f (x, y))) abs_summable_on A"
eberlm@66526
   735
    also have "?this \<longleftrightarrow> (\<lambda>x. \<integral>y\<in>B x. norm (f (x, y)) \<partial>count_space B') abs_summable_on A"
eberlm@66526
   736
      by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
eberlm@66526
   737
    also have "\<dots> \<longleftrightarrow> (\<lambda>x. \<integral>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y)) \<partial>count_space B')
eberlm@66526
   738
                        abs_summable_on A" (is "_ \<longleftrightarrow> ?h abs_summable_on _")
lp15@67974
   739
      unfolding set_lebesgue_integral_def
eberlm@66526
   740
      by (intro abs_summable_on_cong) (auto simp: indicator_def)
eberlm@66526
   741
    also have "\<dots> \<longleftrightarrow> integrable (count_space A) ?h"
eberlm@66526
   742
      by (simp add: abs_summable_on_def)
eberlm@66526
   743
    finally have **: \<dots> .
eberlm@66526
   744
eberlm@66526
   745
    have "integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
eberlm@66526
   746
    proof (rule Fubini_integrable, goal_cases)
eberlm@66526
   747
      case 3
eberlm@66526
   748
      {
eberlm@66526
   749
        fix x assume x: "x \<in> A"
eberlm@66526
   750
        with * have "(\<lambda>y. f (x, y)) abs_summable_on B x"
eberlm@66526
   751
          by blast
eberlm@66526
   752
        also have "?this \<longleftrightarrow> integrable (count_space B') 
eberlm@66526
   753
                      (\<lambda>y. indicator (B x) y *\<^sub>R f (x, y))"
lp15@67974
   754
          unfolding set_integrable_def [symmetric]
lp15@67974
   755
         using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
eberlm@66526
   756
        also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) = 
eberlm@66526
   757
                     (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
eberlm@66526
   758
          using x by (auto simp: indicator_def)
eberlm@66526
   759
        finally have "integrable (count_space B')
eberlm@66526
   760
                        (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))" .
eberlm@66526
   761
      }
eberlm@66526
   762
      thus ?case by (auto simp: AE_count_space)
eberlm@66526
   763
    qed (insert **, auto simp: pair_measure_countable)
lp15@67974
   764
    moreover have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
eberlm@66526
   765
      by (simp add: pair_measure_countable)
lp15@67974
   766
    moreover have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
eberlm@66526
   767
                 f abs_summable_on Sigma A B"
eberlm@66526
   768
      by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
lp15@67974
   769
    ultimately show "f abs_summable_on Sigma A B"
lp15@67974
   770
      by (simp add: set_integrable_def)
eberlm@66526
   771
  }
eberlm@66526
   772
qed
eberlm@66526
   773
eberlm@66526
   774
lemma abs_summable_on_Sigma_project1:
eberlm@66526
   775
  assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
eberlm@66526
   776
  assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
eberlm@66526
   777
  shows   "(\<lambda>x. infsetsum (\<lambda>y. norm (f x y)) (B x)) abs_summable_on A"
eberlm@66526
   778
  using assms by (subst (asm) abs_summable_on_Sigma_iff) auto
eberlm@66526
   779
eberlm@66526
   780
lemma abs_summable_on_Sigma_project1':
eberlm@66526
   781
  assumes "(\<lambda>(x,y). f x y) abs_summable_on Sigma A B"
eberlm@66526
   782
  assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
eberlm@66526
   783
  shows   "(\<lambda>x. infsetsum (\<lambda>y. f x y) (B x)) abs_summable_on A"
eberlm@66526
   784
  by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
eberlm@66526
   785
        norm_infsetsum_bound)
eberlm@66526
   786
eberlm@68651
   787
theorem infsetsum_prod_PiE:
eberlm@66480
   788
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
eberlm@66480
   789
  assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
eberlm@66480
   790
  assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
eberlm@66480
   791
  shows   "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
eberlm@66480
   792
proof -
eberlm@66480
   793
  define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
eberlm@66480
   794
  from assms have [simp]: "countable (B' x)" for x
eberlm@66480
   795
    by (auto simp: B'_def)
eberlm@66480
   796
  then interpret product_sigma_finite "count_space \<circ> B'"
eberlm@66480
   797
    unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
eberlm@66480
   798
  have "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) =
eberlm@66480
   799
          (\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>count_space (PiE A B))"
eberlm@66480
   800
    by (simp add: infsetsum_def)
eberlm@66480
   801
  also have "PiE A B = PiE A B'"
eberlm@66480
   802
    by (intro PiE_cong) (simp_all add: B'_def)
eberlm@66480
   803
  hence "count_space (PiE A B) = count_space (PiE A B')"
eberlm@66480
   804
    by simp
eberlm@66480
   805
  also have "\<dots> = PiM A (count_space \<circ> B')"
eberlm@66480
   806
    unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
eberlm@66480
   807
  also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>A. infsetsum (f x) (B' x))"
eberlm@66480
   808
    by (subst product_integral_prod) 
eberlm@66480
   809
       (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def)
eberlm@66480
   810
  also have "\<dots> = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
eberlm@66480
   811
    by (intro prod.cong refl) (simp_all add: B'_def)
eberlm@66480
   812
  finally show ?thesis .
eberlm@66480
   813
qed
eberlm@66480
   814
eberlm@66480
   815
lemma infsetsum_uminus: "infsetsum (\<lambda>x. -f x) A = -infsetsum f A"
eberlm@66480
   816
  unfolding infsetsum_def abs_summable_on_def 
eberlm@66480
   817
  by (rule Bochner_Integration.integral_minus)
eberlm@66480
   818
eberlm@66480
   819
lemma infsetsum_add:
eberlm@66480
   820
  assumes "f abs_summable_on A" and "g abs_summable_on A"
eberlm@66480
   821
  shows   "infsetsum (\<lambda>x. f x + g x) A = infsetsum f A + infsetsum g A"
eberlm@66480
   822
  using assms unfolding infsetsum_def abs_summable_on_def 
eberlm@66480
   823
  by (rule Bochner_Integration.integral_add)
eberlm@66480
   824
eberlm@66480
   825
lemma infsetsum_diff:
eberlm@66480
   826
  assumes "f abs_summable_on A" and "g abs_summable_on A"
eberlm@66480
   827
  shows   "infsetsum (\<lambda>x. f x - g x) A = infsetsum f A - infsetsum g A"
eberlm@66480
   828
  using assms unfolding infsetsum_def abs_summable_on_def 
eberlm@66480
   829
  by (rule Bochner_Integration.integral_diff)
eberlm@66480
   830
eberlm@66480
   831
lemma infsetsum_scaleR_left:
eberlm@66480
   832
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   833
  shows   "infsetsum (\<lambda>x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c"
eberlm@66480
   834
  using assms unfolding infsetsum_def abs_summable_on_def 
eberlm@66480
   835
  by (rule Bochner_Integration.integral_scaleR_left)
eberlm@66480
   836
eberlm@66480
   837
lemma infsetsum_scaleR_right:
eberlm@66480
   838
  "infsetsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A"
eberlm@66480
   839
  unfolding infsetsum_def abs_summable_on_def 
eberlm@66480
   840
  by (subst Bochner_Integration.integral_scaleR_right) auto
eberlm@66480
   841
eberlm@66480
   842
lemma infsetsum_cmult_left:
eberlm@66480
   843
  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
eberlm@66480
   844
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   845
  shows   "infsetsum (\<lambda>x. f x * c) A = infsetsum f A * c"
eberlm@66480
   846
  using assms unfolding infsetsum_def abs_summable_on_def 
eberlm@66480
   847
  by (rule Bochner_Integration.integral_mult_left)
eberlm@66480
   848
eberlm@66480
   849
lemma infsetsum_cmult_right:
eberlm@66480
   850
  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
eberlm@66480
   851
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66480
   852
  shows   "infsetsum (\<lambda>x. c * f x) A = c * infsetsum f A"
eberlm@66480
   853
  using assms unfolding infsetsum_def abs_summable_on_def 
eberlm@66480
   854
  by (rule Bochner_Integration.integral_mult_right)
eberlm@66480
   855
eberlm@66526
   856
lemma infsetsum_cdiv:
eberlm@66526
   857
  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_field, second_countable_topology}"
eberlm@66526
   858
  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
eberlm@66526
   859
  shows   "infsetsum (\<lambda>x. f x / c) A = infsetsum f A / c"
eberlm@66526
   860
  using assms unfolding infsetsum_def abs_summable_on_def by auto
eberlm@66526
   861
eberlm@66526
   862
eberlm@66480
   863
(* TODO Generalise with bounded_linear *)
eberlm@66480
   864
eberlm@66526
   865
lemma
eberlm@66526
   866
  fixes f :: "'a \<Rightarrow> 'c :: {banach, real_normed_field, second_countable_topology}"
eberlm@66526
   867
  assumes [simp]: "countable A" and [simp]: "countable B"
eberlm@66526
   868
  assumes "f abs_summable_on A" and "g abs_summable_on B"
eberlm@66526
   869
  shows   abs_summable_on_product: "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
eberlm@66526
   870
    and   infsetsum_product: "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) =
eberlm@66526
   871
                                infsetsum f A * infsetsum g B"
eberlm@66526
   872
proof -
eberlm@66526
   873
  from assms show "(\<lambda>(x,y). f x * g y) abs_summable_on A \<times> B"
eberlm@66526
   874
    by (subst abs_summable_on_Sigma_iff)
eberlm@66526
   875
       (auto intro!: abs_summable_on_cmult_right simp: norm_mult infsetsum_cmult_right)
eberlm@66526
   876
  with assms show "infsetsum (\<lambda>(x,y). f x * g y) (A \<times> B) = infsetsum f A * infsetsum g B"
eberlm@66526
   877
    by (subst infsetsum_Sigma)
eberlm@66526
   878
       (auto simp: infsetsum_cmult_left infsetsum_cmult_right)
eberlm@66526
   879
qed
eberlm@66526
   880
eberlm@66480
   881
end