moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

--- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -559,4 +559,62 @@
 qed
 end
 
+lemma interval_cases:
+  fixes S :: "'a :: conditionally_complete_linorder set"
+  assumes ivl: "\<And>a b x. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> x \<in> S"
+  shows "\<exists>a b. S = {} \<or>
+    S = UNIV \<or>
+    S = {..<b} \<or>
+    S = {..b} \<or>
+    S = {a<..} \<or>
+    S = {a..} \<or>
+    S = {a<..<b} \<or>
+    S = {a<..b} \<or>
+    S = {a..<b} \<or>
+    S = {a..b}"
+proof -
+  def lower \<equiv> "{x. \<exists>s\<in>S. s \<le> x}" and upper \<equiv> "{x. \<exists>s\<in>S. x \<le> s}"
+  with ivl have "S = lower \<inter> upper"
+    by auto
+  moreover 
+  have "\<exists>a. upper = UNIV \<or> upper = {} \<or> upper = {.. a} \<or> upper = {..< a}"
+  proof cases
+    assume *: "bdd_above S \<and> S \<noteq> {}"
+    from * have "upper \<subseteq> {.. Sup S}"
+      by (auto simp: upper_def intro: cSup_upper2)
+    moreover from * have "{..< Sup S} \<subseteq> upper"
+      by (force simp add: less_cSup_iff upper_def subset_eq Ball_def)
+    ultimately have "upper = {.. Sup S} \<or> upper = {..< Sup S}"
+      unfolding ivl_disj_un(2)[symmetric] by auto
+    then show ?thesis by auto
+  next
+    assume "\<not> (bdd_above S \<and> S \<noteq> {})"
+    then have "upper = UNIV \<or> upper = {}"
+      by (auto simp: upper_def bdd_above_def not_le dest: less_imp_le)
+    then show ?thesis
+      by auto
+  qed
+  moreover
+  have "\<exists>b. lower = UNIV \<or> lower = {} \<or> lower = {b ..} \<or> lower = {b <..}"
+  proof cases
+    assume *: "bdd_below S \<and> S \<noteq> {}"
+    from * have "lower \<subseteq> {Inf S ..}"
+      by (auto simp: lower_def intro: cInf_lower2)
+    moreover from * have "{Inf S <..} \<subseteq> lower"
+      by (force simp add: cInf_less_iff lower_def subset_eq Ball_def)
+    ultimately have "lower = {Inf S ..} \<or> lower = {Inf S <..}"
+      unfolding ivl_disj_un(1)[symmetric] by auto
+    then show ?thesis by auto
+  next
+    assume "\<not> (bdd_below S \<and> S \<noteq> {})"
+    then have "lower = UNIV \<or> lower = {}"
+      by (auto simp: lower_def bdd_below_def not_le dest: less_imp_le)
+    then show ?thesis
+      by auto
+  qed
+  ultimately show ?thesis
+    unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def
+    by (elim exE disjE) auto
+qed
+
 end

--- a/src/HOL/Groups_Big.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1317,4 +1317,8 @@
   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
 
+lemma (in ordered_comm_monoid_add) setsum_pos: 
+  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
+  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
+
 end

--- a/src/HOL/Hilbert_Choice.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -98,6 +98,18 @@
 lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))"
 by (fast elim: someI)
 
+lemma dependent_nat_choice:
+  assumes  1: "\<exists>x. P x" and 
+           2: "\<And>x n. P x \<Longrightarrow> \<exists>y. P y \<and> Q n x y"
+  shows "\<exists>f. \<forall>n. P (f n) \<and> Q n (f n) (f (Suc n))"
+proof (intro exI allI conjI)
+  fix n def f \<equiv> "rec_nat (SOME x. P x) (\<lambda>n x. SOME y. P y \<and> Q n x y)"
+  then have "P (f 0)" "\<And>n. P (f n) \<Longrightarrow> P (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
+    using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def)
+  then show "P (f n)" "Q n (f n) (f (Suc n))"
+    by (induct n) auto
+qed
+
 subsection {*Function Inverse*}
 
 lemma inv_def: "inv f = (%y. SOME x. f x = y)"

--- a/src/HOL/Limits.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Limits.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -54,6 +54,11 @@
   "at_bot \<le> (at_infinity :: real filter)"
   unfolding at_infinity_eq_at_top_bot by simp
 
+lemma filterlim_at_top_imp_at_infinity:
+  fixes f :: "_ \<Rightarrow> real"
+  shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
+  by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
+
 subsubsection {* Boundedness *}
 
 definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1855,7 +1855,7 @@
     from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \<in> I" "f y < a"
       by auto
     then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
-      unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
+      unfolding eventually_at_right[OF `x < y`] by (metis less_imp_le le_less_trans mono)
     then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
       unfolding eventually_at_filter by eventually_elim simp
   qed

--- a/src/HOL/NthRoot.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/NthRoot.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -538,6 +538,10 @@
   shows "4 * x\<^sup>2 = (2 * x)\<^sup>2"
 by (simp add: power2_eq_square)
 
+lemma sqrt_at_top: "LIM x at_top. sqrt x :: real :> at_top"
+  by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="power2"])
+     (auto intro: eventually_gt_at_top)
+
 subsection {* Square Root of Sum of Squares *}
 
 lemma sum_squares_bound: 

--- a/src/HOL/Probability/Bochner_Integration.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1235,6 +1235,30 @@
   qed fact
 qed
 
+lemma integrableI_bounded_set:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M"
+  assumes finite: "emeasure M A < \<infinity>"
+    and bnd: "AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B"
+    and null: "AE x in M. x \<notin> A \<longrightarrow> f x = 0"
+  shows "integrable M f"
+proof (rule integrableI_bounded)
+  { fix x :: 'b have "norm x \<le> B \<Longrightarrow> 0 \<le> B"
+      using norm_ge_zero[of x] by arith }
+  with bnd null have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (max 0 B) * indicator A x \<partial>M)"
+    by (intro nn_integral_mono_AE) (auto split: split_indicator split_max)
+  also have "\<dots> < \<infinity>"
+    using finite by (subst nn_integral_cmult_indicator) (auto simp: max_def)
+  finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
+qed simp
+
+lemma integrableI_bounded_set_indicator:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  shows "A \<in> sets M \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow>
+    emeasure M A < \<infinity> \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B) \<Longrightarrow>
+    integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+  by (rule integrableI_bounded_set[where A=A]) auto
+
 lemma integrableI_nonneg:
   fixes f :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
@@ -1267,6 +1291,11 @@
   finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" .
 qed 
 
