# HG changeset patch
# User hoelzl
# Date 1455006070 -3600
# Node ID 670063003ad33ef27ecc55ee29490ece38fdde56
# Parent  cb27a55d868a1e36f56cc8254ac5512e82fa2f15
add extended nonnegative real numbers

diff -r cb27a55d868a -r 670063003ad3 src/HOL/Library/Extended_Nonnegative_Real.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Feb 09 09:21:10 2016 +0100
@@ -0,0 +1,184 @@
+(*  Title:      HOL/Library/Extended_Nonnegative_Real.thy
+    Author:     Johannes Hölzl
+*)
+
+subsection \<open>The type of non-negative extended real numbers\<close>
+
+theory Extended_Nonnegative_Real
+  imports Extended_Real
+begin
+
+typedef ennreal = "{x :: ereal. 0 \<le> x}"
+  morphisms enn2ereal e2ennreal
+  by auto
+
+setup_lifting type_definition_ennreal
+
+
+lift_definition ennreal :: "real \<Rightarrow> ennreal" is "max 0 \<circ> ereal"
+  by simp
+
+declare [[coercion ennreal]]
+declare [[coercion e2ennreal]]
+
+instantiation ennreal :: semiring_1_no_zero_divisors
+begin
+
+lift_definition one_ennreal :: ennreal is 1 by simp
+lift_definition zero_ennreal :: ennreal is 0 by simp
+lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op +" by simp
+lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op *" by simp
+
+instance
+  by standard (transfer; auto simp: field_simps ereal_right_distrib)+
+
+end
+
+instance ennreal :: numeral ..
+
+instantiation ennreal :: inverse
+begin
+
+lift_definition inverse_ennreal :: "ennreal \<Rightarrow> ennreal" is inverse
+  by (rule inverse_ereal_ge0I)
+
+definition divide_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal"
+  where "x div y = x * inverse (y :: ennreal)"
+
+instance ..
+
+end
+
+
+instantiation ennreal :: complete_linorder
+begin
+
+lift_definition top_ennreal :: ennreal is top by simp
+lift_definition bot_ennreal :: ennreal is 0 by simp
+lift_definition sup_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is sup by (simp add: max.coboundedI1)
+lift_definition inf_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is inf by (simp add: min.boundedI)
+
+lift_definition Inf_ennreal :: "ennreal set \<Rightarrow> ennreal" is "Inf"
+  by (auto intro: Inf_greatest)
+
+lift_definition Sup_ennreal :: "ennreal set \<Rightarrow> ennreal" is "sup 0 \<circ> Sup"
+  by auto
+
+lift_definition less_eq_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op \<le>" .
+lift_definition less_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op <" .
+
+instance
+  by standard
+     (transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+
+
+end
+
+
+
+lemma ennreal_zero_less_one: "0 < (1::ennreal)"
+  by transfer auto
+
+instance ennreal :: ordered_comm_semiring
+  by standard
+     (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
+
+instantiation ennreal :: linear_continuum_topology
+begin
+
+definition open_ennreal :: "ennreal set \<Rightarrow> bool"
+  where "(open :: ennreal set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
+
+instance
+proof
+  show "\<exists>a b::ennreal. a \<noteq> b"
+    using ennreal_zero_less_one by (auto dest: order.strict_implies_not_eq)
+  show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y"
+  proof transfer
+    fix x y :: ereal assume "0 \<le> x" "x < y"
+    moreover from dense[OF this(2)] guess z ..
+    ultimately show "\<exists>z\<in>Collect (op \<le> 0). x < z \<and> z < y"
+      by (intro bexI[of _ z]) auto
+  qed
+qed (rule open_ennreal_def)
+
+end
+
+lemma ennreal_rat_dense:
+  fixes x y :: ennreal
+  shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
+proof transfer
+  fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y"
+  moreover
+  from ereal_dense3[OF \<open>x < y\<close>]
+  obtain r where "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
+    by auto
+  moreover then have "0 \<le> r"
+    using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
+  ultimately show "\<exists>r. x < (max 0 \<circ> ereal) (real_of_rat r) \<and> (max 0 \<circ> ereal) (real_of_rat r) < y"
+    by (intro exI[of _ r]) (auto simp: max_absorb2)
+qed
+
+lemma enn2ereal_range: "e2ennreal ` {0..} = UNIV"
+proof -
+  have "\<exists>y\<ge>0. x = e2ennreal y" for x
+    by (cases x) auto
+  then show ?thesis
+    by (auto simp: image_iff Bex_def)
+qed
+
+lemma enn2ereal_nonneg: "0 \<le> enn2ereal x"
+  using ennreal.enn2ereal[of x] by simp
+
+lemma ereal_ennreal_cases:
+  obtains b where "0 \<le> a" "a = enn2ereal b" | "a < 0"
+  using e2ennreal_inverse[of a, symmetric] by (cases "0 \<le> a") (auto intro: enn2ereal_nonneg)
+
+lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
+  using enn2ereal_nonneg
+  by (cases a rule: ereal_ennreal_cases)
+     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq
+           intro: le_less_trans less_imp_le)
+
+lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)"
+  using enn2ereal_nonneg
+  by (cases a rule: ereal_ennreal_cases)
+     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq
+           intro: less_le_trans)
+
+lemma continuous_e2ennreal: "continuous_on {0 ..} e2ennreal"
+  by (rule continuous_onI_mono)
+     (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
+
+lemma continuous_enn2ereal: "continuous_on UNIV enn2ereal"
+  by (rule continuous_on_generate_topology[OF open_generated_order])
+     (auto simp add: enn2ereal_Iio enn2ereal_Ioi)
+
+lemma transfer_enn2ereal_continuous_on [transfer_rule]:
+  "rel_fun (op =) (rel_fun (rel_fun op = pcr_ennreal) op =) continuous_on continuous_on"
+proof -
+  have "continuous_on A f" if "continuous_on A (\<lambda>x. enn2ereal (f x))" for A and f :: "'a \<Rightarrow> ennreal"
+    using continuous_on_compose2[OF continuous_e2ennreal that]
+    by (auto simp: ennreal.enn2ereal_inverse subset_eq enn2ereal_nonneg)
+  moreover
+  have "continuous_on A (\<lambda>x. enn2ereal (f x))" if "continuous_on A f" for A and f :: "'a \<Rightarrow> ennreal"
+    using continuous_on_compose2[OF continuous_enn2ereal that] by auto
+  ultimately
+  show ?thesis
+    by (auto simp add: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def)
+qed
+
+lemma continuous_on_add_ennreal[continuous_intros]:
+  fixes f g :: "'a::topological_space \<Rightarrow> ennreal"
+  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x + g x)"
+  by (transfer fixing: A) (auto intro!: tendsto_add_ereal_nonneg simp: continuous_on_def)
+
+lemma continuous_on_inverse_ennreal[continuous_intros]:
+  fixes f :: "_ \<Rightarrow> ennreal"
+  shows "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))"
+proof (transfer fixing: A)
+  show "pred_fun (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
+    for f :: "_ \<Rightarrow> ereal"
+    using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq)
+qed
+
+end
diff -r cb27a55d868a -r 670063003ad3 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Feb 19 12:25:57 2016 +0100
+++ b/src/HOL/Library/Library.thy	Tue Feb 09 09:21:10 2016 +0100
@@ -20,6 +20,7 @@
   Dlist
   Extended
   Extended_Nat
