# 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) \ x \ A" by (auto simp: indicator_def) -lemma split_indicator: - "P (indicator S x) \ ((x \ S \ P 1) \ (x \ S \ P 0))" +lemma split_indicator: "P (indicator S x) \ ((x \ S \ P 1) \ (x \ S \ P 0))" + unfolding indicator_def by auto + +lemma split_indicator_asm: "P (indicator S x) \ (\ (x \ S \ \ P 1 \ x \ S \ \ P 0))" unfolding indicator_def by auto lemma indicator_inter_arith: "indicator (A \ 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 \ B) x = indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)" +lemma indicator_union_arith: "indicator (A \ 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 \ B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)" and indicator_union_max: "indicator (A \ 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 \ B = {} \ indicator (A \ 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 @@ (\x \ A. indicator (B x) (g x) *\<^sub>R f x) = (\x \ {x\A. g x \ 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 "(\i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\i. A i) x" +proof cases + assume "\i. x \ A i" + then obtain i where "x \ A i" + by auto + then have + "\n. (indicator (A (n + i)) x :: 'a) = 1" + "(indicator (\ i. A i) x :: 'a) = 1" + using incseqD[OF `incseq A`, of i "n + i" for n] `x \ 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: + "(\k. indicator (\ i indicator (\i. A i) x" +proof - + have "(\k. indicator (\ i indicator (\k. \ ik. \ ii. A i)" + by auto + finally show ?thesis . +qed + +lemma LIMSEQ_indicator_decseq: + assumes "decseq A" + shows "(\i. indicator (A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\i. A i) x" +proof cases + assume "\i. x \ A i" + then obtain i where "x \ A i" + by auto + then have + "\n. (indicator (A (n + i)) x :: 'a) = 0" + "(indicator (\i. A i) x :: 'a) = 0" + using decseqD[OF `decseq A`, of i "n + i" for n] `x \ 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: + "(\k. indicator (\i indicator (\i. A i) x" +proof - + have "(\k. indicator (\i indicator (\k. \ik. \ ii. A i)" + by auto + finally show ?thesis . +qed + +lemma indicator_add: + "A \ B = {} \ (indicator A x::_::monoid_add) + indicator B x = indicator (A \ 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: "\indicator A x :: 'a::linordered_idom\ = indicator A x" + by (simp split: split_indicator) + +lemma mult_indicator_subset: + "A \ B \ 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 \ (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 \ N \ \ sigma_algebra \ M \ M \ N \ measure_space \ M \" - 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 \ (\n. (\i\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 \ (indicator A x ::ereal)" - unfolding indicator_def by auto - -lemma LIMSEQ_indicator_UN: - "(\k. indicator (\ i (indicator (\i. A i) x :: real)" -proof cases - assume "\i. x \ A i" then guess i .. note i = this - then have *: "\n. (indicator (\ i 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 \ B = {} \ (indicator A x::_::monoid_add) + indicator B x = indicator (A \ B) x" - unfolding indicator_def by auto - lemma suminf_cmult_indicator: fixes f :: "nat \ ereal" assumes "disjoint_family A" "x \ A i" "\i. 0 \ f i" @@ -319,19 +289,19 @@ next assume cont: "\A. range A \ M \ incseq A \ (\i. A i) \ M \ (\i. f (A i)) ----> f (\i. A i)" fix A :: "nat \ 'a set" assume A: "range A \ M" "disjoint_family A" "(\i. A i) \ M" - have *: "(\n. (\i\n. A i)) = (\i. A i)" by auto - have "(\n. f (\i\n. A i)) ----> f (\i. A i)" + have *: "(\n. (\ii. A i)" by auto + have "(\n. f (\i f (\i. A i)" proof (unfold *[symmetric], intro cont[rule_format]) - show "range (\i. \ i\i. A i) \ M" "(\i. \ i\i. A i) \ M" + show "range (\i. \ i M" "(\i. \ i M" using A * by auto qed (force intro!: incseq_SucI) - moreover have "\n. f (\i\n. A i) = (\i\n. f (A i))" + moreover have "\n. f (\iii. f (A i)) sums f (\i. A i)" - unfolding sums_def2 by simp + unfolding sums_def by simp from sums_unique[OF this] show "(\i. f (A i)) = f (\i. A i)" by simp qed