+lemma integrable_mult_indicator:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+  by (rule integrable_bound[of M f]) (auto split: split_indicator)
+
 lemma integrable_abs[simp, intro]:
   fixes f :: "'a \<Rightarrow> real"
   assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
@@ -1282,11 +1311,21 @@
   assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f"
   using assms by (rule integrable_bound) auto
 
+lemma integrable_norm_iff:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. norm (f x)) \<longleftrightarrow> integrable M f"
+  by (auto intro: integrable_norm_cancel)
+
 lemma integrable_abs_cancel:
   fixes f :: "'a \<Rightarrow> real"
   assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f"
   using assms by (rule integrable_bound) auto
 
+lemma integrable_abs_iff:
+  fixes f :: "'a \<Rightarrow> real"
+  shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
+  by (auto intro: integrable_abs_cancel)
+
 lemma integrable_max[simp, intro]:
   fixes f :: "'a \<Rightarrow> real"
   assumes fg[measurable]: "integrable M f" "integrable M g"
@@ -1330,6 +1369,65 @@
   finally show ?thesis .
 qed
 
+lemma integrable_discrete_difference:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes X: "countable X"
+  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
+  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
+  shows "integrable M f \<longleftrightarrow> integrable M g"
+  unfolding integrable_iff_bounded
+proof (rule conj_cong)
+  { assume "f \<in> borel_measurable M" then have "g \<in> borel_measurable M"
+      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
+  moreover
+  { assume "g \<in> borel_measurable M" then have "f \<in> borel_measurable M"
+      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
+  ultimately show "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" ..
+next
+  have "AE x in M. x \<notin> X"
+    by (rule AE_discrete_difference) fact+
+  then have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. norm (g x) \<partial>M)"
+    by (intro nn_integral_cong_AE) (auto simp: eq)
+  then show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity> \<longleftrightarrow> (\<integral>\<^sup>+ x. norm (g x) \<partial>M) < \<infinity>"
+    by simp
+qed
+
+lemma integral_discrete_difference:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes X: "countable X"
+  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
+  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
+  shows "integral\<^sup>L M f = integral\<^sup>L M g"
+proof (rule integral_eq_cases)
+  show eq: "integrable M f \<longleftrightarrow> integrable M g"
+    by (rule integrable_discrete_difference[where X=X]) fact+
+
+  assume f: "integrable M f"
+  show "integral\<^sup>L M f = integral\<^sup>L M g"
+  proof (rule integral_cong_AE)
+    show "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+      using f eq by (auto intro: borel_measurable_integrable)
+
+    have "AE x in M. x \<notin> X"
+      by (rule AE_discrete_difference) fact+
+    with AE_space show "AE x in M. f x = g x"
+      by eventually_elim fact
+  qed
+qed
+
+lemma has_bochner_integral_discrete_difference:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes X: "countable X"
+  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
+  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
+  shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
+  using integrable_discrete_difference[of X M f g, OF assms]
+  using integral_discrete_difference[of X M f g, OF assms]
+  by (metis has_bochner_integral_iff)
+
 lemma
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
@@ -2188,54 +2286,28 @@
   shows "integral\<^sup>L M X < integral\<^sup>L M Y"
   using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
 
-lemma integrable_mult_indicator:
-  fixes f :: "'a \<Rightarrow> real"
-  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
-  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"]) (auto split: split_indicator)
-
 lemma tendsto_integral_at_top:
-  fixes f :: "real \<Rightarrow> real"
-  assumes M: "sets M = sets borel" and f[measurable]: "integrable M f"
-  shows "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
-proof -
-  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
-    using M by (simp add: sets_eq_imp_space_eq measurable_def)
-  { fix f :: "real \<Rightarrow> real" assume f: "integrable M f" "\<And>x. 0 \<le> f x"
-    then have [measurable]: "f \<in> borel_measurable borel"
-      by (simp add: real_integrable_def)
-    have "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
-    proof (rule tendsto_at_topI_sequentially)
-      have int: "\<And>n. integrable M (\<lambda>x. f x * indicator {.. n} x)"
-        by (rule integrable_mult_indicator) (auto simp: M f)
-      show "(\<lambda>n. \<integral> x. f x * indicator {..real n} x \<partial>M) ----> integral\<^sup>L M f"
-      proof (rule integral_dominated_convergence)
-        { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
-            by (rule eventually_sequentiallyI[of "natceiling x"])
-               (auto split: split_indicator simp: natceiling_le_eq) }
-        from filterlim_cong[OF refl refl this]
-        show "AE x in M. (\<lambda>n. f x * indicator {..real n} x) ----> f x"
-          by (simp add: tendsto_const)
-        show "\<And>j. AE x in M. norm (f x * indicator {.. j} x) \<le> f x"
-          using f(2) by (intro AE_I2) (auto split: split_indicator)
-      qed (simp | fact)+
-      show "mono (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
-        by (intro monoI integral_mono int) (auto split: split_indicator intro: f)
-    qed }
-  note nonneg = this
-  let ?P = "\<lambda>y. \<integral> x. max 0 (f x) * indicator {..y} x \<partial>M"
-  let ?N = "\<lambda>y. \<integral> x. max 0 (- f x) * indicator {..y} x \<partial>M"
-  let ?p = "integral\<^sup>L M (\<lambda>x. max 0 (f x))"
-  let ?n = "integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
-  have "(?P ---> ?p) at_top" "(?N ---> ?n) at_top"
-    by (auto intro!: nonneg f)
-  note tendsto_diff[OF this]
-  also have "(\<lambda>y. ?P y - ?N y) = (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
-    by (subst integral_diff[symmetric])
-       (auto intro!: integrable_mult_indicator f integral_cong
-             simp: M split: split_max)
-  also have "?p - ?n = integral\<^sup>L M f"
-    by (subst integral_diff[symmetric]) (auto intro!: f integral_cong simp: M split: split_max)
-  finally show ?thesis .
+  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes [simp]: "sets M = sets borel" and f[measurable]: "integrable M f"
+  shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
+proof (rule tendsto_at_topI_sequentially)
+  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
+  show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) ----> integral\<^sup>L M f"
+  proof (rule integral_dominated_convergence)
+    show "integrable M (\<lambda>x. norm (f x))"
+      by (rule integrable_norm) fact
+    show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
+    proof
+      fix x
+      from `filterlim X at_top sequentially` 
+      have "eventually (\<lambda>n. x \<le> X n) sequentially"
+        unfolding filterlim_at_top_ge[where c=x] by auto
+      then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
+        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_elim1)
+    qed
+    fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
+      by (auto split: split_indicator)
+  qed auto
 qed
 
 lemma

