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