src/HOL/Library/Indicator_Function.thy
author wenzelm
Fri, 13 May 2016 20:24:10 +0200
changeset 63092 a949b2a5f51d
parent 62648 ee48e0b4f669
child 63099 af0e964aad7b
permissions -rw-r--r--
eliminated use of empty "assms";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     1
(*  Title:      HOL/Library/Indicator_Function.thy
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     2
    Author:     Johannes Hoelzl (TU Muenchen)
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     3
*)
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59002
diff changeset
     5
section \<open>Indicator Function\<close>
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     6
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     7
theory Indicator_Function
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 54408
diff changeset
     8
imports Complex_Main
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     9
begin
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    10
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    11
definition "indicator S x = (if x \<in> S then 1 else 0)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    12
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    13
lemma indicator_simps[simp]:
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    14
  "x \<in> S \<Longrightarrow> indicator S x = 1"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    15
  "x \<notin> S \<Longrightarrow> indicator S x = 0"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    16
  unfolding indicator_def by auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    17
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    18
lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    19
  and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    20
  unfolding indicator_def by auto
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    21
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    22
lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    23
  unfolding indicator_def by auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    24
54408
67dec4ccaabd equation when indicator function equals 0 or 1
hoelzl
parents: 45425
diff changeset
    25
lemma indicator_eq_0_iff: "indicator A x = (0::_::zero_neq_one) \<longleftrightarrow> x \<notin> A"
67dec4ccaabd equation when indicator function equals 0 or 1
hoelzl
parents: 45425
diff changeset
    26
  by (auto simp: indicator_def)
67dec4ccaabd equation when indicator function equals 0 or 1
hoelzl
parents: 45425
diff changeset
    27
67dec4ccaabd equation when indicator function equals 0 or 1
hoelzl
parents: 45425
diff changeset
    28
lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A"
67dec4ccaabd equation when indicator function equals 0 or 1
hoelzl
parents: 45425
diff changeset
    29
  by (auto simp: indicator_def)
67dec4ccaabd equation when indicator function equals 0 or 1
hoelzl
parents: 45425
diff changeset
    30
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    31
lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    32
  unfolding indicator_def by auto
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    33
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    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))"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    35
  unfolding indicator_def by auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    36
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    37
lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    38
  unfolding indicator_def by (auto simp: min_def max_def)
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    39
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    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)"
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    41
  unfolding indicator_def by (auto simp: min_def max_def)
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    42
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    43
lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    44
  and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    45
  unfolding indicator_def by (auto simp: min_def max_def)
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    46
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    47
lemma indicator_disj_union: "A \<inter> B = {} \<Longrightarrow>  indicator (A \<union> B) x = (indicator A x + indicator B x::'a::linordered_semidom)"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    48
  by (auto split: split_indicator)
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    49
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    50
lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    51
  and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    52
  unfolding indicator_def by (auto simp: min_def max_def)
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    53
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    54
lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    55
  unfolding indicator_def by (cases x) auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    56
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    57
lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    58
  unfolding indicator_def by (cases x) auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    59
59002
2c8b2fb54b88 cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents: 58881
diff changeset
    60
lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
2c8b2fb54b88 cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents: 58881
diff changeset
    61
  by (auto simp: indicator_def inj_on_def)
2c8b2fb54b88 cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents: 58881
diff changeset
    62
61633
64e6d712af16 add lemmas
Andreas Lochbihler
parents: 60585
diff changeset
    63
lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
64e6d712af16 add lemmas
Andreas Lochbihler
parents: 60585
diff changeset
    64
by(auto split: split_indicator)
64e6d712af16 add lemmas
Andreas Lochbihler
parents: 60585
diff changeset
    65
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    66
lemma
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    67
  fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    68
  shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    69
  and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    70
  unfolding indicator_def
62390
842917225d56 more canonical names
nipkow
parents: 61969
diff changeset
    71
  using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm)
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    72
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    73
lemma setsum_indicator_eq_card:
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    74
  assumes "finite A"
61954
1d43f86f48be more symbols;
wenzelm
parents: 61633
diff changeset
    75
  shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    76
  using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    77
  unfolding card_eq_setsum by simp
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    78
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 54408
diff changeset
    79
