--- a/src/HOL/Library/Indicator_Function.thy Mon May 19 11:27:02 2014 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Mon May 19 12:04:45 2014 +0200
@@ -5,7 +5,7 @@
header {* Indicator Function *}
theory Indicator_Function
-imports Main
+imports Complex_Main
begin
definition "indicator S x = (if x \<in> S then 1 else 0)"
@@ -65,4 +65,9 @@
using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
unfolding card_eq_setsum by simp
+lemma setsum_indicator_scaleR[simp]:
+ "finite A \<Longrightarrow>
+ (\<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)"
+ using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm simp: indicator_def)
+
end
\ No newline at end of file