--- a/src/HOL/Probability/Borel_Space.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -159,6 +159,18 @@
     using A by auto
 qed
 
+lemma borel_measurable_continuous_countable_exceptions:
+  fixes f :: "'a::t1_space \<Rightarrow> 'b::topological_space"
+  assumes X: "countable X"
+  assumes "continuous_on (- X) f"
+  shows "f \<in> borel_measurable borel"
+proof (rule measurable_discrete_difference[OF _ X])
+  have "X \<in> sets borel"
+    by (rule sets.countable[OF _ X]) auto
+  then show "(\<lambda>x. if x \<in> X then undefined else f x) \<in> borel_measurable borel"
+    by (intro borel_measurable_continuous_on_if assms continuous_intros)
+qed auto
+
 lemma borel_measurable_continuous_on1:
   "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
   using borel_measurable_continuous_on_if[of UNIV f "\<lambda>_. undefined"]
@@ -691,6 +703,10 @@
 lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
   by (intro borel_measurable_continuous_on1 continuous_intros)
 
+lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \<Rightarrow> 'a) \<in> borel_measurable borel"
+  by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"])
+     (auto intro!: continuous_on_sgn continuous_on_id)
+
 lemma borel_measurable_uminus[measurable (raw)]:
   fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes g: "g \<in> borel_measurable M"
@@ -780,21 +796,18 @@
   using affine_borel_measurable_vector[of f M a 1] by simp
 
 lemma borel_measurable_inverse[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_div_algebra}"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
