src/HOL/Library/Indicator_Function.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 67683 817944aeac3f
child 69313 b021008c5397
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/Indicator_Function.thy
     2     Author:     Johannes Hoelzl (TU Muenchen)
     3 *)
     4 
     5 section \<open>Indicator Function\<close>
     6 
     7 theory Indicator_Function
     8 imports Complex_Main Disjoint_Sets
     9 begin
    10 
    11 definition "indicator S x = (if x \<in> S then 1 else 0)"
    12 
    13 text\<open>Type constrained version\<close>
    14 abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
    15 
    16 lemma 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 
    21 lemma 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 
    25 lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
    26   unfolding indicator_def by auto
    27 
    28 lemma indicator_eq_0_iff: "indicator A x = (0::'a::zero_neq_one) \<longleftrightarrow> x \<notin> A"
    29   by (auto simp: indicator_def)
    30 
    31 lemma indicator_eq_1_iff: "indicator A x = (1::'a::zero_neq_one) \<longleftrightarrow> x \<in> A"
    32   by (auto simp: indicator_def)
    33 
    34 lemma indicator_UNIV [simp]: "indicator UNIV = (\<lambda>x. 1)"
    35   by auto
    36 
    37 lemma 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 
    41 lemma 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 
    44 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))"
    45   unfolding indicator_def by auto
    46 
    47 lemma 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 
    50 lemma 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 
    54 lemma 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 
    58 lemma 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 
    62 lemma 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 
    66 lemma 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 
    70 lemma 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 
    74 lemma 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 
    77 lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
    78   by (auto split: split_indicator)
    79 
    80 lemma  (* 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 
    88 lemma 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 
    94 lemma 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 
    99 lemma 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"
   102 proof (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)
   112 next
   113   case False
   114   then show ?thesis by (simp add: indicator_def)
   115 qed
   116 
   117 lemma 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"
   119 proof -
   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 .
   125 qed
   126 
   127 lemma 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"
   130 proof (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)
   140 next
   141   case False
   142   then show ?thesis by (simp add: indicator_def)
   143 qed
   144 
   145 lemma 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"
   147 proof -
   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 .
   153 qed
   154 
   155 lemma 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 
   159 lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
   160   by (simp split: split_indicator)
   161 
   162 lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
   163   by (simp split: split_indicator)
   164 
   165 lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x"
   166   by (simp split: split_indicator)
   167 
   168 lemma 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 
   172 lemma 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"
   175 proof (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 .
   183 next
   184   case False
   185   then show ?thesis by simp
   186 qed
   187 
   188 text \<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 
   193 lemma 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 
   198 end