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)" |
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) |
82 using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm simp: indicator_def) |
83 |
83 |
84 lemma LIMSEQ_indicator_incseq: |
84 lemma LIMSEQ_indicator_incseq: |
85 assumes "incseq A" |
85 assumes "incseq A" |
86 shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x" |
86 shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
87 proof cases |
87 proof cases |
88 assume "\<exists>i. x \<in> A i" |
88 assume "\<exists>i. x \<in> A i" |
89 then obtain i where "x \<in> A i" |
89 then obtain i where "x \<in> A i" |
90 by auto |
90 by auto |
91 then have |
91 then have |
95 then show ?thesis |
95 then show ?thesis |
96 by (rule_tac LIMSEQ_offset[of _ i]) simp |
96 by (rule_tac LIMSEQ_offset[of _ i]) simp |
97 qed (auto simp: indicator_def) |
97 qed (auto simp: indicator_def) |
98 |
98 |
99 lemma LIMSEQ_indicator_UN: |
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" |
100 "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
101 proof - |
101 proof - |
102 have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union>i<k. A i) x" |
102 have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x" |
103 by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans) |
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)" |
104 also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)" |
105 by auto |
105 by auto |
106 finally show ?thesis . |
106 finally show ?thesis . |
107 qed |
107 qed |
108 |
108 |
109 lemma LIMSEQ_indicator_decseq: |
109 lemma LIMSEQ_indicator_decseq: |
110 assumes "decseq A" |
110 assumes "decseq A" |
111 shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x" |
111 shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x" |
112 proof cases |
112 proof cases |
113 assume "\<exists>i. x \<notin> A i" |
113 assume "\<exists>i. x \<notin> A i" |
114 then obtain i where "x \<notin> A i" |
114 then obtain i where "x \<notin> A i" |
115 by auto |
115 by auto |
116 then have |
116 then have |
120 then show ?thesis |
120 then show ?thesis |
121 by (rule_tac LIMSEQ_offset[of _ i]) simp |
121 by (rule_tac LIMSEQ_offset[of _ i]) simp |
122 qed (auto simp: indicator_def) |
122 qed (auto simp: indicator_def) |
123 |
123 |
124 lemma LIMSEQ_indicator_INT: |
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" |
125 "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x" |
126 proof - |
126 proof - |
127 have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x" |
127 have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x" |
128 by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans) |
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)" |
129 also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)" |
130 by auto |
130 by auto |
131 finally show ?thesis . |
131 finally show ?thesis . |
132 qed |
132 qed |