-proof -
-  have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
-    by (intro borel_measurable_continuous_on_open' continuous_intros) auto
-  also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
-    by (intro ext) auto
-  finally show ?thesis using f by simp
-qed
+  apply (rule measurable_compose[OF f])
+  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
+  apply (auto intro!: continuous_on_inverse continuous_on_id)
+  done
 
 lemma borel_measurable_divide[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
-    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_field}) \<in> borel_measurable M"
-  by (simp add: field_divide_inverse)
+    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \<in> borel_measurable M"
+  by (simp add: divide_inverse)
 
 lemma borel_measurable_max[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
@@ -846,19 +859,10 @@
 lemma borel_measurable_ln[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
-proof -
-  { fix x :: real assume x: "x \<le> 0"
-    { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
-    from this[of x] x this[of 0] have "ln 0 = ln x"
-      by (auto simp: ln_def) }
-  note ln_imp = this
-  have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
-    by (rule borel_measurable_continuous_on_open[OF _ _ f])
-       (auto intro!: continuous_intros)
-  also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
-    by (simp add: fun_eq_iff not_less ln_imp)
-  finally show ?thesis .
-qed
+  apply (rule measurable_compose[OF f])
+  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
+  apply (auto intro!: continuous_on_ln continuous_on_id)
+  done
 
 lemma borel_measurable_log[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"

--- a/src/HOL/Probability/Distributions.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -9,258 +9,6 @@
   imports Convolution Information
 begin
 
-lemma tendsto_at_topI_sequentially:
-  fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
-  assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) ----> y"
-  shows "(f ---> y) at_top"
-  unfolding filterlim_iff
-proof safe
-  fix P assume "eventually P (nhds y)"
-  then have seq: "\<And>f. f ----> y \<Longrightarrow> eventually (\<lambda>x. P (f x)) at_top"
-    unfolding eventually_nhds_iff_sequentially by simp
-
-  show "eventually (\<lambda>x. P (f x)) at_top"
-  proof (rule ccontr)
-    assume "\<not> eventually (\<lambda>x. P (f x)) at_top"
-    then have "\<And>X. \<exists>x>X. \<not> P (f x)"
-      unfolding eventually_at_top_dense by simp
-    then obtain r where not_P: "\<And>x. \<not> P (f (r x))" and r: "\<And>x. x < r x"
-      by metis
-    
-    def s \<equiv> "rec_nat (r 0) (\<lambda>_ x. r (x + 1))"
-    then have [simp]: "s 0 = r 0" "\<And>n. s (Suc n) = r (s n + 1)"
-      by auto
-
-    { fix n have "n < s n" using r
-        by (induct n) (auto simp add: real_of_nat_Suc intro: less_trans add_strict_right_mono) }
-    note s_subseq = this
-
-    have "mono s"
-    proof (rule incseq_SucI)
-      fix n show "s n \<le> s (Suc n)"
-        using r[of "s n + 1"] by simp
-    qed
-
-    have "filterlim s at_top sequentially"
-      unfolding filterlim_at_top_gt[where c=0] eventually_sequentially
-    proof (safe intro!: exI)
-      fix Z :: real and n assume "0 < Z" "natceiling Z \<le> n"
-      with real_natceiling_ge[of Z] `n < s n`
-      show "Z \<le> s n"
-        by auto
-    qed
-    moreover then have "eventually (\<lambda>x. P (f (s x))) sequentially"
-      by (rule seq[OF *])
-    then obtain n where "P (f (s n))"
-      by (auto simp: eventually_sequentially)
-    then show False
-      using not_P by (cases n) auto
-  qed
-qed
-  
-lemma tendsto_integral_at_top:
-  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
-  assumes [simp]: "sets M = sets borel" and f[measurable]: "integrable M f"
-  shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
-proof (rule tendsto_at_topI_sequentially)
-  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
-  show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) ----> integral\<^sup>L M f"
-  proof (rule integral_dominated_convergence)
-    show "integrable M (\<lambda>x. norm (f x))"
-      by (rule integrable_norm) fact
-    show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
-    proof
-      fix x
-      from `filterlim X at_top sequentially` 
-      have "eventually (\<lambda>n. x \<le> X n) sequentially"
-        unfolding filterlim_at_top_ge[where c=x] by auto
-      then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
-        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_elim1)
-    qed
-    fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
-      by (auto split: split_indicator)
-  qed auto
-qed
-
-lemma filterlim_at_top_imp_at_infinity:
-  fixes f :: "_ \<Rightarrow> real"
-  shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
-  by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
-
-lemma measurable_discrete_difference:
-  fixes f :: "'a \<Rightarrow> 'b::t1_space"
-  assumes f: "f \<in> measurable M N"
-  assumes X: "countable X"
-  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
-  assumes space: "\<And>x. x \<in> X \<Longrightarrow> g x \<in> space N"
-  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
-  shows "g \<in> measurable M N"
-  unfolding measurable_def
-proof safe
-  fix x assume "x \<in> space M" then show "g x \<in> space N"
-    using measurable_space[OF f, of x] eq[of x] space[of x] by (cases "x \<in> X") auto
-next
-  fix S assume S: "S \<in> sets N"
-  have "g -` S \<inter> space M = (f -` S \<inter> space M) - (\<Union>x\<in>X. {x}) \<union> (\<Union>x\<in>{x\<in>X. g x \<in> S}. {x})"
-    using sets.sets_into_space[OF sets] eq by auto
-  also have "\<dots> \<in> sets M"
-    by (safe intro!: sets.Diff sets.Un measurable_sets[OF f] S sets.countable_UN' X countable_Collect sets)
-  finally show "g -` S \<inter> space M \<in> sets M" .
-qed
-
-lemma AE_discrete_difference:
-  assumes X: "countable X"
-  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
-  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
-  shows "AE x in M. x \<notin> X"
-proof -
-  have X_sets: "(\<Union>x\<in>X. {x}) \<in> sets M"
-    using assms by (intro sets.countable_UN') auto
-  have "emeasure M (\<Union>x\<in>X. {x}) = (\<integral>\<^sup>+ i. emeasure M {i} \<partial>count_space X)"
-    by (rule emeasure_UN_countable) (auto simp: assms disjoint_family_on_def)
-  also have "\<dots> = (\<integral>\<^sup>+ i. 0 \<partial>count_space X)"
-    by (intro nn_integral_cong) (simp add: null)
-  finally show "AE x in M. x \<notin> X"
-    using AE_iff_measurable[of X M "\<lambda>x. x \<notin> X"] X_sets sets.sets_into_space[OF sets] by auto
-qed
-
-lemma integrable_discrete_difference:
-  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
-  assumes X: "countable X"
-  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
-  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
-  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
-  shows "integrable M f \<longleftrightarrow> integrable M g"
-  unfolding integrable_iff_bounded
-proof (rule conj_cong)
-  { assume "f \<in> borel_measurable M" then have "g \<in> borel_measurable M"
-      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
-  moreover
-  { assume "g \<in> borel_measurable M" then have "f \<in> borel_measurable M"
-      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
-  ultimately show "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" ..
-next
-  have "AE x in M. x \<notin> X"
-    by (rule AE_discrete_difference) fact+
-  then have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. norm (g x) \<partial>M)"
-    by (intro nn_integral_cong_AE) (auto simp: eq)
-  then show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity> \<longleftrightarrow> (\<integral>\<^sup>+ x. norm (g x) \<partial>M) < \<infinity>"
-    by simp
-qed
-
-lemma integral_discrete_difference:
-  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
-  assumes X: "countable X"
-  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
-  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
-  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
-  shows "integral\<^sup>L M f = integral\<^sup>L M g"
-proof (rule integral_eq_cases)
-  show eq: "integrable M f \<longleftrightarrow> integrable M g"
-    by (rule integrable_discrete_difference[where X=X]) fact+
-
-  assume f: "integrable M f"
-  show "integral\<^sup>L M f = integral\<^sup>L M g"
-  proof (rule integral_cong_AE)
-    show "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-      using f eq by (auto intro: borel_measurable_integrable)
-
-    have "AE x in M. x \<notin> X"
-      by (rule AE_discrete_difference) fact+
-    with AE_space show "AE x in M. f x = g x"
-      by eventually_elim fact
-  qed
-qed
-
-lemma has_bochner_integral_discrete_difference:
-  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
-  assumes X: "countable X"
-  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
-  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
-  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
-  shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
-  using integrable_discrete_difference[of X M f g, OF assms]
-  using integral_discrete_difference[of X M f g, OF assms]
-  by (metis has_bochner_integral_iff)
-
-lemma has_bochner_integral_even_function:
-  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
-  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
-  assumes even: "\<And>x. f (- x) = f x"
-  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
-proof -
-  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
-    by (auto split: split_indicator)
-  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
-    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
-       (auto simp: indicator even f)
-  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
-    by (rule has_bochner_integral_add)
-  then have "has_bochner_integral lborel f (x + x)"
-    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
-       (auto split: split_indicator)
-  then show ?thesis
-    by (simp add: scaleR_2)
-qed
-
-lemma has_bochner_integral_odd_function:
-  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
-  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
-  assumes odd: "\<And>x. f (- x) = - f x"
-  shows "has_bochner_integral lborel f 0"
-proof -
-  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
-    by (auto split: split_indicator)
-  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
-    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
-       (auto simp: indicator odd f)
-  from has_bochner_integral_minus[OF this]
-  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
-    by simp 
-  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
-    by (rule has_bochner_integral_add)
-  then have "has_bochner_integral lborel f (x + - x)"
-    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
-       (auto split: split_indicator)
-  then show ?thesis
-    by simp
-qed
-
-
-lemma filterlim_power2_at_top[intro]: "filterlim (\<lambda>(x::real). x\<^sup>2) at_top at_top"
-  by (auto intro!: filterlim_at_top_mult_at_top filterlim_ident simp: power2_eq_square)
-
-lemma distributed_integrable_var:
-  fixes X :: "'a \<Rightarrow> real"
-  shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X"
-  using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp
-
-lemma (in ordered_comm_monoid_add) setsum_pos: 
-  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
-  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
-
-lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
-  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult_commute)
-
-lemma distr_cong: "M = K \<Longrightarrow> sets N = sets L \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> distr M N f = distr K L g"
-  using sets_eq_imp_space_eq[of N L] by (simp add: distr_def Int_def cong: rev_conj_cong)
-
-lemma AE_borel_affine: 
-  fixes P :: "real \<Rightarrow> bool"
-  shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)"
-  by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
-     (simp_all add: AE_density AE_distr_iff field_simps)
-
-lemma density_distr:
-  assumes [measurable]: "f \<in> borel_measurable N" "X \<in> measurable M N"
-  shows "density (distr M N X) f = distr (density M (\<lambda>x. f (X x))) N X"
-  by (intro measure_eqI)
-     (auto simp add: emeasure_density nn_integral_distr emeasure_distr
-           split: split_indicator intro!: nn_integral_cong)
-
-lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
-  by (simp split: split_indicator)
-
 lemma (in prob_space) distributed_affine:
   fixes f :: "real \<Rightarrow> ereal"
   assumes f: "distributed M lborel X f"
@@ -1178,7 +926,8 @@
   proof (rule nn_integral_FTC_atLeast)
     have "((\<lambda>x::real. - exp (- x\<^sup>2) / 2) ---> - 0 / 2) at_top"
       by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot]
-                   filterlim_compose[OF filterlim_uminus_at_bot_at_top])
+                   filterlim_compose[OF filterlim_uminus_at_bot_at_top]
+                   filterlim_pow_at_top filterlim_ident)
          auto
     then show "((\<lambda>a::real. - exp (- a\<^sup>2) / 2) ---> 0) at_top"
       by simp
