Measures form a CCPO
authorhoelzl
Thu Jul 23 16:40:47 2015 +0200 (2015-07-23)
changeset 60772a0cfa9050fa8
parent 60771 8558e4a37b48
child 60773 d09c66a0ea10
Measures form a CCPO
src/HOL/Library/Extended_Real.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:39:10 2015 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:40:47 2015 +0200
     1.3 @@ -3182,6 +3182,77 @@
     1.4  qed
     1.5  
     1.6  
     1.7 +lemma SUP_ereal_add_directed:
     1.8 +  fixes f g :: "'a \<Rightarrow> ereal"
     1.9 +  assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
    1.10 +  assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
    1.11 +  shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
    1.12 +proof cases
    1.13 +  assume "I = {}" then show ?thesis
    1.14 +    by (simp add: bot_ereal_def)
    1.15 +next
    1.16 +  assume "I \<noteq> {}"
    1.17 +  show ?thesis
    1.18 +  proof (rule antisym)
    1.19 +    show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
    1.20 +      by (rule SUP_least; intro ereal_add_mono SUP_upper)
    1.21 +  next
    1.22 +    have "bot < (SUP i:I. g i)"
    1.23 +      using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff)
    1.24 +    then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
    1.25 +      by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto
    1.26 +    also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
    1.27 +      using nonneg(1) by (intro SUP_cong refl SUP_ereal_add_right[symmetric] \<open>I \<noteq> {}\<close>) auto
    1.28 +    also have "\<dots> \<le> (SUP i:I. f i + g i)"
    1.29 +      using directed by (intro SUP_least) (blast intro: SUP_upper2)
    1.30 +    finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
    1.31 +  qed
    1.32 +qed
    1.33 +
    1.34 +lemma SUP_ereal_setsum_directed:
    1.35 +  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
    1.36 +  assumes "I \<noteq> {}"
    1.37 +  assumes directed: "\<And>N i j. N \<subseteq> A \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f n i \<le> f n k \<and> f n j \<le> f n k"
    1.38 +  assumes nonneg: "\<And>n i. i \<in> I \<Longrightarrow> n \<in> A \<Longrightarrow> 0 \<le> f n i"
    1.39 +  shows "(SUP i:I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i:I. f n i)"
    1.40 +proof -
    1.41 +  have "N \<subseteq> A \<Longrightarrow> (SUP i:I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i:I. f n i)" for N
    1.42 +  proof (induction N rule: infinite_finite_induct)
    1.43 +    case (insert n N)
    1.44 +    moreover have "(SUP i:I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i:I. f n i) + (SUP i:I. \<Sum>l\<in>N. f l i)"
    1.45 +    proof (rule SUP_ereal_add_directed)
    1.46 +      fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)"
    1.47 +        using insert by (auto intro!: setsum_nonneg nonneg)
    1.48 +    next
    1.49 +      fix i j assume "i \<in> I" "j \<in> I"
    1.50 +      from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k ..
    1.51 +      then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" 
    1.52 +        by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono)
    1.53 +    qed
    1.54 +    ultimately show ?case
    1.55 +      by simp
    1.56 +  qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>)
    1.57 +  from this[of A] show ?thesis by simp
    1.58 +qed
    1.59 +
    1.60 +lemma suminf_SUP_eq_directed:
    1.61 +  fixes f :: "_ \<Rightarrow> nat \<Rightarrow> ereal"
    1.62 +  assumes "I \<noteq> {}"
    1.63 +  assumes directed: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
    1.64 +  assumes nonneg: "\<And>n i. 0 \<le> f n i"
    1.65 +  shows "(\<Sum>i. SUP n:I. f n i) = (SUP n:I. \<Sum>i. f n i)"
    1.66 +proof (subst (1 2) suminf_ereal_eq_SUP)
    1.67 +  show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n:I. f n i)"
    1.68 +    using \<open>I \<noteq> {}\<close> nonneg by (auto intro: SUP_upper2)
    1.69 +  show "(SUP n. \<Sum>i<n. SUP n:I. f n i) = (SUP n:I. SUP j. \<Sum>i<j. f n i)"
    1.70 +    apply (subst SUP_commute)
    1.71 +    apply (subst SUP_ereal_setsum_directed)
    1.72 +    apply (auto intro!: assms simp: finite_subset)
    1.73 +    done
    1.74 +qed
    1.75 +
    1.76 +subsection \<open>More Limits\<close>
    1.77 +
    1.78  lemma convergent_limsup_cl:
    1.79    fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    1.80    shows "convergent X \<Longrightarrow> limsup X = lim X"
     2.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Jul 23 16:39:10 2015 +0200
     2.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Jul 23 16:40:47 2015 +0200
     2.3 @@ -2053,5 +2053,174 @@
     2.4  lemma measure_null_measure[simp]: "measure (null_measure M) X = 0"
     2.5    by (simp add: measure_def)
     2.6  
     2.7 +subsection \<open>Measures form a chain-complete partial order\<close>
     2.8 +
     2.9 +instantiation measure :: (type) order_bot
    2.10 +begin
    2.11 +
    2.12 +definition bot_measure :: "'a measure" where
    2.13 +  "bot_measure = sigma {} {{}}"
    2.14 +
    2.15 +lemma space_bot[simp]: "space bot = {}"
    2.16 +  unfolding bot_measure_def by (rule space_measure_of) auto
    2.17 +
    2.18 +lemma sets_bot[simp]: "sets bot = {{}}"
    2.19 +  unfolding bot_measure_def by (subst sets_measure_of) auto
    2.20 +
    2.21 +lemma emeasure_bot[simp]: "emeasure bot = (\<lambda>x. 0)"
    2.22 +  unfolding bot_measure_def by (rule emeasure_sigma)
    2.23 +
    2.24 +inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
    2.25 +  "sets N = sets M \<Longrightarrow> (\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A \<le> emeasure N A) \<Longrightarrow> less_eq_measure M N"
    2.26 +| "less_eq_measure bot N"
    2.27 +
    2.28 +definition less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
    2.29 +  "less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
    2.30 +
    2.31 +instance
    2.32 +proof (standard, goals)
    2.33 +  case 1 then show ?case
    2.34 +    unfolding less_measure_def ..
    2.35 +next
    2.36 +  case (2 M) then show ?case
    2.37 +    by (intro less_eq_measure.intros) auto
    2.38 +next
    2.39 +  case (3 M N L) then show ?case
    2.40 +    apply (safe elim!: less_eq_measure.cases)
    2.41 +    apply (simp_all add: less_eq_measure.intros)
    2.42 +    apply (rule less_eq_measure.intros)
    2.43 +    apply simp
    2.44 +    apply (blast intro: order_trans) []
    2.45 +    unfolding less_eq_measure.simps
    2.46 +    apply (rule disjI2)
    2.47 +    apply simp
    2.48 +    apply (rule measure_eqI)
    2.49 +    apply (auto intro!: antisym)
    2.50 +    done
    2.51 +next
    2.52 +  case (4 M N) then show ?case
    2.53 +    apply (safe elim!: less_eq_measure.cases intro!: measure_eqI)
    2.54 +    apply simp
    2.55 +    apply simp
    2.56 +    apply (blast intro: antisym)
    2.57 +    apply (simp)
    2.58 +    apply (blast intro: antisym)
    2.59 +    apply simp
    2.60 +    done
    2.61 +qed (rule less_eq_measure.intros)
    2.62  end
    2.63  
    2.64 +lemma le_emeasureD: "M \<le> N \<Longrightarrow> emeasure M A \<le> emeasure N A"
    2.65 +  by (cases "A \<in> sets M") (auto elim!: less_eq_measure.cases simp: emeasure_notin_sets)
    2.66 +
    2.67 +lemma le_sets: "N \<le> M \<Longrightarrow> sets N \<le> sets M"
    2.68 +  unfolding less_eq_measure.simps by auto
    2.69 +
    2.70 +instantiation measure :: (type) ccpo
    2.71 +begin
    2.72 +
    2.73 +definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure" where
    2.74 +  "Sup_measure A = measure_of (SUP a:A. space a) (SUP a:A. sets a) (SUP a:A. emeasure a)"
    2.75 +
    2.76 +lemma
    2.77 +  assumes A: "Complete_Partial_Order.chain op \<le> A" and a: "a \<noteq> bot" "a \<in> A"
    2.78 +  shows space_Sup: "space (Sup A) = space a"
    2.79 +    and sets_Sup: "sets (Sup A) = sets a"
    2.80 +proof -
    2.81 +  have sets: "(SUP a:A. sets a) = sets a"
    2.82 +  proof (intro antisym SUP_least)
    2.83 +    fix a' show "a' \<in> A \<Longrightarrow> sets a' \<subseteq> sets a" 
    2.84 +      using a chainD[OF A, of a a'] by (auto elim!: less_eq_measure.cases)
    2.85 +  qed (insert \<open>a\<in>A\<close>, auto)
    2.86 +  have space: "(SUP a:A. space a) = space a"
    2.87 +  proof (intro antisym SUP_least)
    2.88 +    fix a' show "a' \<in> A \<Longrightarrow> space a' \<subseteq> space a" 
    2.89 +      using a chainD[OF A, of a a'] by (intro sets_le_imp_space_le) (auto elim!: less_eq_measure.cases)
    2.90 +  qed (insert \<open>a\<in>A\<close>, auto)
    2.91 +  show "space (Sup A) = space a"
    2.92 +    unfolding Sup_measure_def sets space sets.space_measure_of_eq ..
    2.93 +  show "sets (Sup A) = sets a"
    2.94 +    unfolding Sup_measure_def sets space sets.sets_measure_of_eq ..
    2.95 +qed
    2.96 +
    2.97 +lemma emeasure_Sup:
    2.98 +  assumes A: "Complete_Partial_Order.chain op \<le> A" "A \<noteq> {}"
    2.99 +  assumes "X \<in> sets (Sup A)"
   2.100 +  shows "emeasure (Sup A) X = (SUP a:A. emeasure a) X"
   2.101 +proof (rule emeasure_measure_of[OF Sup_measure_def])
   2.102 +  show "countably_additive (sets (Sup A)) (SUP a:A. emeasure a)"
   2.103 +    unfolding countably_additive_def
   2.104 +  proof safe
   2.105 +    fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> sets (Sup A)" "disjoint_family F"
   2.106 +    show "(\<Sum>i. (SUP a:A. emeasure a) (F i)) = SUPREMUM A emeasure (UNION UNIV F)"
   2.107 +      unfolding SUP_apply
   2.108 +    proof (subst suminf_SUP_eq_directed)
   2.109 +      fix N i j assume "i \<in> A" "j \<in> A"
   2.110 +      with A(1)
   2.111 +      show "\<exists>k\<in>A. \<forall>n\<in>N. emeasure i (F n) \<le> emeasure k (F n) \<and> emeasure j (F n) \<le> emeasure k (F n)"
   2.112 +        by (blast elim: chainE dest: le_emeasureD)
   2.113 +    next
   2.114 +      show "(SUP n:A. \<Sum>i. emeasure n (F i)) = (SUP y:A. emeasure y (UNION UNIV F))"
   2.115 +      proof (intro SUP_cong refl)
   2.116 +        fix a assume "a \<in> A" then show "(\<Sum>i. emeasure a (F i)) = emeasure a (UNION UNIV F)"
   2.117 +          using sets_Sup[OF A(1), of a] F by (cases "a = bot") (auto simp: suminf_emeasure)
   2.118 +      qed
   2.119 +    qed (insert F \<open>A \<noteq> {}\<close>, auto simp: suminf_emeasure intro!: SUP_cong)
   2.120 +  qed
   2.121 +qed (insert \<open>A \<noteq> {}\<close> \<open>X \<in> sets (Sup A)\<close>, auto simp: positive_def dest: sets.sets_into_space intro: SUP_upper2)
   2.122 +
   2.123 +instance
   2.124 +proof
   2.125 +  fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \<le> A" and x: "x \<in> A"
   2.126 +  show "x \<le> Sup A"
   2.127 +  proof cases
   2.128 +    assume "x \<noteq> bot"
   2.129 +    show ?thesis
   2.130 +    proof
   2.131 +      show "sets (Sup A) = sets x"
   2.132 +        using A \<open>x \<noteq> bot\<close> x by (rule sets_Sup)
   2.133 +      with x show "\<And>a. a \<in> sets x \<Longrightarrow> emeasure x a \<le> emeasure (Sup A) a"
   2.134 +        by (subst emeasure_Sup[OF A]) (auto intro: SUP_upper)
   2.135 +    qed
   2.136 +  qed simp
   2.137 +next
   2.138 +  fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \<le> A" and x: "\<And>z. z \<in> A \<Longrightarrow> z \<le> x"
   2.139 +  consider "A = {}" | "A = {bot}" | x where "x\<in>A" "x \<noteq> bot"
   2.140 +    by blast
   2.141 +  then show "Sup A \<le> x"
   2.142 +  proof cases
   2.143 +    assume "A = {}"
   2.144 +    moreover have "Sup ({}::'a measure set) = bot"
   2.145 +      by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI)
   2.146 +    ultimately show ?thesis
   2.147 +      by simp
   2.148 +  next
   2.149 +    assume "A = {bot}"
   2.150 +    moreover have "Sup ({bot}::'a measure set) = bot"
   2.151 +      by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI)
   2.152 +     ultimately show ?thesis
   2.153 +      by simp
   2.154 +  next
   2.155 +    fix a assume "a \<in> A" "a \<noteq> bot"
   2.156 +    then have "a \<le> x" "x \<noteq> bot" "a \<noteq> bot"
   2.157 +      using x[OF \<open>a \<in> A\<close>] by (auto simp: bot_unique)
   2.158 +    then have "sets x = sets a"
   2.159 +      by (auto elim: less_eq_measure.cases)
   2.160 +
   2.161 +    show "Sup A \<le> x"
   2.162 +    proof (rule less_eq_measure.intros)
   2.163 +      show "sets x = sets (Sup A)"
   2.164 +        by (subst sets_Sup[OF A \<open>a \<noteq> bot\<close> \<open>a \<in> A\<close>]) fact
   2.165 +    next
   2.166 +      fix X assume "X \<in> sets (Sup A)"
   2.167 +      then have "emeasure (Sup A) X \<le> (SUP a:A. emeasure a X)"
   2.168 +        using \<open>a\<in>A\<close> by (subst emeasure_Sup[OF A _]) auto
   2.169 +      also have "\<dots> \<le> emeasure x X"
   2.170 +        by (intro SUP_least le_emeasureD x)
   2.171 +      finally show "emeasure (Sup A) X \<le> emeasure x X" .
   2.172 +    qed
   2.173 +  qed
   2.174 +qed
   2.175 +end
   2.176 +
   2.177 +end
     3.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Jul 23 16:39:10 2015 +0200
     3.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Jul 23 16:40:47 2015 +0200
     3.3 @@ -1642,10 +1642,11 @@
     3.4    obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>-A. \<mu> a = 0" "measure_space \<Omega> A \<mu>"
     3.5    by atomize_elim (cases x, auto)
     3.6  
     3.7 -lemma sets_eq_imp_space_eq:
     3.8 -  "sets M = sets M' \<Longrightarrow> space M = space M'"
     3.9 -  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
    3.10 -  by blast
    3.11 +lemma sets_le_imp_space_le: "sets A \<subseteq> sets B \<Longrightarrow> space A \<subseteq> space B"
    3.12 +  by (auto dest: sets.sets_into_space)
    3.13 +
    3.14 +lemma sets_eq_imp_space_eq: "sets M = sets M' \<Longrightarrow> space M = space M'"
    3.15 +  by (auto intro!: antisym sets_le_imp_space_le)
    3.16  
    3.17  lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
    3.18    by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)