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