@@ -1211,14 +960,17 @@
         assume "even k"
         have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top"
           by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0]
-                   filterlim_at_top_imp_at_infinity filterlim_ident filterlim_power2_at_top)
+                   filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident)
+             auto
         also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)"
           using `even k` by (auto simp: even_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
         finally show ?thesis by simp
       next
         assume "odd k"
         have "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top"
-          by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity filterlim_ident filterlim_power2_at_top)
+          by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity
+                    filterlim_ident filterlim_pow_at_top)
+             auto
         also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)"
           using `odd k` by (auto simp: odd_Suc_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
         finally show ?thesis by simp

--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1274,18 +1274,53 @@
             =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" 
   using integral_by_parts[OF assms] by (simp add: mult_ac)
 
-lemma integral_tendsto_at_top:
-  fixes f :: "real \<Rightarrow> real"
-  assumes [simp, intro]: "\<And>x. isCont f x"
-  assumes [simp, arith]: "\<And>x. 0 \<le> f x"
-  assumes [simp]: "integrable lborel f"
-  assumes [measurable]: "f \<in> borel_measurable borel"
-  shows "((\<lambda>x. \<integral>xa. f xa * indicator {0..x} xa \<partial>lborel) ---> \<integral>xa. f xa * indicator {0..} xa \<partial>lborel) at_top"
-  apply (auto intro!: borel_integrable_atLeastAtMost monoI integral_mono tendsto_at_topI_sequentially  
-    split:split_indicator)
-  apply (rule integral_dominated_convergence[where w = " \<lambda>x. f x * indicator {0..} x"])
-  unfolding LIMSEQ_def  
-  apply (auto intro!: AE_I2 tendsto_mult integrable_mult_indicator split: split_indicator)
-  by (metis ge_natfloor_plus_one_imp_gt less_imp_le)
+lemma AE_borel_affine: 
+  fixes P :: "real \<Rightarrow> bool"
+  shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)"
+  by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
+     (simp_all add: AE_density AE_distr_iff field_simps)
+
+lemma has_bochner_integral_even_function:
+  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
+  assumes even: "\<And>x. f (- x) = f x"
+  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
+proof -
+  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
+    by (auto split: split_indicator)
+  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
+    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
+       (auto simp: indicator even f)
+  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
+    by (rule has_bochner_integral_add)
+  then have "has_bochner_integral lborel f (x + x)"
+    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
+       (auto split: split_indicator)
+  then show ?thesis
+    by (simp add: scaleR_2)
+qed
+
+lemma has_bochner_integral_odd_function:
+  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
+  assumes odd: "\<And>x. f (- x) = - f x"
+  shows "has_bochner_integral lborel f 0"
+proof -
+  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
+    by (auto split: split_indicator)
+  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
+    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
+       (auto simp: indicator odd f)
+  from has_bochner_integral_minus[OF this]
+  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
+    by simp 
+  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
+    by (rule has_bochner_integral_add)
+  then have "has_bochner_integral lborel f (x + - x)"
+    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
+       (auto split: split_indicator)
+  then show ?thesis
+    by simp
+qed
 
 end

--- a/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -23,6 +23,9 @@
 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
 
@@ -793,26 +796,42 @@
     by (auto intro!: antisym)
 qed
 
-lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
+lemma UN_from_nat_into: 
+  assumes I: "countable I" "I \<noteq> {}"
+  shows "(\<Union>i\<in>I. N i) = (\<Union>i. N (from_nat_into I i))"
 proof -
-  have "\<Union>range N = \<Union>(N ` range from_nat)" by simp
-  then have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
+  have "(\<Union>i\<in>I. N i) = \<Union>(N ` range (from_nat_into I))"
+    using I by simp
+  also have "\<dots> = (\<Union>i. (N \<circ> from_nat_into I) i)"
     by (simp only: SUP_def image_comp)
