author | nipkow |
Fri, 05 Aug 2016 10:05:50 +0200 | |
changeset 63598 | 025d6e52d86f |
parent 63309 | a77adb28a27a |
child 63649 | e690d6f2185b |
permissions | -rw-r--r-- |
37665 | 1 |
(* Title: HOL/Library/Indicator_Function.thy |
2 |
Author: Johannes Hoelzl (TU Muenchen) |
|
3 |
*) |
|
4 |
||
60500 | 5 |
section \<open>Indicator Function\<close> |
37665 | 6 |
|
7 |
theory Indicator_Function |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
8 |
imports Complex_Main Disjoint_Sets |
37665 | 9 |
begin |
10 |
||
11 |
definition "indicator S x = (if x \<in> S then 1 else 0)" |
|
12 |
||
13 |
lemma indicator_simps[simp]: |
|
14 |
"x \<in> S \<Longrightarrow> indicator S x = 1" |
|
15 |
"x \<notin> S \<Longrightarrow> indicator S x = 0" |
|
16 |
unfolding indicator_def by auto |
|
17 |
||
45425 | 18 |
lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x" |
37665 | 19 |
and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)" |
45425 | 20 |
unfolding indicator_def by auto |
21 |
||
22 |
lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)" |
|
37665 | 23 |
unfolding indicator_def by auto |
24 |
||
63309 | 25 |
lemma indicator_eq_0_iff: "indicator A x = (0::'a::zero_neq_one) \<longleftrightarrow> x \<notin> A" |
54408 | 26 |
by (auto simp: indicator_def) |
27 |
||
63309 | 28 |
lemma indicator_eq_1_iff: "indicator A x = (1::'a::zero_neq_one) \<longleftrightarrow> x \<in> A" |
54408 | 29 |
by (auto simp: indicator_def) |
30 |
||
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
31 |
lemma indicator_leI: |
63309 | 32 |
"(x \<in> A \<Longrightarrow> y \<in> B) \<Longrightarrow> (indicator A x :: 'a::linordered_nonzero_semiring) \<le> indicator B y" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
33 |
by (auto simp: indicator_def) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
34 |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
35 |
lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
36 |
unfolding indicator_def by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
37 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
38 |
lemma split_indicator_asm: "P (indicator S x) \<longleftrightarrow> (\<not> (x \<in> S \<and> \<not> P 1 \<or> x \<notin> S \<and> \<not> P 0))" |
37665 | 39 |
unfolding indicator_def by auto |
40 |
||
45425 | 41 |
lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)" |
42 |
unfolding indicator_def by (auto simp: min_def max_def) |
|
43 |
||
63309 | 44 |
lemma indicator_union_arith: |
45 |
"indicator (A \<union> B) x = indicator A x + indicator B x - indicator A x * (indicator B x :: 'a::ring_1)" |
|
45425 | 46 |
unfolding indicator_def by (auto simp: min_def max_def) |
47 |
||
48 |
lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)" |
|
37665 | 49 |
and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)" |
45425 | 50 |
unfolding indicator_def by (auto simp: min_def max_def) |
51 |
||
63309 | 52 |
lemma indicator_disj_union: |
53 |
"A \<inter> B = {} \<Longrightarrow> indicator (A \<union> B) x = (indicator A x + indicator B x :: 'a::linordered_semidom)" |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
54 |
by (auto split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
55 |
|
63309 | 56 |
lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x :: 'a::ring_1)" |
57 |
and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x ::'a::ring_1)" |
|
37665 | 58 |
unfolding indicator_def by (auto simp: min_def max_def) |
59 |
||
63309 | 60 |
lemma indicator_times: |
61 |
"indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x) :: 'a::semiring_1)" |
|
37665 | 62 |
unfolding indicator_def by (cases x) auto |
63 |
||
63309 | 64 |
lemma indicator_sum: |
65 |
"indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)" |
|
37665 | 66 |
unfolding indicator_def by (cases x) auto |
67 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
58881
diff
changeset
|
68 |
lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)" |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
58881
diff
changeset
|
69 |
by (auto simp: indicator_def inj_on_def) |
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
58881
diff
changeset
|
70 |
|
61633 | 71 |
lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)" |
63309 | 72 |
by (auto split: split_indicator) |
61633 | 73 |
|
63309 | 74 |
lemma (* FIXME unnamed!? *) |
75 |
fixes f :: "'a \<Rightarrow> 'b::semiring_1" |
|
76 |
assumes "finite A" |
|
37665 | 77 |
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)" |
63309 | 78 |
and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)" |
37665 | 79 |
unfolding indicator_def |
62390 | 80 |
using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm) |
37665 | 81 |
|
82 |
lemma setsum_indicator_eq_card: |
|
83 |
assumes "finite A" |
|
61954 | 84 |
shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)" |
63309 | 85 |
using setsum_mult_indicator [OF assms, of "\<lambda>x. 1::nat"] |
37665 | 86 |
unfolding card_eq_setsum by simp |
87 |
||
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
54408
diff
changeset
|
88 |
lemma setsum_indicator_scaleR[simp]: |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
54408
diff
changeset
|
89 |
"finite A \<Longrightarrow> |
63309 | 90 |
(\<Sum>x \<in> A. indicator (B x) (g x) *\<^sub>R f x) = (\<Sum>x \<in> {x\<in>A. g x \<in> B x}. f x :: 'a::real_vector)" |
63092 | 91 |
by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def) |
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
54408
diff
changeset
|
92 |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
93 |
lemma LIMSEQ_indicator_incseq: |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
94 |
assumes "incseq A" |
63309 | 95 |
shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
96 |
proof (cases "\<exists>i. x \<in> A i") |
|
97 |
case True |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
98 |
then obtain i where "x \<in> A i" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
99 |
by auto |
62648 | 100 |
then have |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
101 |
"\<And>n. (indicator (A (n + i)) x :: 'a) = 1" |
60585 | 102 |
"(indicator (\<Union>i. A i) x :: 'a) = 1" |
60500 | 103 |
using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def) |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
104 |
then show ?thesis |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57447
diff
changeset
|
105 |
by (rule_tac LIMSEQ_offset[of _ i]) simp |
63309 | 106 |
next |
107 |
case False |
|
108 |
then show ?thesis by (simp add: indicator_def) |
|
109 |
qed |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
110 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
111 |
lemma LIMSEQ_indicator_UN: |
63309 | 112 |
"(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
113 |
proof - |
61969 | 114 |
have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x" |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
115 |
by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans) |
60585 | 116 |
also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)" |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
117 |
by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
118 |
finally show ?thesis . |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
119 |
qed |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
120 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
121 |
lemma LIMSEQ_indicator_decseq: |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
122 |
assumes "decseq A" |
63309 | 123 |
shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x" |
124 |
proof (cases "\<exists>i. x \<notin> A i") |
|
125 |
case True |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
126 |
then obtain i where "x \<notin> A i" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
127 |
by auto |
62648 | 128 |
then have |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
129 |
"\<And>n. (indicator (A (n + i)) x :: 'a) = 0" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
130 |
"(indicator (\<Inter>i. A i) x :: 'a) = 0" |
60500 | 131 |
using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def) |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
132 |
then show ?thesis |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57447
diff
changeset
|
133 |
by (rule_tac LIMSEQ_offset[of _ i]) simp |
63309 | 134 |
next |
135 |
case False |
|
136 |
then show ?thesis by (simp add: indicator_def) |
|
137 |
qed |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
138 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
139 |
lemma LIMSEQ_indicator_INT: |
63309 | 140 |
"(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x" |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
141 |
proof - |
61969 | 142 |
have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x" |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
143 |
by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans) |
60585 | 144 |
also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)" |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
145 |
by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
146 |
finally show ?thesis . |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
147 |
qed |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
148 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
149 |
lemma indicator_add: |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
150 |
"A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
151 |
unfolding indicator_def by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
152 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
153 |
lemma of_real_indicator: "of_real (indicator A x) = indicator A x" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
154 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
155 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
156 |
lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
157 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
158 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
159 |
lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
160 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
161 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
162 |
lemma mult_indicator_subset: |
63309 | 163 |
"A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::comm_semiring_1)" |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
164 |
by (auto split: split_indicator simp: fun_eq_iff) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
165 |
|
62648 | 166 |
lemma indicator_sums: |
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
167 |
assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
168 |
shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x" |
63309 | 169 |
proof (cases "\<exists>i. x \<in> A i") |
170 |
case True |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
171 |
then obtain i where i: "x \<in> A i" .. |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
172 |
with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
173 |
by (intro sums_finite) (auto split: split_indicator) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
174 |
also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
175 |
using i by (auto split: split_indicator) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
176 |
finally show ?thesis . |
63309 | 177 |
next |
178 |
case False |
|
179 |
then show ?thesis by simp |
|
180 |
qed |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
181 |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
182 |
text \<open> |
63309 | 183 |
The indicator function of the union of a disjoint family of sets is the |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
184 |
sum over all the individual indicators. |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
185 |
\<close> |
63309 | 186 |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
187 |
lemma indicator_UN_disjoint: |
63309 | 188 |
"finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)" |
189 |
by (induct A rule: finite_induct) |
|
190 |
(auto simp: disjoint_family_on_def indicator_def split: if_splits) |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
191 |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
192 |
end |