+  Extended_Nonnegative_Real
   Extended_Real
   FinFun
   Float
diff -r cb27a55d868a -r 670063003ad3 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Feb 19 12:25:57 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Feb 09 09:21:10 2016 +0100
@@ -11,6 +11,7 @@
 imports
   Topology_Euclidean_Space
   "~~/src/HOL/Library/Extended_Real"
+  "~~/src/HOL/Library/Extended_Nonnegative_Real"
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
@@ -85,6 +86,38 @@
   qed
 qed
 
+text \<open>This is a copy from \<open>ereal :: second_countable_topology\<close>. Maybe find a common super class of
+topological spaces where the rational numbers are densely embedded ?\<close>
+instance ennreal :: second_countable_topology
+proof (standard, intro exI conjI)
+  let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ennreal set set)"
+  show "countable ?B"
+    by (auto intro: countable_rat)
+  show "open = generate_topology ?B"
+  proof (intro ext iffI)
+    fix S :: "ennreal set"
+    assume "open S"
+    then show "generate_topology ?B S"
+      unfolding open_generated_order
+    proof induct
+      case (Basis b)
+      then obtain e where "b = {..<e} \<or> b = {e<..}"
+        by auto
+      moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}"
+        by (auto dest: ennreal_rat_dense
+                 simp del: ex_simps
+                 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff)
+      ultimately show ?case
+        by (auto intro: generate_topology.intros)
+    qed (auto intro: generate_topology.intros)
+  next
+    fix S
+    assume "generate_topology ?B S"
+    then show "open S"
+      by induct auto
+  qed
+qed
+
 lemma ereal_open_closed_aux:
   fixes S :: "ereal set"
   assumes "open S"