-  then show ?thesis by simp
+  finally show ?thesis by simp
+qed
+
+lemma null_sets_UN':
+  assumes "countable I"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> N i \<in> null_sets M"
+  shows "(\<Union>i\<in>I. N i) \<in> null_sets M"
+proof cases
+  assume "I = {}" then show ?thesis by simp
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof (intro conjI CollectI null_setsI)
+    show "(\<Union>i\<in>I. N i) \<in> sets M"
+      using assms by (intro sets.countable_UN') auto
+    have "emeasure M (\<Union>i\<in>I. N i) \<le> (\<Sum>n. emeasure M (N (from_nat_into I n)))"
+      unfolding UN_from_nat_into[OF `countable I` `I \<noteq> {}`]
+      using assms `I \<noteq> {}` by (intro emeasure_subadditive_countably) (auto intro: from_nat_into)
+    also have "(\<lambda>n. emeasure M (N (from_nat_into I n))) = (\<lambda>_. 0)"
+      using assms `I \<noteq> {}` by (auto intro: from_nat_into)
+    finally show "emeasure M (\<Union>i\<in>I. N i) = 0"
+      by (intro antisym emeasure_nonneg) simp
+  qed
 qed
 
 lemma null_sets_UN[intro]:
-  assumes "\<And>i::'i::countable. N i \<in> null_sets M"
-  shows "(\<Union>i. N i) \<in> null_sets M"
-proof (intro conjI CollectI null_setsI)
-  show "(\<Union>i. N i) \<in> sets M" using assms by auto
-  have "0 \<le> emeasure M (\<Union>i. N i)" by (rule emeasure_nonneg)
-  moreover have "emeasure M (\<Union>i. N i) \<le> (\<Sum>n. emeasure M (N (Countable.from_nat n)))"
-    unfolding UN_from_nat[of N]
-    using assms by (intro emeasure_subadditive_countably) auto
-  ultimately show "emeasure M (\<Union>i. N i) = 0"
-    using assms by (auto simp: null_setsD1)
-qed
+  "(\<And>i::'i::countable. N i \<in> null_sets M) \<Longrightarrow> (\<Union>i. N i) \<in> null_sets M"
+  by (rule null_sets_UN') auto
 
 lemma null_set_Int1:
   assumes "B \<in> null_sets M" "A \<in> sets M" shows "A \<inter> B \<in> null_sets M"
@@ -1021,6 +1040,18 @@
     unfolding eventually_ae_filter by auto
 qed auto
 
+lemma AE_discrete_difference:
+  assumes X: "countable X"
+  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
+  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  shows "AE x in M. x \<notin> X"
+proof -
+  have "(\<Union>x\<in>X. {x}) \<in> null_sets M"
+    using assms by (intro null_sets_UN') auto
+  from AE_not_in[OF this] show "AE x in M. x \<notin> X"
+    by auto
+qed
+
 lemma AE_finite_all:
   assumes f: "finite S" shows "(AE x in M. \<forall>i\<in>S. P i x) \<longleftrightarrow> (\<forall>i\<in>S. AE x in M. P i x)"
   using f by induct auto

--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1990,6 +1990,13 @@
      (auto intro!: nn_integral_cong_AE
            simp: measurable_If max_def ereal_zero_le_0_iff nn_integral_density')
 
+lemma density_distr:
+  assumes [measurable]: "f \<in> borel_measurable N" "X \<in> measurable M N"
+  shows "density (distr M N X) f = distr (density M (\<lambda>x. f (X x))) N X"
+  by (intro measure_eqI)
+     (auto simp add: emeasure_density nn_integral_distr emeasure_distr
+           split: split_indicator intro!: nn_integral_cong)
+
 lemma emeasure_restricted:
   assumes S: "S \<in> sets M" and X: "X \<in> sets M"
   shows "emeasure (density M (indicator S)) X = emeasure M (S \<inter> X)"

--- a/src/HOL/Probability/Probability_Measure.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -745,6 +745,11 @@
   finally show ?thesis .
 qed
 
+lemma distributed_integrable_var:
+  fixes X :: "'a \<Rightarrow> real"
+  shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X"
+  using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp
+
 lemma (in prob_space) distributed_variance:
   fixes f::"real \<Rightarrow> real"
   assumes D: "distributed M lborel X f"

--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -364,6 +364,17 @@
   finally show ?thesis .
 qed
 
+
+lemma (in sigma_algebra) countable:
+  assumes "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> M" "countable A"
+  shows "A \<in> M"
+proof -
+  have "(\<Union>a\<in>A. {a}) \<in> M"
+    using assms by (intro countable_UN') auto
+  also have "(\<Union>a\<in>A. {a}) = A" by auto
+  finally show ?thesis by auto
+qed
+
 lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)"
   by (auto simp: ring_of_sets_iff)
 
@@ -2028,6 +2039,26 @@
     done
 qed
 
+lemma measurable_discrete_difference:
+  assumes f: "f \<in> measurable M N"
+  assumes X: "countable X"
+  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  assumes space: "\<And>x. x \<in> X \<Longrightarrow> g x \<in> space N"
+  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
+  shows "g \<in> measurable M N"
+  unfolding measurable_def
+proof safe
+  fix x assume "x \<in> space M" then show "g x \<in> space N"
+    using measurable_space[OF f, of x] eq[of x] space[of x] by (cases "x \<in> X") auto
+next
+  fix S assume S: "S \<in> sets N"
+  have "g -` S \<inter> space M = (f -` S \<inter> space M) - (\<Union>x\<in>X. {x}) \<union> (\<Union>x\<in>{x\<in>X. g x \<in> S}. {x})"
+    using sets.sets_into_space[OF sets] eq by auto
+  also have "\<dots> \<in> sets M"
+    by (safe intro!: sets.Diff sets.Un measurable_sets[OF f] S sets.countable_UN' X countable_Collect sets)
+  finally show "g -` S \<inter> space M \<in> sets M" .
+qed
+
 lemma measurable_mono1:
   "M' \<subseteq> Pow \<Omega> \<Longrightarrow> M \<subseteq> M' \<Longrightarrow>
     measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"

--- a/src/HOL/Rat.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Rat.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -916,6 +916,8 @@
   "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   by (rule Rats_cases) auto
 
+lemma Rats_infinite: "\<not> finite \<rat>"
+  by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def)
 
 subsection {* Implementation of rational numbers as pairs of integers *}
 

--- a/src/HOL/Real.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Real.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1319,7 +1319,6 @@
 lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
 by (simp add: real_eq_of_nat)
 
-
 lemma Rats_eq_int_div_int:
   "\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
 proof
@@ -1996,6 +1995,9 @@
   unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
   by simp
 
+lemma Rats_unbounded: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
+  by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
+
 subsection {* Exponentiation with floor *}
 
 lemma floor_power:

--- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -856,15 +856,64 @@
 lemma setprod_norm:
   fixes f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
   shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
-proof (cases "finite A")
-  case True then show ?thesis 
-    by (induct A rule: finite_induct) (auto simp: norm_mult)
-next
-  case False then show ?thesis
-    by (metis norm_one setprod.infinite) 
+  by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
+
+lemma norm_setprod_le: 
+  "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1, comm_monoid_mult}))"
+proof (induction A rule: infinite_finite_induct)
+  case (insert a A)
+  then have "norm (setprod f (insert a A)) \<le> norm (f a) * norm (setprod f A)"
+    by (simp add: norm_mult_ineq)
+  also have "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a))"
+    by (rule insert)
+  finally show ?case
+    by (simp add: insert mult_left_mono)
+qed simp_all
+
+lemma norm_setprod_diff:
+  fixes z w :: "'i \<Rightarrow> 'a::{real_normed_algebra_1, comm_monoid_mult}"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> norm (z i) \<le> 1) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> norm (w i) \<le> 1) \<Longrightarrow>
+    norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))" 
+proof (induction I rule: infinite_finite_induct)
+  case (insert i I)
+  note insert.hyps[simp]
+
+  have "norm ((\<Prod>i\<in>insert i I. z i) - (\<Prod>i\<in>insert i I. w i)) =
+    norm ((\<Prod>i\<in>I. z i) * (z i - w i) + ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * w i)"
+    (is "_ = norm (?t1 + ?t2)")
+    by (auto simp add: field_simps)
+  also have "... \<le> norm ?t1 + norm ?t2"
+    by (rule norm_triangle_ineq)
+  also have "norm ?t1 \<le> norm (\<Prod>i\<in>I. z i) * norm (z i - w i)"
+    by (rule norm_mult_ineq)
+  also have "\<dots> \<le> (\<Prod>i\<in>I. norm (z i)) * norm(z i - w i)"
+    by (rule mult_right_mono) (auto intro: norm_setprod_le)
+  also have "(\<Prod>i\<in>I. norm (z i)) \<le> (\<Prod>i\<in>I. 1)"
+    by (intro setprod_mono) (auto intro!: insert)
+  also have "norm ?t2 \<le> norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * norm (w i)"
+    by (rule norm_mult_ineq)
+  also have "norm (w i) \<le> 1"
+    by (auto intro: insert)
+  also have "norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
+    using insert by auto
+  finally show ?case
+    by (auto simp add: add_ac mult_right_mono mult_left_mono)
+qed simp_all
+
+lemma norm_power_diff: 
+  fixes z w :: "'a::{real_normed_algebra_1, comm_monoid_mult}"
+  assumes "norm z \<le> 1" "norm w \<le> 1"
+  shows "norm (z^m - w^m) \<le> m * norm (z - w)"
+proof -
+  have "norm (z^m - w^m) = norm ((\<Prod> i < m. z) - (\<Prod> i < m. w))"
+    by (simp add: setprod_constant)
+  also have "\<dots> \<le> (\<Sum>i<m. norm (z - w))"
+    by (intro norm_setprod_diff) (auto simp add: assms)
+  also have "\<dots> = m * norm (z - w)"
+    by (simp add: real_of_nat_def)
+  finally show ?thesis .
 qed
 
