author | Manuel Eberl <eberlm@in.tum.de> |
Mon, 21 Aug 2017 20:49:15 +0200 | |
changeset 66480 | 4b8d1df8933b |
child 66526 | 322120e880c5 |
permissions | -rw-r--r-- |
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
1 |
(* |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
2 |
Title: HOL/Analysis/Infinite_Set_Sum.thy |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
3 |
Author: Manuel Eberl, TU München |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
4 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
5 |
A theory of sums over possible infinite sets. (Only works for absolute summability) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
6 |
*) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
7 |
section \<open>Sums over infinite sets\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
8 |
theory Infinite_Set_Sum |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
9 |
imports Set_Integral |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
10 |
begin |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
11 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
12 |
(* TODO Move *) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
13 |
lemma sets_eq_countable: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
14 |
assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
15 |
shows "sets M = Pow A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
16 |
proof (intro equalityI subsetI) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
17 |
fix X assume "X \<in> Pow A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
18 |
hence "(\<Union>x\<in>X. {x}) \<in> sets M" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
19 |
by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3)) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
20 |
also have "(\<Union>x\<in>X. {x}) = X" by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
21 |
finally show "X \<in> sets M" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
22 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
23 |
fix X assume "X \<in> sets M" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
24 |
from sets.sets_into_space[OF this] and assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
25 |
show "X \<in> Pow A" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
26 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
27 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
28 |
lemma measure_eqI_countable': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
29 |
assumes spaces: "space M = A" "space N = A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
30 |
assumes sets: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
31 |
assumes A: "countable A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
32 |
assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
33 |
shows "M = N" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
34 |
proof (rule measure_eqI_countable) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
35 |
show "sets M = Pow A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
36 |
by (intro sets_eq_countable assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
37 |
show "sets N = Pow A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
38 |
by (intro sets_eq_countable assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
39 |
qed fact+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
40 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
41 |
lemma PiE_singleton: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
42 |
assumes "f \<in> extensional A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
43 |
shows "PiE A (\<lambda>x. {f x}) = {f}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
44 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
45 |
{ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
46 |
fix g assume "g \<in> PiE A (\<lambda>x. {f x})" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
47 |
hence "g x = f x" for x |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
48 |
using assms by (cases "x \<in> A") (auto simp: extensional_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
49 |
hence "g = f" by (simp add: fun_eq_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
50 |
} |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
51 |
thus ?thesis using assms by (auto simp: extensional_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
52 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
53 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
54 |
lemma count_space_PiM_finite: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
55 |
fixes B :: "'a \<Rightarrow> 'b set" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
56 |
assumes "finite A" "\<And>i. countable (B i)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
57 |
shows "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
58 |
proof (rule measure_eqI_countable') |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
59 |
show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
60 |
by (simp add: space_PiM) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
61 |
show "space (count_space (PiE A B)) = PiE A B" by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
62 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
63 |
fix f assume f: "f \<in> PiE A B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
64 |
hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
65 |
by (intro sets_PiM_I_finite assms) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
66 |
also from f have "PiE A (\<lambda>x. {f x}) = {f}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
67 |
by (intro PiE_singleton) (auto simp: PiE_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
68 |
finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
69 |
next |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
70 |
interpret product_sigma_finite "(\<lambda>i. count_space (B i))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
71 |
by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
72 |
thm sigma_finite_measure_count_space |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
73 |
fix f assume f: "f \<in> PiE A B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
74 |
hence "{f} = PiE A (\<lambda>x. {f x})" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
75 |
by (intro PiE_singleton [symmetric]) (auto simp: PiE_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
76 |
also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
77 |
(\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
78 |
using f assms by (subst emeasure_PiM) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
79 |
also have "\<dots> = (\<Prod>i\<in>A. 1)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
80 |
by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
81 |
also have "\<dots> = emeasure (count_space (PiE A B)) {f}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
82 |
using f by (subst emeasure_count_space_finite) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
83 |
finally show "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) {f} = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
84 |
emeasure (count_space (Pi\<^sub>E A B)) {f}" . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
85 |
qed (simp_all add: countable_PiE assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
86 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
87 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
88 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
89 |
definition abs_summable_on :: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
90 |
"('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
91 |
(infix "abs'_summable'_on" 50) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
92 |
where |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
93 |
"f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
94 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
95 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
96 |
definition infsetsum :: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
97 |
"('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
98 |
where |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
99 |
"infsetsum f A = lebesgue_integral (count_space A) f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
100 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
101 |
syntax (ASCII) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
102 |
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
103 |
("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
104 |
syntax |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
105 |
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
106 |
("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
107 |
translations \<comment> \<open>Beware of argument permutation!\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
108 |
"\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
109 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
110 |
syntax (ASCII) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
111 |
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
112 |
("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
113 |
syntax |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
114 |
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
115 |
("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
116 |
translations |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
117 |
"\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
118 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
119 |
print_translation \<open> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
120 |
let |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
121 |
fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
122 |
if x <> y then raise Match |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
123 |
else |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
124 |
let |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
125 |
val x' = Syntax_Trans.mark_bound_body (x, Tx); |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
126 |
val t' = subst_bound (x', t); |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
127 |
val P' = subst_bound (x', P); |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
128 |
in |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
129 |
Syntax.const @{syntax_const "_qinfsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
130 |
end |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
131 |
| sum_tr' _ = raise Match; |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
132 |
in [(@{const_syntax infsetsum}, K sum_tr')] end |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
133 |
\<close> |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
134 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
135 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
136 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
137 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
138 |
lemma restrict_count_space_subset: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
139 |
"A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
140 |
by (subst restrict_count_space) (simp_all add: Int_absorb2) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
141 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
142 |
lemma abs_summable_on_restrict: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
143 |
fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
144 |
assumes "A \<subseteq> B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
145 |
shows "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) abs_summable_on B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
146 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
147 |
have "count_space A = restrict_space (count_space B) A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
148 |
by (rule restrict_count_space_subset [symmetric]) fact+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
149 |
also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
150 |
by (subst integrable_restrict_space) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
151 |
finally show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
152 |
unfolding abs_summable_on_def . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
153 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
154 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
155 |
lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
156 |
by (subst abs_summable_on_restrict[of _ UNIV]) (auto simp: abs_summable_on_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
157 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
158 |
lemma abs_summable_on_altdef': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
159 |
"A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
160 |
by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
161 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
162 |
lemma abs_summable_on_cong [cong]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
163 |
"(\<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)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
164 |
unfolding abs_summable_on_def by (intro integrable_cong) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
165 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
166 |
lemma abs_summable_on_cong_neutral: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
167 |
assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
168 |
assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
169 |
assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
170 |
shows "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
171 |
unfolding abs_summable_on_altdef using assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
172 |
by (intro Bochner_Integration.integrable_cong refl) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
173 |
(auto simp: indicator_def split: if_splits) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
174 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
175 |
lemma abs_summable_on_restrict': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
176 |
fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
177 |
assumes "A \<subseteq> B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
178 |
shows "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. if x \<in> A then f x else 0) abs_summable_on B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
179 |
by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
180 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
181 |
lemma abs_summable_on_nat_iff: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
182 |
"f abs_summable_on (A :: nat set) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
183 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
184 |
have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> A then f x else 0))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
185 |
by (subst abs_summable_on_restrict'[of _ UNIV]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
186 |
(simp_all add: abs_summable_on_def integrable_count_space_nat_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
187 |
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)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
188 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
189 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
190 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
191 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
192 |
lemma abs_summable_on_nat_iff': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
193 |
"f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
194 |
by (subst abs_summable_on_nat_iff) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
195 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
196 |
lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
197 |
unfolding abs_summable_on_def by (rule integrable_count_space) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
198 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
199 |
lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
200 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
201 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
202 |
lemma abs_summable_on_subset: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
203 |
assumes "f abs_summable_on B" and "A \<subseteq> B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
204 |
shows "f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
205 |
unfolding abs_summable_on_altdef |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
206 |
by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
207 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
208 |
lemma abs_summable_on_union [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
209 |
assumes "f abs_summable_on A" and "f abs_summable_on B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
210 |
shows "f abs_summable_on (A \<union> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
211 |
using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
212 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
213 |
lemma abs_summable_on_reindex_bij_betw: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
214 |
assumes "bij_betw g A B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
215 |
shows "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
216 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
217 |
have *: "count_space B = distr (count_space A) (count_space B) g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
218 |
by (rule distr_bij_count_space [symmetric]) fact |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
219 |
show ?thesis unfolding abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
220 |
by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
221 |
(insert assms, auto simp: bij_betw_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
222 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
223 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
224 |
lemma abs_summable_on_reindex: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
225 |
assumes "(\<lambda>x. f (g x)) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
226 |
shows "f abs_summable_on (g ` A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
227 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
228 |
define g' where "g' = inv_into A g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
229 |
from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
230 |
by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
231 |
also have "?this \<longleftrightarrow> (\<lambda>x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
232 |
by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
233 |
also have "\<dots> \<longleftrightarrow> f abs_summable_on (g ` A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
234 |
by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
235 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
236 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
237 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
238 |
lemma abs_summable_reindex_iff: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
239 |
"inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
240 |
by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
241 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
242 |
lemma abs_summable_on_Sigma_project: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
243 |
fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
244 |
assumes "f abs_summable_on (Sigma A B)" "x \<in> A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
245 |
shows "(\<lambda>y. f (x, y)) abs_summable_on (B x)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
246 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
247 |
from assms(2) have "f abs_summable_on (Sigma {x} B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
248 |
by (intro abs_summable_on_subset [OF assms(1)]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
249 |
also have "?this \<longleftrightarrow> (\<lambda>z. f (x, snd z)) abs_summable_on (Sigma {x} B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
250 |
by (rule abs_summable_on_cong) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
251 |
finally have "(\<lambda>y. f (x, y)) abs_summable_on (snd ` Sigma {x} B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
252 |
by (rule abs_summable_on_reindex) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
253 |
also have "snd ` Sigma {x} B = B x" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
254 |
using assms by (auto simp: image_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
255 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
256 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
257 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
258 |
lemma abs_summable_on_Times_swap: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
259 |
"f abs_summable_on A \<times> B \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) abs_summable_on B \<times> A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
260 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
261 |
have bij: "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
262 |
by (auto simp: bij_betw_def inj_on_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
263 |
show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
264 |
by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
265 |
(simp_all add: case_prod_unfold) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
266 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
267 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
268 |
lemma abs_summable_on_0 [simp, intro]: "(\<lambda>_. 0) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
269 |
by (simp add: abs_summable_on_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
270 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
271 |
lemma abs_summable_on_uminus [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
272 |
"f abs_summable_on A \<Longrightarrow> (\<lambda>x. -f x) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
273 |
unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
274 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
275 |
lemma abs_summable_on_add [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
276 |
assumes "f abs_summable_on A" and "g abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
277 |
shows "(\<lambda>x. f x + g x) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
278 |
using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
279 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
280 |
lemma abs_summable_on_diff [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
281 |
assumes "f abs_summable_on A" and "g abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
282 |
shows "(\<lambda>x. f x - g x) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
283 |
using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
284 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
285 |
lemma abs_summable_on_scaleR_left [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
286 |
assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
287 |
shows "(\<lambda>x. f x *\<^sub>R c) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
288 |
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
289 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
290 |
lemma abs_summable_on_scaleR_right [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
291 |
assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
292 |
shows "(\<lambda>x. c *\<^sub>R f x) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
293 |
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
294 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
295 |
lemma abs_summable_on_cmult_right [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
296 |
fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
297 |
assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
298 |
shows "(\<lambda>x. c * f x) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
299 |
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
300 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
301 |
lemma abs_summable_on_cmult_left [intro]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
302 |
fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
303 |
assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
304 |
shows "(\<lambda>x. f x * c) abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
305 |
using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
306 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
307 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
308 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
309 |
lemma not_summable_infsetsum_eq: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
310 |
"\<not>f abs_summable_on A \<Longrightarrow> infsetsum f A = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
311 |
by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
312 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
313 |
lemma infsetsum_altdef: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
314 |
"infsetsum f A = set_lebesgue_integral (count_space UNIV) A f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
315 |
by (subst integral_restrict_space [symmetric]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
316 |
(auto simp: restrict_count_space_subset infsetsum_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
317 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
318 |
lemma infsetsum_altdef': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
319 |
"A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
320 |
by (subst integral_restrict_space [symmetric]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
321 |
(auto simp: restrict_count_space_subset infsetsum_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
322 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
323 |
lemma infsetsum_cong [cong]: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
324 |
"(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
325 |
unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
326 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
327 |
lemma infsetsum_0 [simp]: "infsetsum (\<lambda>_. 0) A = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
328 |
by (simp add: infsetsum_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
329 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
330 |
lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
331 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
332 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
333 |
lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
334 |
by (simp add: infsetsum_def lebesgue_integral_count_space_finite) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
335 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
336 |
lemma infsetsum_nat: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
337 |
assumes "f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
338 |
shows "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
339 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
340 |
from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
341 |
unfolding infsetsum_altdef abs_summable_on_altdef by (subst integral_count_space_nat) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
342 |
also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
343 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
344 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
345 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
346 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
347 |
lemma infsetsum_nat': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
348 |
assumes "f abs_summable_on UNIV" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
349 |
shows "infsetsum f UNIV = (\<Sum>n. f n)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
350 |
using assms by (subst infsetsum_nat) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
351 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
352 |
lemma sums_infsetsum_nat: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
353 |
assumes "f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
354 |
shows "(\<lambda>n. if n \<in> A then f n else 0) sums infsetsum f A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
355 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
356 |
from assms have "summable (\<lambda>n. if n \<in> A then norm (f n) else 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
357 |
by (simp add: abs_summable_on_nat_iff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
358 |
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))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
359 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
360 |
finally have "summable (\<lambda>n. if n \<in> A then f n else 0)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
361 |
by (rule summable_norm_cancel) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
362 |
with assms show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
363 |
by (auto simp: sums_iff infsetsum_nat) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
364 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
365 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
366 |
lemma sums_infsetsum_nat': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
367 |
assumes "f abs_summable_on UNIV" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
368 |
shows "f sums infsetsum f UNIV" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
369 |
using sums_infsetsum_nat [OF assms] by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
370 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
371 |
lemma infsetsum_Un_disjoint: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
372 |
assumes "f abs_summable_on A" "f abs_summable_on B" "A \<inter> B = {}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
373 |
shows "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
374 |
using assms unfolding infsetsum_altdef abs_summable_on_altdef |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
375 |
by (subst set_integral_Un) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
376 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
377 |
lemma infsetsum_Diff: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
378 |
assumes "f abs_summable_on B" "A \<subseteq> B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
379 |
shows "infsetsum f (B - A) = infsetsum f B - infsetsum f A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
380 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
381 |
have "infsetsum f ((B - A) \<union> A) = infsetsum f (B - A) + infsetsum f A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
382 |
using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
383 |
also from assms(2) have "(B - A) \<union> A = B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
384 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
385 |
ultimately show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
386 |
by (simp add: algebra_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
387 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
388 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
389 |
lemma infsetsum_Un_Int: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
390 |
assumes "f abs_summable_on (A \<union> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
391 |
shows "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B - infsetsum f (A \<inter> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
392 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
393 |
have "A \<union> B = A \<union> (B - A \<inter> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
394 |
by auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
395 |
also have "infsetsum f \<dots> = infsetsum f A + infsetsum f (B - A \<inter> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
396 |
by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
397 |
also have "infsetsum f (B - A \<inter> B) = infsetsum f B - infsetsum f (A \<inter> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
398 |
by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
399 |
finally show ?thesis |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
400 |
by (simp add: algebra_simps) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
401 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
402 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
403 |
lemma infsetsum_reindex_bij_betw: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
404 |
assumes "bij_betw g A B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
405 |
shows "infsetsum (\<lambda>x. f (g x)) A = infsetsum f B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
406 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
407 |
have *: "count_space B = distr (count_space A) (count_space B) g" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
408 |
by (rule distr_bij_count_space [symmetric]) fact |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
409 |
show ?thesis unfolding infsetsum_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
410 |
by (subst *, subst integral_distr[of _ _ "count_space B"]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
411 |
(insert assms, auto simp: bij_betw_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
412 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
413 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
414 |
lemma infsetsum_reindex: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
415 |
assumes "inj_on g A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
416 |
shows "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
417 |
by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
418 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
419 |
lemma infsetsum_cong_neutral: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
420 |
assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
421 |
assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
422 |
assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
423 |
shows "infsetsum f A = infsetsum g B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
424 |
unfolding infsetsum_altdef using assms |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
425 |
by (intro Bochner_Integration.integral_cong refl) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
426 |
(auto simp: indicator_def split: if_splits) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
427 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
428 |
lemma infsetsum_Sigma: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
429 |
fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
430 |
assumes [simp]: "countable A" and "\<And>i. countable (B i)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
431 |
assumes summable: "f abs_summable_on (Sigma A B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
432 |
shows "infsetsum f (Sigma A B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
433 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
434 |
define B' where "B' = (\<Union>i\<in>A. B i)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
435 |
have [simp]: "countable B'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
436 |
unfolding B'_def by (intro countable_UN assms) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
437 |
interpret pair_sigma_finite "count_space A" "count_space B'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
438 |
by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+ |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
439 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
440 |
have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
441 |
using summable by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
442 |
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))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
443 |
by (intro Bochner_Integration.integrable_cong) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
444 |
(auto simp: pair_measure_countable indicator_def split: if_splits) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
445 |
finally have integrable: \<dots> . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
446 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
447 |
have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
448 |
(\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
449 |
unfolding infsetsum_def by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
450 |
also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
451 |
by (intro Bochner_Integration.integral_cong infsetsum_altdef'[of _ B'] refl) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
452 |
(auto simp: B'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
453 |
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'))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
454 |
by (subst integral_fst [OF integrable]) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
455 |
also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
456 |
by (intro Bochner_Integration.integral_cong) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
457 |
(auto simp: pair_measure_countable indicator_def split: if_splits) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
458 |
also have "\<dots> = infsetsum f (Sigma A B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
459 |
by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
460 |
finally show ?thesis .. |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
461 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
462 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
463 |
lemma infsetsum_Times: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
464 |
fixes A :: "'a set" and B :: "'b set" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
465 |
assumes [simp]: "countable A" and "countable B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
466 |
assumes summable: "f abs_summable_on (A \<times> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
467 |
shows "infsetsum f (A \<times> B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) B) A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
468 |
using assms by (subst infsetsum_Sigma) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
469 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
470 |
lemma infsetsum_Times': |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
471 |
fixes A :: "'a set" and B :: "'b set" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
472 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
473 |
assumes [simp]: "countable A" and [simp]: "countable B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
474 |
assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (A \<times> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
475 |
shows "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
476 |
using assms by (subst infsetsum_Times) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
477 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
478 |
lemma infsetsum_swap: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
479 |
fixes A :: "'a set" and B :: "'b set" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
480 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
481 |
assumes [simp]: "countable A" and [simp]: "countable B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
482 |
assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on A \<times> B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
483 |
shows "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
484 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
485 |
from summable have summable': "(\<lambda>(x,y). f y x) abs_summable_on B \<times> A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
486 |
by (subst abs_summable_on_Times_swap) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
487 |
have bij: "bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
488 |
by (auto simp: bij_betw_def inj_on_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
489 |
have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
490 |
using summable by (subst infsetsum_Times) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
491 |
also have "\<dots> = infsetsum (\<lambda>(x,y). f y x) (B \<times> A)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
492 |
by (subst infsetsum_reindex_bij_betw[OF bij, of "\<lambda>(x,y). f x y", symmetric]) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
493 |
(simp_all add: case_prod_unfold) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
494 |
also have "\<dots> = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
495 |
using summable' by (subst infsetsum_Times) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
496 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
497 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
498 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
499 |
lemma infsetsum_prod_PiE: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
500 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
501 |
assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
502 |
assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
503 |
shows "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsetsum (f x) (B x))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
504 |
proof - |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
505 |
define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
506 |
from assms have [simp]: "countable (B' x)" for x |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
507 |
by (auto simp: B'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
508 |
then interpret product_sigma_finite "count_space \<circ> B'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
509 |
unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
510 |
have "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
511 |
(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>count_space (PiE A B))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
512 |
by (simp add: infsetsum_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
513 |
also have "PiE A B = PiE A B'" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
514 |
by (intro PiE_cong) (simp_all add: B'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
515 |
hence "count_space (PiE A B) = count_space (PiE A B')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
516 |
by simp |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
517 |
also have "\<dots> = PiM A (count_space \<circ> B')" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
518 |
unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
519 |
also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>A. infsetsum (f x) (B' x))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
520 |
by (subst product_integral_prod) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
521 |
(insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
522 |
also have "\<dots> = (\<Prod>x\<in>A. infsetsum (f x) (B x))" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
523 |
by (intro prod.cong refl) (simp_all add: B'_def) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
524 |
finally show ?thesis . |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
525 |
qed |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
526 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
527 |
lemma infsetsum_uminus: "infsetsum (\<lambda>x. -f x) A = -infsetsum f A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
528 |
unfolding infsetsum_def abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
529 |
by (rule Bochner_Integration.integral_minus) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
530 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
531 |
lemma infsetsum_add: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
532 |
assumes "f abs_summable_on A" and "g abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
533 |
shows "infsetsum (\<lambda>x. f x + g x) A = infsetsum f A + infsetsum g A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
534 |
using assms unfolding infsetsum_def abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
535 |
by (rule Bochner_Integration.integral_add) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
536 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
537 |
lemma infsetsum_diff: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
538 |
assumes "f abs_summable_on A" and "g abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
539 |
shows "infsetsum (\<lambda>x. f x - g x) A = infsetsum f A - infsetsum g A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
540 |
using assms unfolding infsetsum_def abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
541 |
by (rule Bochner_Integration.integral_diff) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
542 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
543 |
lemma infsetsum_scaleR_left: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
544 |
assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
545 |
shows "infsetsum (\<lambda>x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
546 |
using assms unfolding infsetsum_def abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
547 |
by (rule Bochner_Integration.integral_scaleR_left) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
548 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
549 |
lemma infsetsum_scaleR_right: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
550 |
"infsetsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
551 |
unfolding infsetsum_def abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
552 |
by (subst Bochner_Integration.integral_scaleR_right) auto |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
553 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
554 |
lemma infsetsum_cmult_left: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
555 |
fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
556 |
assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
557 |
shows "infsetsum (\<lambda>x. f x * c) A = infsetsum f A * c" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
558 |
using assms unfolding infsetsum_def abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
559 |
by (rule Bochner_Integration.integral_mult_left) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
560 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
561 |
lemma infsetsum_cmult_right: |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
562 |
fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
563 |
assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
564 |
shows "infsetsum (\<lambda>x. c * f x) A = c * infsetsum f A" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
565 |
using assms unfolding infsetsum_def abs_summable_on_def |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
566 |
by (rule Bochner_Integration.integral_mult_right) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
567 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
568 |
(* TODO Generalise with bounded_linear *) |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
569 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
diff
changeset
|
570 |
end |