6 |
6 |
7 theory Indicator_Function |
7 theory Indicator_Function |
8 imports Complex_Main Disjoint_Sets |
8 imports Complex_Main Disjoint_Sets |
9 begin |
9 begin |
10 |
10 |
11 definition "indicator S x = (if x \<in> S then 1 else 0)" |
11 definition "indicator S x = of_bool (x \<in> S)" |
12 |
12 |
13 text\<open>Type constrained version\<close> |
13 text\<open>Type constrained version\<close> |
14 abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S" |
14 abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S" |
15 |
15 |
16 lemma indicator_simps[simp]: |
16 lemma indicator_simps[simp]: |
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)" |
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) |
97 by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm simp: indicator_def) |
98 |
98 |
99 lemma LIMSEQ_indicator_incseq: |
99 lemma LIMSEQ_indicator_incseq: |
100 assumes "incseq A" |
100 assumes "incseq A" |
101 shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
101 shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
102 proof (cases "\<exists>i. x \<in> A i") |
102 proof (cases "\<exists>i. x \<in> A i") |
103 case True |
103 case True |
104 then obtain i where "x \<in> A i" |
104 then obtain i where "x \<in> A i" |
105 by auto |
105 by auto |
106 then have *: |
106 then have *: |
113 case False |
113 case False |
114 then show ?thesis by (simp add: indicator_def) |
114 then show ?thesis by (simp add: indicator_def) |
115 qed |
115 qed |
116 |
116 |
117 lemma LIMSEQ_indicator_UN: |
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" |
118 "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
119 proof - |
119 proof - |
120 have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x" |
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) |
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)" |
122 also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)" |
123 by auto |
123 by auto |
124 finally show ?thesis . |
124 finally show ?thesis . |
125 qed |
125 qed |
126 |
126 |
127 lemma LIMSEQ_indicator_decseq: |
127 lemma LIMSEQ_indicator_decseq: |
128 assumes "decseq A" |
128 assumes "decseq A" |
129 shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x" |
129 shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x" |
130 proof (cases "\<exists>i. x \<notin> A i") |
130 proof (cases "\<exists>i. x \<notin> A i") |
131 case True |
131 case True |
132 then obtain i where "x \<notin> A i" |
132 then obtain i where "x \<notin> A i" |
133 by auto |
133 by auto |
134 then have *: |
134 then have *: |
141 case False |
141 case False |
142 then show ?thesis by (simp add: indicator_def) |
142 then show ?thesis by (simp add: indicator_def) |
143 qed |
143 qed |
144 |
144 |
145 lemma LIMSEQ_indicator_INT: |
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" |
146 "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a::{topological_space,zero_neq_one}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x" |
147 proof - |
147 proof - |
148 have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x" |
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) |
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)" |
150 also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)" |
151 by auto |
151 by auto |