(* Title: HOL/Library/Indicator_Function.thy
Author: Johannes Hoelzl (TU Muenchen)
*)
section \<open>Indicator Function\<close>
theory Indicator_Function
imports Complex_Main Disjoint_Sets
begin
definition "indicator S x = (if x \ S then 1 else 0)"
text\<open>Type constrained version\<close>
abbreviation indicat_real :: "'a set \ 'a \ real" where "indicat_real S \ indicator S"
lemma indicator_simps[simp]:
"x \ S \ indicator S x = 1"
"x \ S \ indicator S x = 0"
unfolding indicator_def by auto
lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \ indicator S x"
and indicator_le_1[intro, simp]: "indicator S x \ (1::'a::linordered_semidom)"
unfolding indicator_def by auto
lemma indicator_abs_le_1: "\indicator S x\ \ (1::'a::linordered_idom)"
unfolding indicator_def by auto
lemma indicator_eq_0_iff: "indicator A x = (0::'a::zero_neq_one) \ x \ A"
by (auto simp: indicator_def)
lemma indicator_eq_1_iff: "indicator A x = (1::'a::zero_neq_one) \ x \ A"
by (auto simp: indicator_def)
lemma indicator_UNIV [simp]: "indicator UNIV = (\x. 1)"
by auto
lemma indicator_leI:
"(x \ A \ y \ B) \ (indicator A x :: 'a::linordered_nonzero_semiring) \ indicator B y"
by (auto simp: indicator_def)
lemma split_indicator: "P (indicator S x) \ ((x \ S \ P 1) \ (x \ S \ P 0))"
unfolding indicator_def by auto
lemma split_indicator_asm: "P (indicator S x) \ (\ (x \ S \ \ P 1 \ x \ S \ \ P 0))"
unfolding indicator_def by auto
lemma indicator_inter_arith: "indicator (A \ B) x = indicator A x * (indicator B x::'a::semiring_1)"
unfolding indicator_def by (auto simp: min_def max_def)
lemma indicator_union_arith:
"indicator (A \ B) x = indicator A x + indicator B x - indicator A x * (indicator B x :: 'a::ring_1)"
unfolding indicator_def by (auto simp: min_def max_def)
lemma indicator_inter_min: "indicator (A \ B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
and indicator_union_max: "indicator (A \ B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
unfolding indicator_def by (auto simp: min_def max_def)
lemma indicator_disj_union:
"A \ B = {} \ indicator (A \ B) x = (indicator A x + indicator B x :: 'a::linordered_semidom)"
by (auto split: split_indicator)
lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x :: 'a::ring_1)"
and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x ::'a::ring_1)"
unfolding indicator_def by (auto simp: min_def max_def)
lemma indicator_times:
"indicator (A \ B) x = indicator A (fst x) * (indicator B (snd x) :: 'a::semiring_1)"
unfolding indicator_def by (cases x) auto
lemma indicator_sum:
"indicator (A <+> B) x = (case x of Inl x \ indicator A x | Inr x \ indicator B x)"
unfolding indicator_def by (cases x) auto
lemma indicator_image: "inj f \ indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
by (auto simp: indicator_def inj_def)
lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
by (auto split: split_indicator)
lemma (* FIXME unnamed!? *)
fixes f :: "'a \ 'b::semiring_1"
assumes "finite A"
shows sum_mult_indicator[simp]: "(\x \ A. f x * indicator B x) = (\x \ A \ B. f x)"
and sum_indicator_mult[simp]: "(\x \ A. indicator B x * f x) = (\x \ A \ B. f x)"
unfolding indicator_def
using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm)
lemma sum_indicator_eq_card:
assumes "finite A"
shows "(\x \ A. indicator B x) = card (A Int B)"
using sum_mult_indicator [OF assms, of "\x. 1::nat"]
unfolding card_eq_sum by simp
lemma sum_indicator_scaleR[simp]:
"finite A \
(\<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)"
by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
lemma LIMSEQ_indicator_incseq:
assumes "incseq A"
shows "(\i. indicator (A i) x :: 'a::{topological_space,one,zero}) \ indicator (\i. A i) x"
proof (cases "\i. x \ A i")
case True
then obtain i where "x \ A i"
by auto
then have *:
"\n. (indicator (A (n + i)) x :: 'a) = 1"
"(indicator (\i. A i) x :: 'a) = 1"
using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
show ?thesis
by (rule LIMSEQ_offset[of _ i]) (use * in simp)
next
case False
then show ?thesis by (simp add: indicator_def)
qed
lemma LIMSEQ_indicator_UN:
"(\k. indicator (\i indicator (\i. A i) x"
proof -
have "(\k. indicator (\i indicator (\k. \i
by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
also have "(\k. \ii. A i)"
by auto
finally show ?thesis .
qed
lemma LIMSEQ_indicator_decseq:
assumes "decseq A"
shows "(\i. indicator (A i) x :: 'a::{topological_space,one,zero}) \ indicator (\i. A i) x"
proof (cases "\i. x \ A i")
case True
then obtain i where "x \ A i"
by auto
then have *:
"\n. (indicator (A (n + i)) x :: 'a) = 0"
"(indicator (\i. A i) x :: 'a) = 0"
using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
show ?thesis
by (rule LIMSEQ_offset[of _ i]) (use * in simp)
next
case False
then show ?thesis by (simp add: indicator_def)
qed
lemma LIMSEQ_indicator_INT:
"(\k. indicator (\i indicator (\i. A i) x"
proof -
have "(\k. indicator (\i indicator (\k. \i
by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
also have "(\k. \ii. A i)"
by auto
finally show ?thesis .
qed
lemma indicator_add:
"A \ B = {} \ (indicator A x::_::monoid_add) + indicator B x = indicator (A \ B) x"
unfolding indicator_def by auto
lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
by (simp split: split_indicator)
lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
by (simp split: split_indicator)
lemma abs_indicator: "\indicator A x :: 'a::linordered_idom\ = indicator A x"
by (simp split: split_indicator)
lemma mult_indicator_subset:
"A \ B \ indicator A x * indicator B x = (indicator A x :: 'a::comm_semiring_1)"
by (auto split: split_indicator simp: fun_eq_iff)
lemma indicator_times_eq_if:
fixes f :: "'a \ 'b::comm_ring_1"
shows "indicator S x * f x = (if x \ S then f x else 0)" "f x * indicator S x = (if x \ S then f x else 0)"
by auto
lemma indicator_scaleR_eq_if:
fixes f :: "'a \ 'b::real_vector"
shows "indicator S x *\<^sub>R f x = (if x \ S then f x else 0)"
by simp
lemma indicator_sums:
assumes "\i j. i \ j \ A i \ A j = {}"
shows "(\i. indicator (A i) x::real) sums indicator (\i. A i) x"
proof (cases "\i. x \ A i")
case True
then obtain i where i: "x \ A i" ..
with assms have "(\i. indicator (A i) x::real) sums (\i\{i}. indicator (A i) x)"
by (intro sums_finite) (auto split: split_indicator)
also have "(\i\{i}. indicator (A i) x) = indicator (\i. A i) x"
using i by (auto split: split_indicator)
finally show ?thesis .
next
case False
then show ?thesis by simp
qed
text \<open>
The indicator function of the union of a disjoint family of sets is the
sum over all the individual indicators.
\<close>
lemma indicator_UN_disjoint:
"finite A \ disjoint_family_on f A \ indicator (\(f ` A)) x = (\y\A. indicator (f y) x)"
by (induct A rule: finite_induct)
(auto simp: disjoint_family_on_def indicator_def split: if_splits)
end
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