@@ -94,7 +127,7 @@
 proof (rule ccontr)
   assume "\<not> ?thesis"
   then have *: "Inf S \<in> S"
-    
+
     by (metis assms(2) closed_contains_Inf_cl)
   {
     assume "Inf S = -\<infinity>"
diff -r cb27a55d868a -r 670063003ad3 src/HOL/Probability/Weak_Convergence.thy
--- a/src/HOL/Probability/Weak_Convergence.thy	Fri Feb 19 12:25:57 2016 +0100
+++ b/src/HOL/Probability/Weak_Convergence.thy	Tue Feb 09 09:21:10 2016 +0100
@@ -27,11 +27,11 @@
 
 section \<open>Skorohod's theorem\<close>
 
-locale right_continuous_mono = 
+locale right_continuous_mono =
   fixes f :: "real \<Rightarrow> real" and a b :: real
   assumes cont: "\<And>x. continuous (at_right x) f"
   assumes mono: "mono f"
-  assumes bot: "(f \<longlongrightarrow> a) at_bot" 
+  assumes bot: "(f \<longlongrightarrow> a) at_bot"
   assumes top: "(f \<longlongrightarrow> b) at_top"
 begin
 
@@ -47,7 +47,7 @@
     by (auto intro!: bdd_belowI[of _ y] elim: mono_invE[OF _ less_le_trans])
 
   have ne: "?F \<noteq> {}"
-    using order_tendstoD(1)[OF top \<open>\<omega> < b\<close>] 
+    using order_tendstoD(1)[OF top \<open>\<omega> < b\<close>]
     by (auto dest!: eventually_happens'[OF trivial_limit_at_top_linorder] intro: less_imp_le)
 
   show "\<omega> \<le> f x \<Longrightarrow> I \<omega> \<le> x"
@@ -115,14 +115,14 @@
 context
   fixes \<mu> :: "nat \<Rightarrow> real measure"
     and M :: "real measure"
-  assumes \<mu>: "\<And>n. real_distribution (\<mu> n)" 
+  assumes \<mu>: "\<And>n. real_distribution (\<mu> n)"
   assumes M: "real_distribution M"
   assumes \<mu>_to_M: "weak_conv_m \<mu> M"
-begin  
+begin
 
 (* state using obtains? *)
 theorem Skorohod:
- "\<exists> (\<Omega> :: real measure) (Y_seq :: nat \<Rightarrow> real \<Rightarrow> real) (Y :: real \<Rightarrow> real). 
+ "\<exists> (\<Omega> :: real measure) (Y_seq :: nat \<Rightarrow> real \<Rightarrow> real) (Y :: real \<Rightarrow> real).
     prob_space \<Omega> \<and>
     (\<forall>n. Y_seq n \<in> measurable \<Omega> borel) \<and>
     (\<forall>n. distr \<Omega> borel (Y_seq n) = \<mu> n) \<and>
@@ -147,7 +147,7 @@
   have Y_distr: "distr ?\<Omega> borel M.I = M"
     by (rule M.distr_I_eq_M)
 
-  have Y_cts_cnv: "(\<lambda>n. \<mu>.I n \<omega>) \<longlonglongrightarrow> M.I \<omega>" 
+  have Y_cts_cnv: "(\<lambda>n. \<mu>.I n \<omega>) \<longlonglongrightarrow> M.I \<omega>"
     if \<omega>: "\<omega> \<in> {0<..<1}" "isCont M.I \<omega>" for \<omega> :: real
   proof (intro limsup_le_liminf_real)
     show "liminf (\<lambda>n. \<mu>.I n \<omega>) \<ge> M.I \<omega>"
@@ -196,7 +196,7 @@
         using \<open>y < B\<close>
         by (intro Limsup_bounded[rotated]) (auto intro: le_less_trans elim: eventually_mono)
     qed simp
-    
+
     have **: "(M.I \<longlongrightarrow> ereal (M.I \<omega>)) (at_right \<omega>)"
       using \<omega>(2) by (auto intro: tendsto_within_subset simp: continuous_at)
     show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>"
@@ -247,13 +247,13 @@
 \<close>
 
 theorem weak_conv_imp_bdd_ae_continuous_conv:
-  fixes 
+  fixes
     f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
-  assumes 
+  assumes
     discont_null: "M ({x. \<not> isCont f x}) = 0" and
     f_bdd: "\<And>x. norm (f x) \<le> B" and
     [measurable]: "f \<in> borel_measurable borel"
-  shows 
+  shows
     "(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f"
 proof -
   have "0 \<le> B"
@@ -278,10 +278,10 @@
 
 theorem weak_conv_imp_integral_bdd_continuous_conv:
   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
-  assumes 
+  assumes
     "\<And>x. isCont f x" and
     "\<And>x. norm (f x) \<le> B"
-  shows 
+  shows
     "(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f"
   using assms
   by (intro weak_conv_imp_bdd_ae_continuous_conv)
@@ -294,7 +294,7 @@
 proof -
   interpret M: real_distribution M by fact
   interpret \<mu>: real_distribution "\<mu> n" for n by fact
-  
+
   have "(\<lambda>n. (\<integral>x. indicator A x \<partial>\<mu> n) :: real) \<longlonglongrightarrow> (\<integral>x. indicator A x \<partial>M)"
     by (intro weak_conv_imp_bdd_ae_continuous_conv[where B=1])
        (auto intro: assms simp: isCont_indicator)
@@ -347,9 +347,9 @@
 context
   fixes M_seq :: "nat \<Rightarrow> real measure"
     and M :: "real measure"
-  assumes distr_M_seq [simp]: "\<And>n. real_distribution (M_seq n)" 
+  assumes distr_M_seq [simp]: "\<And>n. real_distribution (M_seq n)"
   assumes distr_M [simp]: "real_distribution M"
-begin  
+begin
 
 theorem continuity_set_conv_imp_weak_conv:
   fixes f :: "real \<Rightarrow> real"
@@ -364,9 +364,9 @@
 theorem integral_cts_step_conv_imp_weak_conv:
   assumes integral_conv: "\<And>x y. x < y \<Longrightarrow> (\<lambda>n. integral\<^sup>L (M_seq n) (cts_step x y)) \<longlonglongrightarrow> integral\<^sup>L M (cts_step x y)"
   shows "weak_conv_m M_seq M"
-  unfolding weak_conv_m_def weak_conv_def 
+  unfolding weak_conv_m_def weak_conv_def
 proof (clarsimp)
-  interpret real_distribution M by (rule distr_M) 
+  interpret real_distribution M by (rule distr_M)
   fix x assume "isCont (cdf M) x"
   hence left_cont: "continuous (at_left x) (cdf M)"
     unfolding continuous_at_split ..
@@ -400,13 +400,13 @@
       by (subst eventually_at_left[of "x - 1"]) (auto simp: ** intro: exI [of _ "x-1"])
   qed (insert left_cont, auto simp: continuous_within)
   ultimately show "(\<lambda>n. cdf (M_seq n) x) \<longlonglongrightarrow> cdf M x"
-    by (elim limsup_le_liminf_real) 
+    by (elim limsup_le_liminf_real)
 qed
 
 theorem integral_bdd_continuous_conv_imp_weak_conv:
-  assumes 
+  assumes
     "\<And>f. (\<And>x. isCont f x) \<Longrightarrow> (\<And>x. abs (f x) \<le> 1) \<Longrightarrow> (\<lambda>n. integral\<^sup>L (M_seq n) f::real) \<longlonglongrightarrow> integral\<^sup>L M f"
-  shows 
+  shows
     "weak_conv_m M_seq M"
   apply (rule integral_cts_step_conv_imp_weak_conv [OF assms])
   apply (rule continuous_on_interior)