src/HOL/Probability/Caratheodory.thy
changeset 42950 6e5c2a3c69da
parent 42145 8448713d48b7
child 43920 cedb5cb948fd
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon May 23 10:58:21 2011 +0200
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon May 23 19:21:05 2011 +0200
     1.3 @@ -9,6 +9,12 @@
     1.4    imports Sigma_Algebra Extended_Real_Limits
     1.5  begin
     1.6  
     1.7 +lemma sums_def2:
     1.8 +  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
     1.9 +  unfolding sums_def
    1.10 +  apply (subst LIMSEQ_Suc_iff[symmetric])
    1.11 +  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
    1.12 +
    1.13  text {*
    1.14    Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
    1.15  *}
    1.16 @@ -853,12 +859,6 @@
    1.17  
    1.18  subsubsection {*Alternative instances of caratheodory*}
    1.19  
    1.20 -lemma sums_def2:
    1.21 -  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
    1.22 -  unfolding sums_def
    1.23 -  apply (subst LIMSEQ_Suc_iff[symmetric])
    1.24 -  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
    1.25 -
    1.26  lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
    1.27    assumes f: "positive M f" "additive M f"
    1.28    shows "countably_additive M f \<longleftrightarrow>
    1.29 @@ -900,28 +900,6 @@
    1.30    show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
    1.31  qed
    1.32  
    1.33 -lemma uminus_extreal_add_uminus_uminus:
    1.34 -  fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
    1.35 -  by (cases rule: extreal2_cases[of a b]) auto
    1.36 -
    1.37 -lemma INFI_extreal_add:
    1.38 -  assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
    1.39 -  shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
    1.40 -proof -
    1.41 -  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
    1.42 -    using assms unfolding INF_less_iff by auto
    1.43 -  { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
    1.44 -      by (rule uminus_extreal_add_uminus_uminus) }
    1.45 -  then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
    1.46 -    by simp
    1.47 -  also have "\<dots> = INFI UNIV f + INFI UNIV g"
    1.48 -    unfolding extreal_INFI_uminus
    1.49 -    using assms INF_less
    1.50 -    by (subst SUPR_extreal_add)
    1.51 -       (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
    1.52 -  finally show ?thesis .
    1.53 -qed
    1.54 -
    1.55  lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
    1.56    assumes f: "positive M f" "additive M f"
    1.57    shows "(\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> sets M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))