-
 subsection {* Metric spaces *}
 
 class metric_space = open_dist +
@@ -1734,6 +1783,55 @@
 instance real :: banach by default
 
 lemma tendsto_at_topI_sequentially:
+  fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
+  assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) ----> y"
+  shows "(f ---> y) at_top"
+  unfolding filterlim_iff
+proof safe
+  fix P assume "eventually P (nhds y)"
+  then have seq: "\<And>f. f ----> y \<Longrightarrow> eventually (\<lambda>x. P (f x)) at_top"
+    unfolding eventually_nhds_iff_sequentially by simp
+
+  show "eventually (\<lambda>x. P (f x)) at_top"
+  proof (rule ccontr)
+    assume "\<not> eventually (\<lambda>x. P (f x)) at_top"
+    then have "\<And>X. \<exists>x>X. \<not> P (f x)"
+      unfolding eventually_at_top_dense by simp
+    then obtain r where not_P: "\<And>x. \<not> P (f (r x))" and r: "\<And>x. x < r x"
+      by metis
+    
+    def s \<equiv> "rec_nat (r 0) (\<lambda>_ x. r (x + 1))"
+    then have [simp]: "s 0 = r 0" "\<And>n. s (Suc n) = r (s n + 1)"
+      by auto
+
+    { fix n have "n < s n" using r
+        by (induct n) (auto simp add: real_of_nat_Suc intro: less_trans add_strict_right_mono) }
+    note s_subseq = this
+
+    have "mono s"
+    proof (rule incseq_SucI)
+      fix n show "s n \<le> s (Suc n)"
+        using r[of "s n + 1"] by simp
+    qed
+
+    have "filterlim s at_top sequentially"
+      unfolding filterlim_at_top_gt[where c=0] eventually_sequentially
+    proof (safe intro!: exI)
+      fix Z :: real and n assume "0 < Z" "natceiling Z \<le> n"
+      with real_natceiling_ge[of Z] `n < s n`
+      show "Z \<le> s n"
+        by auto
+    qed
+    moreover then have "eventually (\<lambda>x. P (f (s x))) sequentially"
+      by (rule seq[OF *])
+    then obtain n where "P (f (s n))"
+      by (auto simp: eventually_sequentially)
+    then show False
+      using not_P by (cases n) auto
+  qed
+qed
+
+lemma tendsto_at_topI_sequentially_real:
   fixes f :: "real \<Rightarrow> real"
   assumes mono: "mono f"
   assumes limseq: "(\<lambda>n. f (real n)) ----> y"

--- a/src/HOL/Series.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Series.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -344,6 +344,14 @@
 lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
 lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
 
+lemmas sums_scaleR_left = bounded_linear.sums[OF bounded_linear_scaleR_left]
+lemmas summable_scaleR_left = bounded_linear.summable[OF bounded_linear_scaleR_left]
+lemmas suminf_scaleR_left = bounded_linear.suminf[OF bounded_linear_scaleR_left]
+
+lemmas sums_scaleR_right = bounded_linear.sums[OF bounded_linear_scaleR_right]
+lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
+lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
+
 subsection {* Infinite summability on real normed algebras *}
 
 context

--- a/src/HOL/Topological_Spaces.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -789,13 +789,13 @@
   by (simp add: at_eq_bot_iff not_open_singleton)
 
 lemma eventually_at_right:
-  fixes x :: "'a :: {no_top, linorder_topology}"
+  fixes x :: "'a :: linorder_topology"
+  assumes gt_ex: "x < y"
   shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
   unfolding eventually_at_topological
 proof safe
-  obtain y where "x < y" using gt_ex[of x] ..
+  note gt_ex
   moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
-  moreover note gt_ex[of x]
   moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
   ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
     by (auto simp: subset_eq Ball_def)
@@ -806,11 +806,12 @@
 qed
 
 lemma eventually_at_left:
-  fixes x :: "'a :: {no_bot, linorder_topology}"
+  fixes x :: "'a :: linorder_topology"
+  assumes lt_ex: "y < x"
   shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
   unfolding eventually_at_topological
 proof safe
-  obtain y where "y < x" using lt_ex[of x] ..
+  note lt_ex
   moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
   moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
   ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
@@ -821,13 +822,21 @@
     by (intro exI[of _ "{b <..}"]) auto
 qed
 
+lemma trivial_limit_at_right_top: "at_right (top::_::{order_top, linorder_topology}) = bot"
+  unfolding filter_eq_iff eventually_at_topological by auto
+
+lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot, linorder_topology}) = bot"
+  unfolding filter_eq_iff eventually_at_topological by auto
+
 lemma trivial_limit_at_left_real [simp]:
-  "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"
-  unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
+  "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_order, linorder_topology}))"
+  using lt_ex[of x]
+  by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense)
 
 lemma trivial_limit_at_right_real [simp]:
-  "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"
-  unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
+  "\<not> trivial_limit (at_right (x::'a::{no_top, dense_order, linorder_topology}))"
+  using gt_ex[of x]
+  by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
 
 lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
   by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
@@ -867,6 +876,15 @@
   "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
   by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
 
+lemma filterlim_mono_eventually:
+  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
+  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
+  shows "filterlim f' F' G'"
+  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
+  apply (rule filterlim_mono[OF _ ord])
+  apply fact
+  done
+
 lemma filterlim_principal:
   "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   unfolding filterlim_def eventually_filtermap le_principal ..
@@ -1179,7 +1197,7 @@
   by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
 
 lemma filterlim_at_bot_at_right:
-  fixes f :: "'a::{no_top, linorder_topology} \<Rightarrow> 'b::linorder"
+  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b"
@@ -1194,14 +1212,14 @@
     with x have "P z" by auto
     have "eventually (\<lambda>x. x \<le> g z) (at_right a)"
       using bound[OF bij(2)[OF `P z`]]
