--- 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
--- 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
--- 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 *}
--- 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