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