src/HOL/Library/Indicator_Function.thy
 author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 61633 64e6d712af16 child 61954 1d43f86f48be permissions -rw-r--r--
more symbols;
```     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
```
```     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
```
```    18 lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
```
```    19   and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
```
```    20   unfolding indicator_def by auto
```
```    21
```
```    22 lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
```
```    23   unfolding indicator_def by auto
```
```    24
```
```    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
```
```    31 lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
```
```    32   unfolding indicator_def by auto
```
```    33
```
```    34 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))"
```
```    35   unfolding indicator_def by auto
```
```    36
```
```    37 lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
```
```    38   unfolding indicator_def by (auto simp: min_def max_def)
```
```    39
```
```    40 lemma indicator_union_arith: "indicator (A \<union> B) x = indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
```
```    41   unfolding indicator_def by (auto simp: min_def max_def)
```
```    42
```
```    43 lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
```
```    44   and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
```
```    45   unfolding indicator_def by (auto simp: min_def max_def)
```
```    46
```
```    47 lemma indicator_disj_union: "A \<inter> B = {} \<Longrightarrow>  indicator (A \<union> B) x = (indicator A x + indicator B x::'a::linordered_semidom)"
```
```    48   by (auto split: split_indicator)
```
```    49
```
```    50 lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
```
```    51   and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
```
```    52   unfolding indicator_def by (auto simp: min_def max_def)
```
```    53
```
```    54 lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
```
```    55   unfolding indicator_def by (cases x) auto
```
```    56
```
```    57 lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
```
```    58   unfolding indicator_def by (cases x) auto
```
```    59
```
```    60 lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
```
```    61   by (auto simp: indicator_def inj_on_def)
```
```    62
```
```    63 lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
```
```    64 by(auto split: split_indicator)
```
```    65
```
```    66 lemma
```
```    67   fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
```
```    68   shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
```
```    69   and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
```
```    70   unfolding indicator_def
```
```    71   using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm)
```
```    72
```
```    73 lemma setsum_indicator_eq_card:
```
```    74   assumes "finite A"
```
```    75   shows "(SUM x : A. indicator B x) = card (A Int B)"
```
```    76   using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
```
```    77   unfolding card_eq_setsum by simp
```
```    78
```
```    79 lemma setsum_indicator_scaleR[simp]:
```
```    80   "finite A \<Longrightarrow>
```
```    81     (\<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)"
```
```    82   using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm simp: indicator_def)
```
```    83
```
```    84 lemma LIMSEQ_indicator_incseq:
```
```    85   assumes "incseq A"
```
```    86   shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
```
```    87 proof cases
```
```    88   assume "\<exists>i. x \<in> A i"
```
```    89   then obtain i where "x \<in> A i"
```
```    90     by auto
```
```    91   then have
```
```    92     "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
```
```    93     "(indicator (\<Union>i. A i) x :: 'a) = 1"
```
```    94     using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
```
```    95   then show ?thesis
```
```    96     by (rule_tac LIMSEQ_offset[of _ i]) simp
```
```    97 qed (auto simp: indicator_def)
```
```    98
```
```    99 lemma LIMSEQ_indicator_UN:
```
```   100   "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
```
```   101 proof -
```
```   102   have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union>i<k. A i) x"
```
```   103     by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
```
```   104   also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
```
```   105     by auto
```
```   106   finally show ?thesis .
```
```   107 qed
```
```   108
```
```   109 lemma LIMSEQ_indicator_decseq:
```
```   110   assumes "decseq A"
```
```   111   shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
```
```   112 proof cases
```
```   113   assume "\<exists>i. x \<notin> A i"
```
```   114   then obtain i where "x \<notin> A i"
```
```   115     by auto
```
```   116   then have
```
```   117     "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
```
```   118     "(indicator (\<Inter>i. A i) x :: 'a) = 0"
```
```   119     using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
```
```   120   then show ?thesis
```
```   121     by (rule_tac LIMSEQ_offset[of _ i]) simp
```
```   122 qed (auto simp: indicator_def)
```
```   123
```
```   124 lemma LIMSEQ_indicator_INT:
```
```   125   "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
```
```   126 proof -
```
```   127   have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
```
```   128     by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
```
```   129   also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
```
```   130     by auto
```
```   131   finally show ?thesis .
```
```   132 qed
```
```   133
```
```   134 lemma indicator_add:
```
```   135   "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
```
```   136   unfolding indicator_def by auto
```
```   137
```
```   138 lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
```
```   139   by (simp split: split_indicator)
```
```   140
```
```   141 lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
```
```   142   by (simp split: split_indicator)
```
```   143
```
```   144 lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x"
```
```   145   by (simp split: split_indicator)
```
```   146
```
```   147 lemma mult_indicator_subset:
```
```   148   "A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::{comm_semiring_1})"
```
```   149   by (auto split: split_indicator simp: fun_eq_iff)
```
```   150
```
```   151 lemma indicator_sums:
```
```   152   assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
```
```   153   shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
```
```   154 proof cases
```
```   155   assume "\<exists>i. x \<in> A i"
```
```   156   then obtain i where i: "x \<in> A i" ..
```
```   157   with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)"
```
```   158     by (intro sums_finite) (auto split: split_indicator)
```
```   159   also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x"
```
```   160     using i by (auto split: split_indicator)
```
```   161   finally show ?thesis .
```
```   162 qed simp
```
```   163
```
```   164 end
```