src/HOL/Library/Indicator_Function.thy
author blanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425 246985c6b20b
parent 57447 87429bdecad5
child 58729 e8ecc79aee43
permissions -rw-r--r--
simpler proof
     1 (*  Title:      HOL/Library/Indicator_Function.thy
     2     Author:     Johannes Hoelzl (TU Muenchen)
     3 *)
     4 
     5 header {* Indicator Function *}
     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
    61   fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
    62   shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
    63   and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
    64   unfolding indicator_def
    65   using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm)
    66 
    67 lemma setsum_indicator_eq_card:
    68   assumes "finite A"
    69   shows "(SUM x : A. indicator B x) = card (A Int B)"
    70   using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
    71   unfolding card_eq_setsum by simp
    72 
    73 lemma setsum_indicator_scaleR[simp]:
    74   "finite A \<Longrightarrow>
    75     (\<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)"
    76   using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm simp: indicator_def)
    77 
    78 lemma LIMSEQ_indicator_incseq:
    79   assumes "incseq A"
    80   shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
    81 proof cases
    82   assume "\<exists>i. x \<in> A i"
    83   then obtain i where "x \<in> A i"
    84     by auto
    85   then have 
    86     "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
    87     "(indicator (\<Union> i. A i) x :: 'a) = 1"
    88     using incseqD[OF `incseq A`, of i "n + i" for n] `x \<in> A i` by (auto simp: indicator_def)
    89   then show ?thesis
    90     by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
    91 qed (auto simp: indicator_def tendsto_const)
    92 
    93 lemma LIMSEQ_indicator_UN:
    94   "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
    95 proof -
    96   have "(\<lambda>k. indicator (\<Union> i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union> i<k. A i) x"
    97     by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
    98   also have "(\<Union>k. \<Union> i<k. A i) = (\<Union>i. A i)"
    99     by auto
   100   finally show ?thesis .
   101 qed
   102 
   103 lemma LIMSEQ_indicator_decseq:
   104   assumes "decseq A"
   105   shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
   106 proof cases
   107   assume "\<exists>i. x \<notin> A i"
   108   then obtain i where "x \<notin> A i"
   109     by auto
   110   then have 
   111     "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
   112     "(indicator (\<Inter>i. A i) x :: 'a) = 0"
   113     using decseqD[OF `decseq A`, of i "n + i" for n] `x \<notin> A i` by (auto simp: indicator_def)
   114   then show ?thesis
   115     by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
   116 qed (auto simp: indicator_def tendsto_const)
   117 
   118 lemma LIMSEQ_indicator_INT:
   119   "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
   120 proof -
   121   have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
   122     by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
   123   also have "(\<Inter>k. \<Inter> i<k. A i) = (\<Inter>i. A i)"
   124     by auto
   125   finally show ?thesis .
   126 qed
   127 
   128 lemma indicator_add:
   129   "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
   130   unfolding indicator_def by auto
   131 
   132 lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
   133   by (simp split: split_indicator)
   134 
   135 lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
   136   by (simp split: split_indicator)
   137 
   138 lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x"
   139   by (simp split: split_indicator)
   140 
   141 lemma mult_indicator_subset:
   142   "A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::{comm_semiring_1})"
   143   by (auto split: split_indicator simp: fun_eq_iff)
   144 
   145 lemma indicator_sums: 
   146   assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
   147   shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
   148 proof cases
   149   assume "\<exists>i. x \<in> A i"
   150   then obtain i where i: "x \<in> A i" ..
   151   with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)"
   152     by (intro sums_finite) (auto split: split_indicator)
   153   also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x"
   154     using i by (auto split: split_indicator)
   155   finally show ?thesis .
   156 qed simp
   157 
   158 end