-      unfolding eventually_at_right by (auto intro!: exI[of _ "g z"])
+      unfolding eventually_at_right[OF bound[OF bij(2)[OF `P z`]]] by (auto intro!: exI[of _ "g z"])
     with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)"
       by eventually_elim (metis bij `P z` mono)
   qed
 qed
 
 lemma filterlim_at_top_at_left:
-  fixes f :: "'a::{no_bot, linorder_topology} \<Rightarrow> 'b::linorder"
+  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a"
@@ -1216,7 +1234,7 @@
     with x have "P z" by auto
     have "eventually (\<lambda>x. g z \<le> x) (at_left a)"
       using bound[OF bij(2)[OF `P z`]]
-      unfolding eventually_at_left by (auto intro!: exI[of _ "g z"])
+      unfolding eventually_at_left[OF bound[OF bij(2)[OF `P z`]]] by (auto intro!: exI[of _ "g z"])
     with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)"
       by eventually_elim (metis bij `P z` mono)
   qed

--- a/src/HOL/Transcendental.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Transcendental.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1303,29 +1303,42 @@
 lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
   by simp
 
-lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
-  apply (subgoal_tac "isCont ln (exp (ln x))", simp)
-  apply (rule isCont_inverse_function [where f=exp], simp_all)
-  done
+lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
+  by (auto simp add: ln_def intro!: arg_cong[where f=The])
+
+lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
+proof cases
+  assume "0 < x"
+  moreover then have "isCont ln (exp (ln x))"
+    by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
+  ultimately show ?thesis
+    by simp
+next
+  assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
+    unfolding isCont_def
+    by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
+       (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
+                intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
+qed
 
 lemma tendsto_ln [tendsto_intros]:
-  "(f ---> a) F \<Longrightarrow> 0 < a \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
+  "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
   by (rule isCont_tendsto_compose [OF isCont_ln])
 
 lemma continuous_ln:
-  "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
+  "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
   unfolding continuous_def by (rule tendsto_ln)
 
 lemma isCont_ln' [continuous_intros]:
-  "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
+  "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
   unfolding continuous_at by (rule tendsto_ln)
 
 lemma continuous_within_ln [continuous_intros]:
-  "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
+  "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
   unfolding continuous_within by (rule tendsto_ln)
 
 lemma continuous_on_ln [continuous_intros]:
-  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
+  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
   unfolding continuous_on_def by (auto intro: tendsto_ln)
 
 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
@@ -1992,6 +2005,9 @@
 lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
 by(simp add: root_powr_inverse ln_powr)
 
+lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
+  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult_commute)
+
 lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
 by(simp add: log_def ln_root)
 
@@ -2085,30 +2101,30 @@
 qed
 
 lemma tendsto_powr [tendsto_intros]:
-  "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
+  "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
   unfolding powr_def by (intro tendsto_intros)
 
 lemma continuous_powr:
   assumes "continuous F f"
     and "continuous F g"
-    and "0 < f (Lim F (\<lambda>x. x))"
+    and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
   shows "continuous F (\<lambda>x. (f x) powr (g x))"
   using assms unfolding continuous_def by (rule tendsto_powr)
 
 lemma continuous_at_within_powr[continuous_intros]:
   assumes "continuous (at a within s) f"
     and "continuous (at a within s) g"
-    and "0 < f a"
+    and "f a \<noteq> 0"
   shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
   using assms unfolding continuous_within by (rule tendsto_powr)
 
 lemma isCont_powr[continuous_intros, simp]:
-  assumes "isCont f a" "isCont g a" "0 < f a"
+  assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
   shows "isCont (\<lambda>x. (f x) powr g x) a"
   using assms unfolding continuous_at by (rule tendsto_powr)
 
 lemma continuous_on_powr[continuous_intros]:
-  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
+  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
 
@@ -2150,6 +2166,53 @@
   show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
 qed
 
+(* it is funny that this isn't in the library! It could go in Transcendental *)
+lemma tendsto_exp_limit_at_right:
+  fixes x :: real
+  shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
+proof cases
+  assume "x \<noteq> 0"
+
+  have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
+    by (auto intro!: derivative_eq_intros)
+  then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
+    by (auto simp add: has_field_derivative_def field_has_derivative_at) 
+  then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
+    by (rule tendsto_intros)
+  then show ?thesis
+  proof (rule filterlim_mono_eventually)
+    show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
+      unfolding eventually_at_right[OF zero_less_one]
+      using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
+  qed (simp_all add: at_eq_sup_left_right)
+qed (simp add: tendsto_const)
+
+lemma tendsto_exp_limit_at_top:
+  fixes x :: real
+  shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
+  apply (subst filterlim_at_top_to_right)
+  apply (simp add: inverse_eq_divide)
+  apply (rule tendsto_exp_limit_at_right)
+  done
+
+lemma tendsto_exp_limit_sequentially:
+  fixes x :: real
+  shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
+proof (rule filterlim_mono_eventually)
+  from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
+  hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
+    apply (intro eventually_sequentiallyI [of n])
+    apply (case_tac "x \<ge> 0")
+    apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
+    apply (subgoal_tac "x / real xa > -1")
+    apply (auto simp add: field_simps)
+    done
+  then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
+    by (rule eventually_elim1) (erule powr_realpow)
+  show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
+    by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
+qed auto
+
 subsection {* Sine and Cosine *}
 
 definition sin_coeff :: "nat \<Rightarrow> real" where
@@ -2374,6 +2437,31 @@
   using cos_add [where x=x and y=x]
   by (simp add: power2_eq_square)
 
+lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
+proof -
+  let ?f = "\<lambda>x. x - sin x"
+  from x have "?f x \<ge> ?f 0"
+    apply (rule DERIV_nonneg_imp_nondecreasing)
+    apply (intro allI impI exI[of _ "1 - cos x" for x])
+    apply (auto intro!: derivative_eq_intros simp: field_simps)
+    done
+  thus "sin x \<le> x" by simp
+qed
+
+lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
+proof -
+  let ?f = "\<lambda>x. x + sin x"
+  from x have "?f x \<ge> ?f 0"
+    apply (rule DERIV_nonneg_imp_nondecreasing)
+    apply (intro allI impI exI[of _ "1 + cos x" for x])
+    apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
+    done
+  thus "sin x \<ge> -x" by simp
+qed
+
+lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
+  using sin_x_ge_neg_x [of x] sin_x_le_x [of x] sin_x_ge_neg_x [of "-x"] sin_x_le_x [of "-x"]
+  by (auto simp: abs_real_def)
 
 subsection {* The Constant Pi *}