# HG changeset patch
# User hoelzl
# Date 1404135903 -7200
# Node ID 06e195515deb7d490bdc85cc4afb772465f1541c
# Parent  2d0cf40f6fb3c9754796d5242fc2322963504bbc
some lemmas about the indicator function; removed lemma sums_def2

diff -r 2d0cf40f6fb3 -r 06e195515deb src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Tue Jul 01 11:06:31 2014 +0200
+++ b/src/HOL/Library/Indicator_Function.thy	Mon Jun 30 15:45:03 2014 +0200
@@ -28,20 +28,25 @@
 lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A"
   by (auto simp: indicator_def)
 
-lemma split_indicator:
-  "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
+lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
+  unfolding indicator_def by auto
+
+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))"
   unfolding indicator_def by auto
 
 lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
   unfolding indicator_def by (auto simp: min_def max_def)
 
-lemma indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
+lemma indicator_union_arith: "indicator (A \<union> B) x = indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
   unfolding indicator_def by (auto simp: min_def max_def)
 
 lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
   and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
   unfolding indicator_def by (auto simp: min_def max_def)
 
+lemma indicator_disj_union: "A \<inter> B = {} \<Longrightarrow>  indicator (A \<union> B) x = (indicator A x + indicator B x::'a::linordered_semidom)"
+  by (auto split: split_indicator)
+
 lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
   and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
   unfolding indicator_def by (auto simp: min_def max_def)
@@ -70,4 +75,71 @@
     (\<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_neutral_cong_right split: split_if_asm simp: indicator_def)
 
-end
\ No newline at end of file
+lemma LIMSEQ_indicator_incseq:
+  assumes "incseq A"
+  shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
+proof cases
+  assume "\<exists>i. x \<in> A i"
+  then obtain i where "x \<in> A i"
+    by auto
+  then have 
+    "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
+    "(indicator (\<Union> i. A i) x :: 'a) = 1"
+    using incseqD[OF `incseq A`, of i "n + i" for n] `x \<in> A i` by (auto simp: indicator_def)
+  then show ?thesis
+    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
+qed (auto simp: indicator_def tendsto_const)
+
+lemma LIMSEQ_indicator_UN:
+  "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
+proof -
+  have "(\<lambda>k. indicator (\<Union> i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union> i<k. A i) x"
+    by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
+  also have "(\<Union>k. \<Union> i<k. A i) = (\<Union>i. A i)"
+    by auto
+  finally show ?thesis .
+qed
+
+lemma LIMSEQ_indicator_decseq:
+  assumes "decseq A"
+  shows "(\<lambda>i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
+proof cases
+  assume "\<exists>i. x \<notin> A i"
+  then obtain i where "x \<notin> A i"
+    by auto
+  then have 
+    "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
+    "(indicator (\<Inter>i. A i) x :: 'a) = 0"
+    using decseqD[OF `decseq A`, of i "n + i" for n] `x \<notin> A i` by (auto simp: indicator_def)
+  then show ?thesis
+    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
+qed (auto simp: indicator_def tendsto_const)
+
+lemma LIMSEQ_indicator_INT:
+  "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
+proof -
+  have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
+    by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
+  also have "(\<Inter>k. \<Inter> i<k. A i) = (\<Inter>i. A i)"
+    by auto
+  finally show ?thesis .
+qed
+
+lemma indicator_add:
+  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
+  unfolding indicator_def by auto
+
+lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
+  by (simp split: split_indicator)
+
+lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
+  by (simp split: split_indicator)
+
+lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x"
+  by (simp split: split_indicator)
+
+lemma mult_indicator_subset:
+  "A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::{comm_semiring_1})"
+  by (auto split: split_indicator simp: fun_eq_iff)
+
+end
diff -r 2d0cf40f6fb3 -r 06e195515deb src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Jul 01 11:06:31 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Jun 30 15:45:03 2014 +0200
@@ -8,7 +8,7 @@
 header {* Limits on the Extended real number line *}
 
 theory Extended_Real_Limits
-  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real"
+  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
 begin
 
 lemma convergent_limsup_cl:
@@ -1425,4 +1425,18 @@
     by auto
 qed
 
+subsection "Relate extended reals and the indicator function"
+
+lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
+  by (auto simp: indicator_def one_ereal_def)
+
+lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
+  by (simp split: split_indicator)
+
+lemma ereal_indicator_mult: "ereal (indicator A y * x) = indicator A y * ereal x"
+  by (simp split: split_indicator)
+
+lemma ereal_indicator_nonneg[simp, intro]: "0 \<le> (indicator A x ::ereal)"
+  unfolding indicator_def by auto
+
 end
diff -r 2d0cf40f6fb3 -r 06e195515deb src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Tue Jul 01 11:06:31 2014 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Mon Jun 30 15:45:03 2014 +0200
@@ -640,8 +640,7 @@
 
 lemma measure_down:
   "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
-  by (simp add: measure_space_def positive_def countably_additive_def)
-     blast
+  by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)
 
 subsection {* Caratheodory's theorem *}
 
diff -r 2d0cf40f6fb3 -r 06e195515deb src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Tue Jul 01 11:06:31 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Mon Jun 30 15:45:03 2014 +0200
@@ -8,41 +8,11 @@
 
 theory Measure_Space
 imports
-  Measurable
-  "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
+  Measurable Multivariate_Analysis
 begin
 
-lemma sums_def2:
-  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
-  unfolding sums_def
-  apply (subst LIMSEQ_Suc_iff[symmetric])
-  unfolding lessThan_Suc_atMost ..
-
 subsection "Relate extended reals and the indicator function"
 
-lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
-  by (auto simp: indicator_def one_ereal_def)
-
-lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
-  by (simp split: split_indicator)
-
-lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
-  unfolding indicator_def by auto
-
-lemma LIMSEQ_indicator_UN:
-  "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
-proof cases
-  assume "\<exists>i. x \<in> A i" then guess i .. note i = this
-  then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
-    "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
-  show ?thesis
-    apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
-qed (auto simp: indicator_def)
-
-lemma indicator_add:
-  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
-  unfolding indicator_def by auto
-
 lemma suminf_cmult_indicator:
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
@@ -319,19 +289,19 @@
 next
   assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
-  have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
-  have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
+  have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
+  have "(\<lambda>n. f (\<Union>i<n. A i)) ----> f (\<Union>i. A i)"
   proof (unfold *[symmetric], intro cont[rule_format])
-    show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> M"
+    show "range (\<lambda>i. \<Union> i<i. A i) \<subseteq> M" "(\<Union>i. \<Union> i<i. A i) \<in> M"
       using A * by auto
   qed (force intro!: incseq_SucI)
-  moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
+  moreover have "\<And>n. f (\<Union>i<n. A i) = (\<Sum>i<n. f (A i))"
     using A
     by (intro additive_sum[OF f, of _ A, symmetric])
        (auto intro: disjoint_family_on_mono[where B=UNIV])
   ultimately
   have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
-    unfolding sums_def2 by simp
+    unfolding sums_def by simp
   from sums_unique[OF this]
   show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
 qed