author | eberlm |
Tue, 17 May 2016 17:05:35 +0200 | |
changeset 63099 | af0e964aad7b |
parent 63092 | a949b2a5f51d |
child 63309 | a77adb28a27a |
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 |
||
54408 | 25 |
lemma indicator_eq_0_iff: "indicator A x = (0::_::zero_neq_one) \<longleftrightarrow> x \<notin> A" |
26 |
by (auto simp: indicator_def) |
|
27 |
||
28 |
lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A" |
|
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: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
32 |
"(x \<in> A \<Longrightarrow> y \<in> B) \<Longrightarrow> (indicator A x :: 'a :: linordered_nonzero_semiring) \<le> indicator B y" |
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 |
||
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
44 |
lemma indicator_union_arith: "indicator (A \<union> B) x = indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)" |
45425 | 45 |
unfolding indicator_def by (auto simp: min_def max_def) |
46 |
||
47 |
lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)" |
|
37665 | 48 |
and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)" |
45425 | 49 |
unfolding indicator_def by (auto simp: min_def max_def) |
50 |
||
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
51 |
lemma indicator_disj_union: "A \<inter> B = {} \<Longrightarrow> indicator (A \<union> B) x = (indicator A x + indicator B x::'a::linordered_semidom)" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
52 |
by (auto split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
53 |
|
45425 | 54 |
lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)" |
37665 | 55 |
and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)" |
56 |
unfolding indicator_def by (auto simp: min_def max_def) |
|
57 |
||
45425 | 58 |
lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)" |
37665 | 59 |
unfolding indicator_def by (cases x) auto |
60 |
||
45425 | 61 |
lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)" |
37665 | 62 |
unfolding indicator_def by (cases x) auto |
63 |
||
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
58881
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
|
61633 | 67 |
lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)" |
68 |
by(auto split: split_indicator) |
|
69 |
||
37665 | 70 |
lemma |
71 |
fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A" |
|
72 |
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)" |
|
73 |
and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)" |
|
74 |
unfolding indicator_def |
|
62390 | 75 |
using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm) |
37665 | 76 |
|
77 |
lemma setsum_indicator_eq_card: |
|
78 |
assumes "finite A" |
|
61954 | 79 |
shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)" |
37665 | 80 |
using setsum_mult_indicator[OF assms, of "%x. 1::nat"] |
81 |
unfolding card_eq_setsum by simp |
|
82 |
||
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
54408
diff
changeset
|
83 |
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
|
84 |
"finite A \<Longrightarrow> |
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents:
54408
diff
changeset
|
85 |
(\<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 | 86 |
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
|
87 |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
88 |
lemma LIMSEQ_indicator_incseq: |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
89 |
assumes "incseq A" |
61969 | 90 |
shows "(\<lambda>i. indicator (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
|
91 |
proof cases |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
92 |
assume "\<exists>i. x \<in> A i" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
93 |
then obtain i where "x \<in> A i" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
94 |
by auto |
62648 | 95 |
then have |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
96 |
"\<And>n. (indicator (A (n + i)) x :: 'a) = 1" |
60585 | 97 |
"(indicator (\<Union>i. A i) x :: 'a) = 1" |
60500 | 98 |
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
|
99 |
then show ?thesis |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57447
diff
changeset
|
100 |
by (rule_tac LIMSEQ_offset[of _ i]) simp |
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57447
diff
changeset
|
101 |
qed (auto simp: indicator_def) |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
102 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
103 |
lemma LIMSEQ_indicator_UN: |
61969 | 104 |
"(\<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
|
105 |
proof - |
61969 | 106 |
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
|
107 |
by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans) |
60585 | 108 |
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
|
109 |
by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
110 |
finally show ?thesis . |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
111 |
qed |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
112 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
113 |
lemma LIMSEQ_indicator_decseq: |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
114 |
assumes "decseq A" |
61969 | 115 |
shows "(\<lambda>i. indicator (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
|
116 |
proof cases |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
117 |
assume "\<exists>i. x \<notin> A i" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
118 |
then obtain i where "x \<notin> A i" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
119 |
by auto |
62648 | 120 |
then have |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
121 |
"\<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
|
122 |
"(indicator (\<Inter>i. A i) x :: 'a) = 0" |
60500 | 123 |
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
|
124 |
then show ?thesis |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57447
diff
changeset
|
125 |
by (rule_tac LIMSEQ_offset[of _ i]) simp |
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57447
diff
changeset
|
126 |
qed (auto simp: indicator_def) |
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
127 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
128 |
lemma LIMSEQ_indicator_INT: |
61969 | 129 |
"(\<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
|
130 |
proof - |
61969 | 131 |
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
|
132 |
by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans) |
60585 | 133 |
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
|
134 |
by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
135 |
finally show ?thesis . |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
136 |
qed |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
137 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
138 |
lemma indicator_add: |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
139 |
"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
|
140 |
unfolding indicator_def by auto |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
141 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
142 |
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
|
143 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
144 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
145 |
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
|
146 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
147 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
148 |
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
|
149 |
by (simp split: split_indicator) |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
150 |
|
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
151 |
lemma mult_indicator_subset: |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
152 |
"A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::{comm_semiring_1})" |
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
153 |
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
|
154 |
|
62648 | 155 |
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
|
156 |
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
|
157 |
shows "(\<lambda>i. indicator (A i) x::real) sums 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
|
158 |
proof cases |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
159 |
assume "\<exists>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
|
160 |
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
|
161 |
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
|
162 |
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
|
163 |
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
|
164 |
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
|
165 |
finally show ?thesis . |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
166 |
qed simp |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57446
diff
changeset
|
167 |
|
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
168 |
text \<open> |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
169 |
The indicator function of the union of a disjoint family of sets is the |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
170 |
sum over all the individual indicators. |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
171 |
\<close> |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
172 |
lemma indicator_UN_disjoint: |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
173 |
assumes "finite A" "disjoint_family_on f A" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
174 |
shows "indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)" |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
175 |
using assms by (induction A rule: finite_induct) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
176 |
(auto simp: disjoint_family_on_def indicator_def split: if_splits) |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset
|
177 |
|
57446
06e195515deb
some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents:
57418
diff
changeset
|
178 |
end |