1(*  Title:      HOL/Library/Indicator_Function.thy
2    Author:     Johannes Hoelzl (TU Muenchen)
3*)
4
5section \<open>Indicator Function\<close>
6
7theory Indicator_Function
8imports Complex_Main Disjoint_Sets
9begin
10
11definition "indicator S x = (if x \<in> S then 1 else 0)"
12
13text\<open>Type constrained version\<close>
14abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
15
16lemma indicator_simps[simp]:
17  "x \<in> S \<Longrightarrow> indicator S x = 1"
18  "x \<notin> S \<Longrightarrow> indicator S x = 0"
19  unfolding indicator_def by auto
20
21lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
22  and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
23  unfolding indicator_def by auto
24
25lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
26  unfolding indicator_def by auto
27
28lemma indicator_eq_0_iff: "indicator A x = (0::'a::zero_neq_one) \<longleftrightarrow> x \<notin> A"
29  by (auto simp: indicator_def)
30
31lemma indicator_eq_1_iff: "indicator A x = (1::'a::zero_neq_one) \<longleftrightarrow> x \<in> A"
32  by (auto simp: indicator_def)
33
34lemma indicator_UNIV [simp]: "indicator UNIV = (\<lambda>x. 1)"
35  by auto
36
37lemma indicator_leI:
38  "(x \<in> A \<Longrightarrow> y \<in> B) \<Longrightarrow> (indicator A x :: 'a::linordered_nonzero_semiring) \<le> indicator B y"
39  by (auto simp: indicator_def)
40
41lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
42  unfolding indicator_def by auto
43
44lemma split_indicator_asm: "P (indicator S x) \<longleftrightarrow> (\<not> (x \<in> S \<and> \<not> P 1 \<or> x \<notin> S \<and> \<not> P 0))"
45  unfolding indicator_def by auto
46
47lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
48  unfolding indicator_def by (auto simp: min_def max_def)
49
50lemma indicator_union_arith:
51  "indicator (A \<union> B) x = indicator A x + indicator B x - indicator A x * (indicator B x :: 'a::ring_1)"
52  unfolding indicator_def by (auto simp: min_def max_def)
53
54lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
55  and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
56  unfolding indicator_def by (auto simp: min_def max_def)
57
58lemma indicator_disj_union:
59  "A \<inter> B = {} \<Longrightarrow> indicator (A \<union> B) x = (indicator A x + indicator B x :: 'a::linordered_semidom)"
60  by (auto split: split_indicator)
61
62lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x :: 'a::ring_1)"
63  and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x ::'a::ring_1)"
64  unfolding indicator_def by (auto simp: min_def max_def)
65
66lemma indicator_times:
67  "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x) :: 'a::semiring_1)"
68  unfolding indicator_def by (cases x) auto
69
70lemma indicator_sum:
71  "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
72  unfolding indicator_def by (cases x) auto
73
74lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
75  by (auto simp: indicator_def inj_def)
76
77lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
78  by (auto split: split_indicator)
79
80lemma  (* FIXME unnamed!? *)
81  fixes f :: "'a \<Rightarrow> 'b::semiring_1"
82  assumes "finite A"
83  shows sum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
84    and sum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
85  unfolding indicator_def
86  using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm)
87
88lemma sum_indicator_eq_card:
89  assumes "finite A"
90  shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)"
91  using sum_mult_indicator [OF assms, of "\<lambda>x. 1::nat"]
92  unfolding card_eq_sum by simp
93
94lemma sum_indicator_scaleR[simp]:
95  "finite A \<Longrightarrow>
96    (\<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)"
97  by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
98
99lemma LIMSEQ_indicator_incseq:
100  assumes "incseq A"
101  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
102proof (cases "\<exists>i. x \<in> A i")
103  case True
104  then obtain i where "x \<in> A i"
105    by auto
106  then have *:
107    "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
108    "(indicator (\<Union>i. A i) x :: 'a) = 1"
109    using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
110  show ?thesis
111    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
112next
113  case False
114  then show ?thesis by (simp add: indicator_def)
115qed
116
117lemma LIMSEQ_indicator_UN:
118  "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
119proof -
120  have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x"
121    by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
122  also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
123    by auto
124  finally show ?thesis .
125qed
126
127lemma LIMSEQ_indicator_decseq:
128  assumes "decseq A"
129  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
130proof (cases "\<exists>i. x \<notin> A i")
131  case True
132  then obtain i where "x \<notin> A i"
133    by auto
134  then have *:
135    "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
136    "(indicator (\<Inter>i. A i) x :: 'a) = 0"
137    using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
138  show ?thesis
139    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
140next
141  case False
142  then show ?thesis by (simp add: indicator_def)
143qed
144
145lemma LIMSEQ_indicator_INT:
146  "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
147proof -
148  have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x"
149    by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
150  also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
151    by auto
152  finally show ?thesis .
153qed
154
155lemma indicator_add:
156  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
157  unfolding indicator_def by auto
158
159lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
160  by (simp split: split_indicator)
161
162lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
163  by (simp split: split_indicator)
164
165lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x"
166  by (simp split: split_indicator)
167
168lemma mult_indicator_subset:
169  "A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::comm_semiring_1)"
170  by (auto split: split_indicator simp: fun_eq_iff)
171
172lemma indicator_sums:
173  assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
174  shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
175proof (cases "\<exists>i. x \<in> A i")
176  case True
177  then obtain i where i: "x \<in> A i" ..
178  with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)"
179    by (intro sums_finite) (auto split: split_indicator)
180  also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x"
181    using i by (auto split: split_indicator)
182  finally show ?thesis .
183next
184  case False
185  then show ?thesis by simp
186qed
187
188text \<open>
189  The indicator function of the union of a disjoint family of sets is the
190  sum over all the individual indicators.
191\<close>
192
193lemma indicator_UN_disjoint:
194  "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)"
195  by (induct A rule: finite_induct)
196    (auto simp: disjoint_family_on_def indicator_def split: if_splits)
197
198end
199