lemma setsum_indicator_scaleR[simp]:
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 54408
diff changeset
    80
  "finite A \<Longrightarrow>
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 54408
diff changeset
    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)"
63092
a949b2a5f51d eliminated use of empty "assms";
wenzelm
parents: 62648
diff changeset
    82
  by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
56993
e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
hoelzl
parents: 54408
diff changeset
    83
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    84
lemma LIMSEQ_indicator_incseq:
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    85
  assumes "incseq A"
61969
e01015e49041 more symbols;
wenzelm
parents: 61954
diff changeset
    86
  shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    87
proof cases
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    88
  assume "\<exists>i. x \<in> A i"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    89
  then obtain i where "x \<in> A i"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    90
    by auto
62648
ee48e0b4f669 more stuff for extended nonnegative real numbers
hoelzl
parents: 62390
diff changeset
    91
  then have
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    92
    "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60500
diff changeset
    93
    "(indicator (\<Union>i. A i) x :: 'a) = 1"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59002
diff changeset
    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)
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    95
  then show ?thesis
58729
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57447
diff changeset
    96
    by (rule_tac LIMSEQ_offset[of _ i]) simp
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57447
diff changeset
    97
qed (auto simp: indicator_def)
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    98
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
    99
lemma LIMSEQ_indicator_UN:
61969
e01015e49041 more symbols;
wenzelm
parents: 61954
diff changeset
   100
  "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   101
proof -
61969
e01015e49041 more symbols;
wenzelm
parents: 61954
diff changeset
   102
  have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   103
    by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60500
diff changeset
   104
  also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   105
    by auto
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   106
  finally show ?thesis .
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   107
qed
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   108
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   109
lemma LIMSEQ_indicator_decseq:
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   110
  assumes "decseq A"
61969
e01015e49041 more symbols;
wenzelm
parents: 61954
diff changeset
   111
  shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   112
proof cases
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   113
  assume "\<exists>i. x \<notin> A i"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   114
  then obtain i where "x \<notin> A i"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   115
    by auto
62648
ee48e0b4f669 more stuff for extended nonnegative real numbers
hoelzl
parents: 62390
diff changeset
   116
  then have
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   117
    "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   118
    "(indicator (\<Inter>i. A i) x :: 'a) = 0"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59002
diff changeset
   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)
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   120
  then show ?thesis
58729
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57447
diff changeset
   121
    by (rule_tac LIMSEQ_offset[of _ i]) simp
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57447
diff changeset
   122
qed (auto simp: indicator_def)
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   123
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   124
lemma LIMSEQ_indicator_INT:
61969
e01015e49041 more symbols;
wenzelm
parents: 61954
diff changeset
   125
  "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   126
proof -
61969
e01015e49041 more symbols;
wenzelm
parents: 61954
diff changeset
   127
  have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   128
    by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60500
diff changeset
   129
  also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   130
    by auto
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   131
  finally show ?thesis .
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   132
qed
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   133
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   134
lemma indicator_add:
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   135
  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   136
  unfolding indicator_def by auto
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   137
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   138
lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   139
  by (simp split: split_indicator)
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   140
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   141
lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   142
  by (simp split: split_indicator)
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   143
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   144
lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   145
  by (simp split: split_indicator)
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   146
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   147
lemma mult_indicator_subset:
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   148
  "A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::{comm_semiring_1})"
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   149
  by (auto split: split_indicator simp: fun_eq_iff)
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   150
62648
ee48e0b4f669 more stuff for extended nonnegative real numbers
hoelzl
parents: 62390
diff changeset
   151
lemma indicator_sums:
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   152
  assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   153
  shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   154
proof cases
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   155
  assume "\<exists>i. x \<in> A i"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   156
  then obtain i where i: "x \<in> A i" ..
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   157
  with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   158
    by (intro sums_finite) (auto split: split_indicator)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   159
  also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   160
    using i by (auto split: split_indicator)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   161
  finally show ?thesis .
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   162
qed simp
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57446
diff changeset
   163
57446
06e195515deb some lemmas about the indicator function; removed lemma sums_def2
hoelzl
parents: 57418
diff changeset
   164
end