75 by (auto split: split_indicator) |
75 by (auto split: split_indicator) |
76 |
76 |
77 lemma (* FIXME unnamed!? *) |
77 lemma (* FIXME unnamed!? *) |
78 fixes f :: "'a \<Rightarrow> 'b::semiring_1" |
78 fixes f :: "'a \<Rightarrow> 'b::semiring_1" |
79 assumes "finite A" |
79 assumes "finite A" |
80 shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)" |
80 shows sum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)" |
81 and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)" |
81 and sum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)" |
82 unfolding indicator_def |
82 unfolding indicator_def |
83 using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm) |
83 using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm) |
84 |
84 |
85 lemma setsum_indicator_eq_card: |
85 lemma sum_indicator_eq_card: |
86 assumes "finite A" |
86 assumes "finite A" |
87 shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)" |
87 shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)" |
88 using setsum_mult_indicator [OF assms, of "\<lambda>x. 1::nat"] |
88 using sum_mult_indicator [OF assms, of "\<lambda>x. 1::nat"] |
89 unfolding card_eq_setsum by simp |
89 unfolding card_eq_sum by simp |
90 |
90 |
91 lemma setsum_indicator_scaleR[simp]: |
91 lemma sum_indicator_scaleR[simp]: |
92 "finite A \<Longrightarrow> |
92 "finite A \<Longrightarrow> |
93 (\<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)" |
93 (\<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)" |
94 by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def) |
94 by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm simp: indicator_def) |
95 |
95 |
96 lemma LIMSEQ_indicator_incseq: |
96 lemma LIMSEQ_indicator_incseq: |
97 assumes "incseq A" |
97 assumes "incseq A" |
98 shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
98 shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x" |
99 proof (cases "\<exists>i. x \<in> A i") |
99 proof (cases "\<exists>i. x \<in> A i") |