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 \Sums over Infinite Sets\ ``` 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" "\x. x \ A \ {x} \ sets M" ``` eberlm@66480 ` 16` ``` shows "sets M = Pow A" ``` eberlm@66480 ` 17` ```proof (intro equalityI subsetI) ``` eberlm@66480 ` 18` ``` fix X assume "X \ Pow A" ``` eberlm@66480 ` 19` ``` hence "(\x\X. {x}) \ sets M" ``` eberlm@66480 ` 20` ``` by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3)) ``` eberlm@66480 ` 21` ``` also have "(\x\X. {x}) = X" by auto ``` eberlm@66480 ` 22` ``` finally show "X \ sets M" . ``` eberlm@66480 ` 23` ```next ``` eberlm@66480 ` 24` ``` fix X assume "X \ sets M" ``` eberlm@66480 ` 25` ``` from sets.sets_into_space[OF this] and assms ``` eberlm@66480 ` 26` ``` show "X \ 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: "\x. x \ A \ {x} \ sets M" "\x. x \ A \ {x} \ sets N" ``` eberlm@66480 ` 32` ``` assumes A: "countable A" ``` eberlm@66480 ` 33` ``` assumes eq: "\a. a \ A \ 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 \ extensional A" ``` eberlm@66480 ` 44` ``` shows "PiE A (\x. {f x}) = {f}" ``` eberlm@66480 ` 45` ```proof - ``` eberlm@66480 ` 46` ``` { ``` eberlm@66480 ` 47` ``` fix g assume "g \ PiE A (\x. {f x})" ``` eberlm@66480 ` 48` ``` hence "g x = f x" for x ``` eberlm@66480 ` 49` ``` using assms by (cases "x \ 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 \ 'b set" ``` eberlm@66480 ` 57` ``` assumes "finite A" "\i. countable (B i)" ``` eberlm@66480 ` 58` ``` shows "PiM A (\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 (\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 \ PiE A B" ``` eberlm@66480 ` 65` ``` hence "PiE A (\x. {f x}) \ sets (Pi\<^sub>M A (\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 (\x. {f x}) = {f}" ``` eberlm@66480 ` 68` ``` by (intro PiE_singleton) (auto simp: PiE_def) ``` eberlm@66480 ` 69` ``` finally show "{f} \ sets (Pi\<^sub>M A (\i. count_space (B i)))" . ``` eberlm@66480 ` 70` ```next ``` eberlm@66480 ` 71` ``` interpret product_sigma_finite "(\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 \ PiE A B" ``` eberlm@66480 ` 75` ``` hence "{f} = PiE A (\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 (\i. count_space (B i))) \ = ``` eberlm@66480 ` 78` ``` (\i\A. emeasure (count_space (B i)) {f i})" ``` eberlm@66480 ` 79` ``` using f assms by (subst emeasure_PiM) auto ``` eberlm@66480 ` 80` ``` also have "\ = (\i\A. 1)" ``` eberlm@66480 ` 81` ``` by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto) ``` eberlm@66480 ` 82` ``` also have "\ = 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 (\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 \ 'b :: {banach, second_countable_topology}) \ 'a set \ bool" ``` eberlm@66480 ` 92` ``` (infix "abs'_summable'_on" 50) ``` eberlm@66480 ` 93` ``` where ``` eberlm@66480 ` 94` ``` "f abs_summable_on A \ integrable (count_space A) f" ``` eberlm@66480 ` 95` eberlm@66480 ` 96` eberlm@68651 ` 97` ```definition%important infsetsum :: ``` eberlm@66480 ` 98` ``` "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ '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 \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ``` eberlm@66480 ` 104` ``` ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) ``` eberlm@66480 ` 105` ```syntax ``` eberlm@66480 ` 106` ``` "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ``` eberlm@66480 ` 107` ``` ("(2\\<^sub>a_\_./ _)" [0, 51, 10] 10) ``` eberlm@66480 ` 108` ```translations \ \Beware of argument permutation!\ ``` eberlm@66480 ` 109` ``` "\\<^sub>ai\A. b" \ "CONST infsetsum (\i. b) A" ``` eberlm@66480 ` 110` eberlm@66480 ` 111` ```syntax (ASCII) ``` eberlm@66526 ` 112` ``` "_uinfsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ``` eberlm@66526 ` 113` ``` ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) ``` eberlm@66526 ` 114` ```syntax ``` eberlm@66526 ` 115` ``` "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" ``` eberlm@66526 ` 116` ``` ("(2\\<^sub>a_./ _)" [0, 10] 10) ``` eberlm@66526 ` 117` ```translations \ \Beware of argument permutation!\ ``` eberlm@66526 ` 118` ``` "\\<^sub>ai. b" \ "CONST infsetsum (\i. b) (CONST UNIV)" ``` eberlm@66526 ` 119` eberlm@66526 ` 120` ```syntax (ASCII) ``` eberlm@66480 ` 121` ``` "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ``` eberlm@66480 ` 122` ``` ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10) ``` eberlm@66480 ` 123` ```syntax ``` eberlm@66480 ` 124` ``` "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ``` eberlm@66480 ` 125` ``` ("(2\\<^sub>a_ | (_)./ _)" [0, 0, 10] 10) ``` eberlm@66480 ` 126` ```translations ``` eberlm@66480 ` 127` ``` "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}" ``` eberlm@66480 ` 128` eberlm@66480 ` 129` ```print_translation \ ``` 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` ```\ ``` eberlm@66480 ` 144` eberlm@66480 ` 145` eberlm@66480 ` 146` ```lemma restrict_count_space_subset: ``` eberlm@66480 ` 147` ``` "A \ B \ 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 \ 'b :: {banach, second_countable_topology}" ``` eberlm@66480 ` 152` ``` assumes "A \ B" ``` eberlm@66480 ` 153` ``` shows "f abs_summable_on A \ (\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 \ f \ 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 \ 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 \ B \ f abs_summable_on A \ 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` ``` "(\x. norm (f x)) abs_summable_on A \ 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 \ (\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]: "(\n. complex_of_real (f n)) abs_summable_on A \ 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 "\x. x \ A \ norm (f x) \ 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 "\x. x \ A \ norm (f x) \ 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 \ A" ``` eberlm@66526 ` 195` ``` with assms(2) have "norm (f x) \ g x" . ``` eberlm@66526 ` 196` ``` also have "\ \ norm (g x)" by simp ``` eberlm@66526 ` 197` ``` finally show "norm (f x) \ norm (g x)" . ``` eberlm@66526 ` 198` ```qed ``` eberlm@66526 ` 199` eberlm@66480 ` 200` ```lemma abs_summable_on_cong [cong]: ``` eberlm@66480 ` 201` ``` "(\x. x \ A \ f x = g x) \ A = B \ (f abs_summable_on A) \ (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 "\x. x \ A - B \ f x = 0" ``` eberlm@66480 ` 206` ``` assumes "\x. x \ B - A \ g x = 0" ``` eberlm@66480 ` 207` ``` assumes "\x. x \ A \ B \ f x = g x" ``` eberlm@66480 ` 208` ``` shows "f abs_summable_on A \ 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 \ 'b :: {banach, second_countable_topology}" ``` eberlm@66480 ` 215` ``` assumes "A \ B" ``` eberlm@66480 ` 216` ``` shows "f abs_summable_on A \ (\x. if x \ 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) \ summable (\n. if n \ A then norm (f n) else 0)" ``` eberlm@66480 ` 221` ```proof - ``` eberlm@66480 ` 222` ``` have "f abs_summable_on A \ summable (\x. norm (if x \ 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 "(\x. norm (if x \ A then f x else 0)) = (\x. if x \ 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) \ summable (\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 \ 'a :: {banach, second_countable_topology}" ``` lp15@67268 ` 236` ``` assumes "g abs_summable_on I" ``` lp15@67268 ` 237` ``` assumes "\n. \n\N; n \ I\ \ norm (f n) \ 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 (\x. x \ I \ norm (f x) \ 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) \ (\e>0. \N. \m\N. \n. (\x = m.. 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 \ 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 \ 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 \ 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 "\x. x \ A \ f x abs_summable_on B" ``` eberlm@67167 ` 282` ``` shows "(\y. \x\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 \ (\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 \ (\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 \ 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 \ (B - A))" ``` eberlm@67167 ` 296` ``` by (intro abs_summable_on_union assms abs_summable_on_finite) ``` eberlm@67167 ` 297` ``` also from assms have "A \ (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 "(\x. f (g x)) abs_summable_on A \ 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 "(\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 "(\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 \ (\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 "\ \ 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 \ (\x. f (g x)) abs_summable_on A \ 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 \ 'b set" ``` eberlm@66480 ` 332` ``` assumes "f abs_summable_on (Sigma A B)" "x \ A" ``` eberlm@66480 ` 333` ``` shows "(\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 \ (\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 "(\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 \ B \ (\(x,y). f (y,x)) abs_summable_on B \ A" ``` eberlm@66480 ` 348` ```proof - ``` eberlm@66480 ` 349` ``` have bij: "bij_betw (\(x,y). (y,x)) (B \ A) (A \ 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]: "(\_. 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 \ (\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 "(\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 "(\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 \ 0 \ f abs_summable_on A" ``` eberlm@66480 ` 375` ``` shows "(\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 \ 0 \ f abs_summable_on A" ``` eberlm@66480 ` 380` ``` shows "(\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 \ 'b :: {banach, real_normed_algebra, second_countable_topology}" ``` eberlm@66480 ` 385` ``` assumes "c \ 0 \ f abs_summable_on A" ``` eberlm@66480 ` 386` ``` shows "(\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 \ 'b :: {banach, real_normed_algebra, second_countable_topology}" ``` eberlm@66480 ` 391` ``` assumes "c \ 0 \ f abs_summable_on A" ``` eberlm@66480 ` 392` ``` shows "(\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 \ 'b \ 'c :: {real_normed_field,banach,second_countable_topology}" ``` eberlm@66568 ` 397` ``` assumes finite: "finite A" and countable: "\x. x \ A \ countable (B x)" ``` eberlm@66568 ` 398` ``` assumes summable: "\x. x \ A \ f x abs_summable_on B x" ``` eberlm@66568 ` 399` ``` shows "(\g. \x\A. f x (g x)) abs_summable_on PiE A B" ``` eberlm@66568 ` 400` ```proof - ``` eberlm@66568 ` 401` ``` define B' where "B' = (\x. if x \ 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 \ 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 \ B')) (\g. \x\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 \ 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` ``` "\f abs_summable_on A \ 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 \ B \ 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" "\x. x \ A \ f x \ 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 \ \" "\x. x \ A \ f x \ 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` ``` "(\x. x \ A \ f x = g x) \ A = B \ 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 (\_. 0) A = 0" ``` eberlm@66480 ` 449` ``` by (simp add: infsetsum_def) ``` eberlm@66480 ` 450` eberlm@66480 ` 451` ```lemma infsetsum_all_0: "(\x. x \ A \ f x = 0) \ infsetsum f A = 0" ``` eberlm@66480 ` 452` ``` by simp ``` eberlm@66480 ` 453` eberlm@67167 ` 454` ```lemma infsetsum_nonneg: "(\x. x \ A \ f x \ (0::real)) \ infsetsum f A \ 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 "\x. x \ A \ f x abs_summable_on B" ``` eberlm@67167 ` 459` ``` shows "(\x\A. \\<^sub>ay\B. f x y) = (\\<^sub>ay\B. \x\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 \ Re (infsetsum f A) = (\\<^sub>ax\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 \ Im (infsetsum f A) = (\\<^sub>ax\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 (\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 \ infsetsum f A = (\x\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 = (\n. if n \ A then f n else 0)" ``` eberlm@66480 ` 481` ```proof - ``` eberlm@66480 ` 482` ``` from assms have "infsetsum f A = (\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 "(\n. indicator A n *\<^sub>R f n) = (\n. if n \ 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 = (\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 "(\n. if n \ A then f n else 0) sums infsetsum f A" ``` eberlm@66480 ` 498` ```proof - ``` eberlm@66480 ` 499` ``` from assms have "summable (\n. if n \ A then norm (f n) else 0)" ``` eberlm@66480 ` 500` ``` by (simp add: abs_summable_on_nat_iff) ``` eberlm@66480 ` 501` ``` also have "(\n. if n \ A then norm (f n) else 0) = (\n. norm (if n \ A then f n else 0))" ``` eberlm@66480 ` 502` ``` by auto ``` eberlm@66480 ` 503` ``` finally have "summable (\n. if n \ 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 \ B = {}" ``` eberlm@66480 ` 516` ``` shows "infsetsum f (A \ 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 \ 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) \ 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) \ 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 \ B)" ``` eberlm@66480 ` 534` ``` shows "infsetsum f (A \ B) = infsetsum f A + infsetsum f B - infsetsum f (A \ B)" ``` eberlm@66480 ` 535` ```proof - ``` eberlm@66480 ` 536` ``` have "A \ B = A \ (B - A \ B)" ``` eberlm@66480 ` 537` ``` by auto ``` eberlm@66480 ` 538` ``` also have "infsetsum f \ = infsetsum f A + infsetsum f (B - A \ 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 \ B) = infsetsum f B - infsetsum f (A \ 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 (\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 (\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 "\x. x \ A - B \ f x = 0" ``` eberlm@66480 ` 564` ``` assumes "\x. x \ B - A \ g x = 0" ``` eberlm@66480 ` 565` ``` assumes "\x. x \ A \ B \ 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 \ real" ``` eberlm@66526 ` 573` ``` assumes "f abs_summable_on A" and "g abs_summable_on B" ``` eberlm@66526 ` 574` ``` assumes "\x. x \ A \ f x \ g x" ``` eberlm@66526 ` 575` ``` assumes "\x. x \ A - B \ f x \ 0" ``` eberlm@66526 ` 576` ``` assumes "\x. x \ B - A \ g x \ 0" ``` eberlm@66526 ` 577` ``` shows "infsetsum f A \ 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 \ real" ``` eberlm@66526 ` 583` ``` assumes "f abs_summable_on A" and "g abs_summable_on B" ``` eberlm@66526 ` 584` ``` assumes "\x. x \ A \ f x \ g x" ``` eberlm@66526 ` 585` ``` assumes "A \ B" ``` eberlm@66526 ` 586` ``` assumes "\x. x \ B - A \ g x \ 0" ``` eberlm@66526 ` 587` ``` shows "infsetsum f A \ infsetsum g B" ``` eberlm@66526 ` 588` ``` using \A \ B\ 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 \ real" ``` eberlm@66526 ` 592` ``` assumes "f abs_summable_on A" and "g abs_summable_on B" ``` eberlm@66526 ` 593` ``` assumes "\x. x \ A \ f x \ g x" ``` eberlm@66526 ` 594` ``` assumes "B \ A" ``` eberlm@66526 ` 595` ``` assumes "\x. x \ A - B \ f x \ 0" ``` eberlm@66526 ` 596` ``` shows "infsetsum f A \ infsetsum g B" ``` eberlm@66526 ` 597` ``` using \B \ A\ by (intro infsetsum_mono_neutral assms) auto ``` eberlm@66526 ` 598` eberlm@66526 ` 599` ```lemma infsetsum_mono: ``` eberlm@66526 ` 600` ``` fixes f g :: "'a \ real" ``` eberlm@66526 ` 601` ``` assumes "f abs_summable_on A" and "g abs_summable_on A" ``` eberlm@66526 ` 602` ``` assumes "\x. x \ A \ f x \ g x" ``` eberlm@66526 ` 603` ``` shows "infsetsum f A \ 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) \ infsetsum (\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 \ 'b set" ``` eberlm@66480 ` 613` ``` assumes [simp]: "countable A" 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 (\x. infsetsum (\y. f (x, y)) (B x)) A" ``` eberlm@66480 ` 616` ```proof - ``` eberlm@66480 ` 617` ``` define B' where "B' = (\i\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 \ B')) (\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 \ integrable (count_space A \\<^sub>M count_space B') (\(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: \ . ``` eberlm@66480 ` 630` ``` ``` eberlm@66480 ` 631` ``` have "infsetsum (\x. infsetsum (\y. f (x, y)) (B x)) A = ``` eberlm@66480 ` 632` ``` (\x. infsetsum (\y. f (x, y)) (B x) \count_space A)" ``` eberlm@66480 ` 633` ``` unfolding infsetsum_def by simp ``` eberlm@66480 ` 634` ``` also have "\ = (\x. \y. indicator (B x) y *\<^sub>R f (x, y) \count_space B' \count_space A)" ``` lp15@67974 ` 635` ``` proof (rule Bochner_Integration.integral_cong [OF refl]) ``` lp15@67974 ` 636` ``` show "\x. x \ space (count_space A) \ ``` lp15@67974 ` 637` ``` (\\<^sub>ay\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 "\ = (\(x,y). indicator (B x) y *\<^sub>R f (x, y) \(count_space A \\<^sub>M count_space B'))" ``` eberlm@66480 ` 643` ``` by (subst integral_fst [OF integrable]) auto ``` eberlm@66480 ` 644` ``` also have "\ = (\z. indicator (Sigma A B) z *\<^sub>R f z \count_space (A \ 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 "\ = 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 \ 'b set" ``` eberlm@66526 ` 655` ``` assumes [simp]: "countable A" and "\i. countable (B i)" ``` eberlm@66526 ` 656` ``` assumes summable: "(\(x,y). f x y) abs_summable_on (Sigma A B)" ``` eberlm@66526 ` 657` ``` shows "infsetsum (\x. infsetsum (\y. f x y) (B x)) A = infsetsum (\(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 \ B)" ``` eberlm@66480 ` 664` ``` shows "infsetsum f (A \ B) = infsetsum (\x. infsetsum (\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 \ 'b \ 'c :: {banach, second_countable_topology}" ``` eberlm@66480 ` 670` ``` assumes [simp]: "countable A" and [simp]: "countable B" ``` eberlm@66480 ` 671` ``` assumes summable: "(\(x,y). f x y) abs_summable_on (A \ B)" ``` eberlm@66480 ` 672` ``` shows "infsetsum (\x. infsetsum (\y. f x y) B) A = infsetsum (\(x,y). f x y) (A \ 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 \ 'b \ 'c :: {banach, second_countable_topology}" ``` eberlm@66480 ` 678` ``` assumes [simp]: "countable A" and [simp]: "countable B" ``` eberlm@66480 ` 679` ``` assumes summable: "(\(x,y). f x y) abs_summable_on A \ B" ``` eberlm@66480 ` 680` ``` shows "infsetsum (\x. infsetsum (\y. f x y) B) A = infsetsum (\y. infsetsum (\x. f x y) A) B" ``` eberlm@66480 ` 681` ```proof - ``` eberlm@66480 ` 682` ``` from summable have summable': "(\(x,y). f y x) abs_summable_on B \ A" ``` eberlm@66480 ` 683` ``` by (subst abs_summable_on_Times_swap) auto ``` eberlm@66480 ` 684` ``` have bij: "bij_betw (\(x, y). (y, x)) (B \ A) (A \ B)" ``` eberlm@66480 ` 685` ``` by (auto simp: bij_betw_def inj_on_def) ``` eberlm@66480 ` 686` ``` have "infsetsum (\x. infsetsum (\y. f x y) B) A = infsetsum (\(x,y). f x y) (A \ B)" ``` eberlm@66480 ` 687` ``` using summable by (subst infsetsum_Times) auto ``` eberlm@66480 ` 688` ``` also have "\ = infsetsum (\(x,y). f y x) (B \ A)" ``` eberlm@66480 ` 689` ``` by (subst infsetsum_reindex_bij_betw[OF bij, of "\(x,y). f x y", symmetric]) ``` eberlm@66480 ` 690` ``` (simp_all add: case_prod_unfold) ``` eberlm@66480 ` 691` ``` also have "\ = infsetsum (\y. infsetsum (\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 "\x. x \ A \ countable (B x)" ``` eberlm@66526 ` 698` ``` shows "f abs_summable_on Sigma A B \ ``` eberlm@66526 ` 699` ``` (\x\A. (\y. f (x, y)) abs_summable_on B x) \ ``` eberlm@66526 ` 700` ``` ((\x. infsetsum (\y. norm (f (x, y))) (B x)) abs_summable_on A)" ``` eberlm@66526 ` 701` ```proof safe ``` eberlm@66526 ` 702` ``` define B' where "B' = (\x\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 "(\y. f (x, y)) abs_summable_on B x" if "x \ 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 \ B')) (Sigma A B) (\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 \ B') = count_space A \\<^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` ``` (\x. lebesgue_integral (count_space B') ``` eberlm@66526 ` 719` ``` (\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 \ integrable (count_space A) ``` eberlm@66526 ` 722` ``` (\x. lebesgue_integral (count_space B') ``` eberlm@66526 ` 723` ``` (\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 "\ \ integrable (count_space A) (\x. infsetsum (\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 "\ \ (\x. infsetsum (\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 \ . ``` eberlm@66526 ` 731` ``` } ``` eberlm@66526 ` 732` ``` { ``` eberlm@66526 ` 733` ``` assume *: "\x\A. (\y. f (x, y)) abs_summable_on B x" ``` eberlm@66526 ` 734` ``` assume "(\x. \\<^sub>ay\B x. norm (f (x, y))) abs_summable_on A" ``` eberlm@66526 ` 735` ``` also have "?this \ (\x. \y\B x. norm (f (x, y)) \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 "\ \ (\x. \y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y)) \count_space B') ``` eberlm@66526 ` 738` ``` abs_summable_on A" (is "_ \ ?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 "\ \ integrable (count_space A) ?h" ``` eberlm@66526 ` 742` ``` by (simp add: abs_summable_on_def) ``` eberlm@66526 ` 743` ``` finally have **: \ . ``` eberlm@66526 ` 744` eberlm@66526 ` 745` ``` have "integrable (count_space A \\<^sub>M count_space B') (\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 \ A" ``` eberlm@66526 ` 750` ``` with * have "(\y. f (x, y)) abs_summable_on B x" ``` eberlm@66526 ` 751` ``` by blast ``` eberlm@66526 ` 752` ``` also have "?this \ integrable (count_space B') ``` eberlm@66526 ` 753` ``` (\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 "(\y. indicator (B x) y *\<^sub>R f (x, y)) = ``` eberlm@66526 ` 757` ``` (\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` ``` (\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 \\<^sub>M count_space B' = count_space (A \ B')" ``` eberlm@66526 ` 765` ``` by (simp add: pair_measure_countable) ``` lp15@67974 ` 766` ``` moreover have "set_integrable (count_space (A \ B')) (Sigma A B) f \ ``` 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 "(\(x,y). f x y) abs_summable_on Sigma A B" ``` eberlm@66526 ` 776` ``` assumes [simp]: "countable A" and "\x. x \ A \ countable (B x)" ``` eberlm@66526 ` 777` ``` shows "(\x. infsetsum (\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 "(\(x,y). f x y) abs_summable_on Sigma A B" ``` eberlm@66526 ` 782` ``` assumes [simp]: "countable A" and "\x. x \ A \ countable (B x)" ``` eberlm@66526 ` 783` ``` shows "(\x. infsetsum (\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 \ 'b \ 'c :: {real_normed_field,banach,second_countable_topology}" ``` eberlm@66480 ` 789` ``` assumes finite: "finite A" and countable: "\x. x \ A \ countable (B x)" ``` eberlm@66480 ` 790` ``` assumes summable: "\x. x \ A \ f x abs_summable_on B x" ``` eberlm@66480 ` 791` ``` shows "infsetsum (\g. \x\A. f x (g x)) (PiE A B) = (\x\A. infsetsum (f x) (B x))" ``` eberlm@66480 ` 792` ```proof - ``` eberlm@66480 ` 793` ``` define B' where "B' = (\x. if x \ 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 \ B'" ``` eberlm@66480 ` 797` ``` unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable) ``` eberlm@66480 ` 798` ``` have "infsetsum (\g. \x\A. f x (g x)) (PiE A B) = ``` eberlm@66480 ` 799` ``` (\g. (\x\A. f x (g x)) \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 "\ = PiM A (count_space \ B')" ``` eberlm@66480 ` 806` ``` unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all ``` eberlm@66480 ` 807` ``` also have "(\g. (\x\A. f x (g x)) \\) = (\x\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 "\ = (\x\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 (\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 (\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 (\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 \ 0 \ f abs_summable_on A" ``` eberlm@66480 ` 833` ``` shows "infsetsum (\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 (\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 \ 'b :: {banach, real_normed_algebra, second_countable_topology}" ``` eberlm@66480 ` 844` ``` assumes "c \ 0 \ f abs_summable_on A" ``` eberlm@66480 ` 845` ``` shows "infsetsum (\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 \ 'b :: {banach, real_normed_algebra, second_countable_topology}" ``` eberlm@66480 ` 851` ``` assumes "c \ 0 \ f abs_summable_on A" ``` eberlm@66480 ` 852` ``` shows "infsetsum (\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 \ 'b :: {banach, real_normed_field, second_countable_topology}" ``` eberlm@66526 ` 858` ``` assumes "c \ 0 \ f abs_summable_on A" ``` eberlm@66526 ` 859` ``` shows "infsetsum (\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 \ '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: "(\(x,y). f x * g y) abs_summable_on A \ B" ``` eberlm@66526 ` 870` ``` and infsetsum_product: "infsetsum (\(x,y). f x * g y) (A \ B) = ``` eberlm@66526 ` 871` ``` infsetsum f A * infsetsum g B" ``` eberlm@66526 ` 872` ```proof - ``` eberlm@66526 ` 873` ``` from assms show "(\(x,y). f x * g y) abs_summable_on A \ 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 (\(x,y). f x * g y) (A \ 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 ```