moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
authorhoelzl
Wed Jun 18 07:31:12 2014 +0200 (2014-06-18)
changeset 572750ddb5b755cdc
parent 57274 0acfdb151e52
child 57276 49c51eeaa623
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Groups_Big.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NthRoot.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Jun 18 15:23:40 2014 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Jun 18 07:31:12 2014 +0200
     1.3 @@ -559,4 +559,62 @@
     1.4  qed
     1.5  end
     1.6  
     1.7 +lemma interval_cases:
     1.8 +  fixes S :: "'a :: conditionally_complete_linorder set"
     1.9 +  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"
    1.10 +  shows "\<exists>a b. S = {} \<or>
    1.11 +    S = UNIV \<or>
    1.12 +    S = {..<b} \<or>
    1.13 +    S = {..b} \<or>
    1.14 +    S = {a<..} \<or>
    1.15 +    S = {a..} \<or>
    1.16 +    S = {a<..<b} \<or>
    1.17 +    S = {a<..b} \<or>
    1.18 +    S = {a..<b} \<or>
    1.19 +    S = {a..b}"
    1.20 +proof -
    1.21 +  def lower \<equiv> "{x. \<exists>s\<in>S. s \<le> x}" and upper \<equiv> "{x. \<exists>s\<in>S. x \<le> s}"
    1.22 +  with ivl have "S = lower \<inter> upper"
    1.23 +    by auto
    1.24 +  moreover 
    1.25 +  have "\<exists>a. upper = UNIV \<or> upper = {} \<or> upper = {.. a} \<or> upper = {..< a}"
    1.26 +  proof cases
    1.27 +    assume *: "bdd_above S \<and> S \<noteq> {}"
    1.28 +    from * have "upper \<subseteq> {.. Sup S}"
    1.29 +      by (auto simp: upper_def intro: cSup_upper2)
    1.30 +    moreover from * have "{..< Sup S} \<subseteq> upper"
    1.31 +      by (force simp add: less_cSup_iff upper_def subset_eq Ball_def)
    1.32 +    ultimately have "upper = {.. Sup S} \<or> upper = {..< Sup S}"
    1.33 +      unfolding ivl_disj_un(2)[symmetric] by auto
    1.34 +    then show ?thesis by auto
    1.35 +  next
    1.36 +    assume "\<not> (bdd_above S \<and> S \<noteq> {})"
    1.37 +    then have "upper = UNIV \<or> upper = {}"
    1.38 +      by (auto simp: upper_def bdd_above_def not_le dest: less_imp_le)
    1.39 +    then show ?thesis
    1.40 +      by auto
    1.41 +  qed
    1.42 +  moreover
    1.43 +  have "\<exists>b. lower = UNIV \<or> lower = {} \<or> lower = {b ..} \<or> lower = {b <..}"
    1.44 +  proof cases
    1.45 +    assume *: "bdd_below S \<and> S \<noteq> {}"
    1.46 +    from * have "lower \<subseteq> {Inf S ..}"
    1.47 +      by (auto simp: lower_def intro: cInf_lower2)
    1.48 +    moreover from * have "{Inf S <..} \<subseteq> lower"
    1.49 +      by (force simp add: cInf_less_iff lower_def subset_eq Ball_def)
    1.50 +    ultimately have "lower = {Inf S ..} \<or> lower = {Inf S <..}"
    1.51 +      unfolding ivl_disj_un(1)[symmetric] by auto
    1.52 +    then show ?thesis by auto
    1.53 +  next
    1.54 +    assume "\<not> (bdd_below S \<and> S \<noteq> {})"
    1.55 +    then have "lower = UNIV \<or> lower = {}"
    1.56 +      by (auto simp: lower_def bdd_below_def not_le dest: less_imp_le)
    1.57 +    then show ?thesis
    1.58 +      by auto
    1.59 +  qed
    1.60 +  ultimately show ?thesis
    1.61 +    unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def
    1.62 +    by (elim exE disjE) auto
    1.63 +qed
    1.64 +
    1.65  end
     2.1 --- a/src/HOL/Groups_Big.thy	Wed Jun 18 15:23:40 2014 +0200
     2.2 +++ b/src/HOL/Groups_Big.thy	Wed Jun 18 07:31:12 2014 +0200
     2.3 @@ -1317,4 +1317,8 @@
     2.4    "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
     2.5  using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
     2.6  
     2.7 +lemma (in ordered_comm_monoid_add) setsum_pos: 
     2.8 +  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
     2.9 +  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
    2.10 +
    2.11  end
     3.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jun 18 15:23:40 2014 +0200
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jun 18 07:31:12 2014 +0200
     3.3 @@ -98,6 +98,18 @@
     3.4  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))"
     3.5  by (fast elim: someI)
     3.6  
     3.7 +lemma dependent_nat_choice:
     3.8 +  assumes  1: "\<exists>x. P x" and 
     3.9 +           2: "\<And>x n. P x \<Longrightarrow> \<exists>y. P y \<and> Q n x y"
    3.10 +  shows "\<exists>f. \<forall>n. P (f n) \<and> Q n (f n) (f (Suc n))"
    3.11 +proof (intro exI allI conjI)
    3.12 +  fix n def f \<equiv> "rec_nat (SOME x. P x) (\<lambda>n x. SOME y. P y \<and> Q n x y)"
    3.13 +  then have "P (f 0)" "\<And>n. P (f n) \<Longrightarrow> P (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
    3.14 +    using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def)
    3.15 +  then show "P (f n)" "Q n (f n) (f (Suc n))"
    3.16 +    by (induct n) auto
    3.17 +qed
    3.18 +
    3.19  subsection {*Function Inverse*}
    3.20  
    3.21  lemma inv_def: "inv f = (%y. SOME x. f x = y)"
     4.1 --- a/src/HOL/Limits.thy	Wed Jun 18 15:23:40 2014 +0200
     4.2 +++ b/src/HOL/Limits.thy	Wed Jun 18 07:31:12 2014 +0200
     4.3 @@ -54,6 +54,11 @@
     4.4    "at_bot \<le> (at_infinity :: real filter)"
     4.5    unfolding at_infinity_eq_at_top_bot by simp
     4.6  
     4.7 +lemma filterlim_at_top_imp_at_infinity:
     4.8 +  fixes f :: "_ \<Rightarrow> real"
     4.9 +  shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
    4.10 +  by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
    4.11 +
    4.12  subsubsection {* Boundedness *}
    4.13  
    4.14  definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
     5.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 15:23:40 2014 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 07:31:12 2014 +0200
     5.3 @@ -1855,7 +1855,7 @@
     5.4      from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \<in> I" "f y < a"
     5.5        by auto
     5.6      then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
     5.7 -      unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
     5.8 +      unfolding eventually_at_right[OF `x < y`] by (metis less_imp_le le_less_trans mono)
     5.9      then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
    5.10        unfolding eventually_at_filter by eventually_elim simp
    5.11    qed
     6.1 --- a/src/HOL/NthRoot.thy	Wed Jun 18 15:23:40 2014 +0200
     6.2 +++ b/src/HOL/NthRoot.thy	Wed Jun 18 07:31:12 2014 +0200
     6.3 @@ -538,6 +538,10 @@
     6.4    shows "4 * x\<^sup>2 = (2 * x)\<^sup>2"
     6.5  by (simp add: power2_eq_square)
     6.6  
     6.7 +lemma sqrt_at_top: "LIM x at_top. sqrt x :: real :> at_top"
     6.8 +  by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="power2"])
     6.9 +     (auto intro: eventually_gt_at_top)
    6.10 +
    6.11  subsection {* Square Root of Sum of Squares *}
    6.12  
    6.13  lemma sum_squares_bound: 
     7.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Wed Jun 18 15:23:40 2014 +0200
     7.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Wed Jun 18 07:31:12 2014 +0200
     7.3 @@ -1235,6 +1235,30 @@
     7.4    qed fact
     7.5  qed
     7.6  
     7.7 +lemma integrableI_bounded_set:
     7.8 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
     7.9 +  assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M"
    7.10 +  assumes finite: "emeasure M A < \<infinity>"
    7.11 +    and bnd: "AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B"
    7.12 +    and null: "AE x in M. x \<notin> A \<longrightarrow> f x = 0"
    7.13 +  shows "integrable M f"
    7.14 +proof (rule integrableI_bounded)
    7.15 +  { fix x :: 'b have "norm x \<le> B \<Longrightarrow> 0 \<le> B"
    7.16 +      using norm_ge_zero[of x] by arith }
    7.17 +  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)"
    7.18 +    by (intro nn_integral_mono_AE) (auto split: split_indicator split_max)
    7.19 +  also have "\<dots> < \<infinity>"
    7.20 +    using finite by (subst nn_integral_cmult_indicator) (auto simp: max_def)
    7.21 +  finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
    7.22 +qed simp
    7.23 +
    7.24 +lemma integrableI_bounded_set_indicator:
    7.25 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    7.26 +  shows "A \<in> sets M \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow>
    7.27 +    emeasure M A < \<infinity> \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B) \<Longrightarrow>
    7.28 +    integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
    7.29 +  by (rule integrableI_bounded_set[where A=A]) auto
    7.30 +
    7.31  lemma integrableI_nonneg:
    7.32    fixes f :: "'a \<Rightarrow> real"
    7.33    assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
    7.34 @@ -1267,6 +1291,11 @@
    7.35    finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" .
    7.36  qed 
    7.37  
    7.38 +lemma integrable_mult_indicator:
    7.39 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    7.40 +  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
    7.41 +  by (rule integrable_bound[of M f]) (auto split: split_indicator)
    7.42 +
    7.43  lemma integrable_abs[simp, intro]:
    7.44    fixes f :: "'a \<Rightarrow> real"
    7.45    assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
    7.46 @@ -1282,11 +1311,21 @@
    7.47    assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f"
    7.48    using assms by (rule integrable_bound) auto
    7.49  
    7.50 +lemma integrable_norm_iff:
    7.51 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    7.52 +  shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. norm (f x)) \<longleftrightarrow> integrable M f"
    7.53 +  by (auto intro: integrable_norm_cancel)
    7.54 +
    7.55  lemma integrable_abs_cancel:
    7.56    fixes f :: "'a \<Rightarrow> real"
    7.57    assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f"
    7.58    using assms by (rule integrable_bound) auto
    7.59  
    7.60 +lemma integrable_abs_iff:
    7.61 +  fixes f :: "'a \<Rightarrow> real"
    7.62 +  shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
    7.63 +  by (auto intro: integrable_abs_cancel)
    7.64 +
    7.65  lemma integrable_max[simp, intro]:
    7.66    fixes f :: "'a \<Rightarrow> real"
    7.67    assumes fg[measurable]: "integrable M f" "integrable M g"
    7.68 @@ -1330,6 +1369,65 @@
    7.69    finally show ?thesis .
    7.70  qed
    7.71  
    7.72 +lemma integrable_discrete_difference:
    7.73 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    7.74 +  assumes X: "countable X"
    7.75 +  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
    7.76 +  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
    7.77 +  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
    7.78 +  shows "integrable M f \<longleftrightarrow> integrable M g"
    7.79 +  unfolding integrable_iff_bounded
    7.80 +proof (rule conj_cong)
    7.81 +  { assume "f \<in> borel_measurable M" then have "g \<in> borel_measurable M"
    7.82 +      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
    7.83 +  moreover
    7.84 +  { assume "g \<in> borel_measurable M" then have "f \<in> borel_measurable M"
    7.85 +      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
    7.86 +  ultimately show "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" ..
    7.87 +next
    7.88 +  have "AE x in M. x \<notin> X"
    7.89 +    by (rule AE_discrete_difference) fact+
    7.90 +  then have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. norm (g x) \<partial>M)"
    7.91 +    by (intro nn_integral_cong_AE) (auto simp: eq)
    7.92 +  then show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity> \<longleftrightarrow> (\<integral>\<^sup>+ x. norm (g x) \<partial>M) < \<infinity>"
    7.93 +    by simp
    7.94 +qed
    7.95 +
    7.96 +lemma integral_discrete_difference:
    7.97 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    7.98 +  assumes X: "countable X"
    7.99 +  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
   7.100 +  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   7.101 +  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   7.102 +  shows "integral\<^sup>L M f = integral\<^sup>L M g"
   7.103 +proof (rule integral_eq_cases)
   7.104 +  show eq: "integrable M f \<longleftrightarrow> integrable M g"
   7.105 +    by (rule integrable_discrete_difference[where X=X]) fact+
   7.106 +
   7.107 +  assume f: "integrable M f"
   7.108 +  show "integral\<^sup>L M f = integral\<^sup>L M g"
   7.109 +  proof (rule integral_cong_AE)
   7.110 +    show "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   7.111 +      using f eq by (auto intro: borel_measurable_integrable)
   7.112 +
   7.113 +    have "AE x in M. x \<notin> X"
   7.114 +      by (rule AE_discrete_difference) fact+
   7.115 +    with AE_space show "AE x in M. f x = g x"
   7.116 +      by eventually_elim fact
   7.117 +  qed
   7.118 +qed
   7.119 +
   7.120 +lemma has_bochner_integral_discrete_difference:
   7.121 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   7.122 +  assumes X: "countable X"
   7.123 +  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
   7.124 +  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   7.125 +  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   7.126 +  shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
   7.127 +  using integrable_discrete_difference[of X M f g, OF assms]
   7.128 +  using integral_discrete_difference[of X M f g, OF assms]
   7.129 +  by (metis has_bochner_integral_iff)
   7.130 +
   7.131  lemma
   7.132    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
   7.133    assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
   7.134 @@ -2188,54 +2286,28 @@
   7.135    shows "integral\<^sup>L M X < integral\<^sup>L M Y"
   7.136    using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
   7.137  
   7.138 -lemma integrable_mult_indicator:
   7.139 -  fixes f :: "'a \<Rightarrow> real"
   7.140 -  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
   7.141 -  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"]) (auto split: split_indicator)
   7.142 -
   7.143  lemma tendsto_integral_at_top:
   7.144 -  fixes f :: "real \<Rightarrow> real"
   7.145 -  assumes M: "sets M = sets borel" and f[measurable]: "integrable M f"
   7.146 -  shows "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
   7.147 -proof -
   7.148 -  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
   7.149 -    using M by (simp add: sets_eq_imp_space_eq measurable_def)
   7.150 -  { fix f :: "real \<Rightarrow> real" assume f: "integrable M f" "\<And>x. 0 \<le> f x"
   7.151 -    then have [measurable]: "f \<in> borel_measurable borel"
   7.152 -      by (simp add: real_integrable_def)
   7.153 -    have "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
   7.154 -    proof (rule tendsto_at_topI_sequentially)
   7.155 -      have int: "\<And>n. integrable M (\<lambda>x. f x * indicator {.. n} x)"
   7.156 -        by (rule integrable_mult_indicator) (auto simp: M f)
   7.157 -      show "(\<lambda>n. \<integral> x. f x * indicator {..real n} x \<partial>M) ----> integral\<^sup>L M f"
   7.158 -      proof (rule integral_dominated_convergence)
   7.159 -        { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
   7.160 -            by (rule eventually_sequentiallyI[of "natceiling x"])
   7.161 -               (auto split: split_indicator simp: natceiling_le_eq) }
   7.162 -        from filterlim_cong[OF refl refl this]
   7.163 -        show "AE x in M. (\<lambda>n. f x * indicator {..real n} x) ----> f x"
   7.164 -          by (simp add: tendsto_const)
   7.165 -        show "\<And>j. AE x in M. norm (f x * indicator {.. j} x) \<le> f x"
   7.166 -          using f(2) by (intro AE_I2) (auto split: split_indicator)
   7.167 -      qed (simp | fact)+
   7.168 -      show "mono (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
   7.169 -        by (intro monoI integral_mono int) (auto split: split_indicator intro: f)
   7.170 -    qed }
   7.171 -  note nonneg = this
   7.172 -  let ?P = "\<lambda>y. \<integral> x. max 0 (f x) * indicator {..y} x \<partial>M"
   7.173 -  let ?N = "\<lambda>y. \<integral> x. max 0 (- f x) * indicator {..y} x \<partial>M"
   7.174 -  let ?p = "integral\<^sup>L M (\<lambda>x. max 0 (f x))"
   7.175 -  let ?n = "integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
   7.176 -  have "(?P ---> ?p) at_top" "(?N ---> ?n) at_top"
   7.177 -    by (auto intro!: nonneg f)
   7.178 -  note tendsto_diff[OF this]
   7.179 -  also have "(\<lambda>y. ?P y - ?N y) = (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
   7.180 -    by (subst integral_diff[symmetric])
   7.181 -       (auto intro!: integrable_mult_indicator f integral_cong
   7.182 -             simp: M split: split_max)
   7.183 -  also have "?p - ?n = integral\<^sup>L M f"
   7.184 -    by (subst integral_diff[symmetric]) (auto intro!: f integral_cong simp: M split: split_max)
   7.185 -  finally show ?thesis .
   7.186 +  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   7.187 +  assumes [simp]: "sets M = sets borel" and f[measurable]: "integrable M f"
   7.188 +  shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
   7.189 +proof (rule tendsto_at_topI_sequentially)
   7.190 +  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
   7.191 +  show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) ----> integral\<^sup>L M f"
   7.192 +  proof (rule integral_dominated_convergence)
   7.193 +    show "integrable M (\<lambda>x. norm (f x))"
   7.194 +      by (rule integrable_norm) fact
   7.195 +    show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
   7.196 +    proof
   7.197 +      fix x
   7.198 +      from `filterlim X at_top sequentially` 
   7.199 +      have "eventually (\<lambda>n. x \<le> X n) sequentially"
   7.200 +        unfolding filterlim_at_top_ge[where c=x] by auto
   7.201 +      then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
   7.202 +        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_elim1)
   7.203 +    qed
   7.204 +    fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
   7.205 +      by (auto split: split_indicator)
   7.206 +  qed auto
   7.207  qed
   7.208  
   7.209  lemma
     8.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Jun 18 15:23:40 2014 +0200
     8.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Jun 18 07:31:12 2014 +0200
     8.3 @@ -159,6 +159,18 @@
     8.4      using A by auto
     8.5  qed
     8.6  
     8.7 +lemma borel_measurable_continuous_countable_exceptions:
     8.8 +  fixes f :: "'a::t1_space \<Rightarrow> 'b::topological_space"
     8.9 +  assumes X: "countable X"
    8.10 +  assumes "continuous_on (- X) f"
    8.11 +  shows "f \<in> borel_measurable borel"
    8.12 +proof (rule measurable_discrete_difference[OF _ X])
    8.13 +  have "X \<in> sets borel"
    8.14 +    by (rule sets.countable[OF _ X]) auto
    8.15 +  then show "(\<lambda>x. if x \<in> X then undefined else f x) \<in> borel_measurable borel"
    8.16 +    by (intro borel_measurable_continuous_on_if assms continuous_intros)
    8.17 +qed auto
    8.18 +
    8.19  lemma borel_measurable_continuous_on1:
    8.20    "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
    8.21    using borel_measurable_continuous_on_if[of UNIV f "\<lambda>_. undefined"]
    8.22 @@ -691,6 +703,10 @@
    8.23  lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
    8.24    by (intro borel_measurable_continuous_on1 continuous_intros)
    8.25  
    8.26 +lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \<Rightarrow> 'a) \<in> borel_measurable borel"
    8.27 +  by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"])
    8.28 +     (auto intro!: continuous_on_sgn continuous_on_id)
    8.29 +
    8.30  lemma borel_measurable_uminus[measurable (raw)]:
    8.31    fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
    8.32    assumes g: "g \<in> borel_measurable M"
    8.33 @@ -780,21 +796,18 @@
    8.34    using affine_borel_measurable_vector[of f M a 1] by simp
    8.35  
    8.36  lemma borel_measurable_inverse[measurable (raw)]:
    8.37 -  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_div_algebra}"
    8.38 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra"
    8.39    assumes f: "f \<in> borel_measurable M"
    8.40    shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
    8.41 -proof -
    8.42 -  have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
    8.43 -    by (intro borel_measurable_continuous_on_open' continuous_intros) auto
    8.44 -  also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
    8.45 -    by (intro ext) auto
    8.46 -  finally show ?thesis using f by simp
    8.47 -qed
    8.48 +  apply (rule measurable_compose[OF f])
    8.49 +  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
    8.50 +  apply (auto intro!: continuous_on_inverse continuous_on_id)
    8.51 +  done
    8.52  
    8.53  lemma borel_measurable_divide[measurable (raw)]:
    8.54    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
    8.55 -    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_field}) \<in> borel_measurable M"
    8.56 -  by (simp add: field_divide_inverse)
    8.57 +    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \<in> borel_measurable M"
    8.58 +  by (simp add: divide_inverse)
    8.59  
    8.60  lemma borel_measurable_max[measurable (raw)]:
    8.61    "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"
    8.62 @@ -846,19 +859,10 @@
    8.63  lemma borel_measurable_ln[measurable (raw)]:
    8.64    assumes f: "f \<in> borel_measurable M"
    8.65    shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
    8.66 -proof -
    8.67 -  { fix x :: real assume x: "x \<le> 0"
    8.68 -    { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }
    8.69 -    from this[of x] x this[of 0] have "ln 0 = ln x"
    8.70 -      by (auto simp: ln_def) }
    8.71 -  note ln_imp = this
    8.72 -  have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
    8.73 -    by (rule borel_measurable_continuous_on_open[OF _ _ f])
    8.74 -       (auto intro!: continuous_intros)
    8.75 -  also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
    8.76 -    by (simp add: fun_eq_iff not_less ln_imp)
    8.77 -  finally show ?thesis .
    8.78 -qed
    8.79 +  apply (rule measurable_compose[OF f])
    8.80 +  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
    8.81 +  apply (auto intro!: continuous_on_ln continuous_on_id)
    8.82 +  done
    8.83  
    8.84  lemma borel_measurable_log[measurable (raw)]:
    8.85    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
     9.1 --- a/src/HOL/Probability/Distributions.thy	Wed Jun 18 15:23:40 2014 +0200
     9.2 +++ b/src/HOL/Probability/Distributions.thy	Wed Jun 18 07:31:12 2014 +0200
     9.3 @@ -9,258 +9,6 @@
     9.4    imports Convolution Information
     9.5  begin
     9.6  
     9.7 -lemma tendsto_at_topI_sequentially:
     9.8 -  fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
     9.9 -  assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) ----> y"
    9.10 -  shows "(f ---> y) at_top"
    9.11 -  unfolding filterlim_iff
    9.12 -proof safe
    9.13 -  fix P assume "eventually P (nhds y)"
    9.14 -  then have seq: "\<And>f. f ----> y \<Longrightarrow> eventually (\<lambda>x. P (f x)) at_top"
    9.15 -    unfolding eventually_nhds_iff_sequentially by simp
    9.16 -
    9.17 -  show "eventually (\<lambda>x. P (f x)) at_top"
    9.18 -  proof (rule ccontr)
    9.19 -    assume "\<not> eventually (\<lambda>x. P (f x)) at_top"
    9.20 -    then have "\<And>X. \<exists>x>X. \<not> P (f x)"
    9.21 -      unfolding eventually_at_top_dense by simp
    9.22 -    then obtain r where not_P: "\<And>x. \<not> P (f (r x))" and r: "\<And>x. x < r x"
    9.23 -      by metis
    9.24 -    
    9.25 -    def s \<equiv> "rec_nat (r 0) (\<lambda>_ x. r (x + 1))"
    9.26 -    then have [simp]: "s 0 = r 0" "\<And>n. s (Suc n) = r (s n + 1)"
    9.27 -      by auto
    9.28 -
    9.29 -    { fix n have "n < s n" using r
    9.30 -        by (induct n) (auto simp add: real_of_nat_Suc intro: less_trans add_strict_right_mono) }
    9.31 -    note s_subseq = this
    9.32 -
    9.33 -    have "mono s"
    9.34 -    proof (rule incseq_SucI)
    9.35 -      fix n show "s n \<le> s (Suc n)"
    9.36 -        using r[of "s n + 1"] by simp
    9.37 -    qed
    9.38 -
    9.39 -    have "filterlim s at_top sequentially"
    9.40 -      unfolding filterlim_at_top_gt[where c=0] eventually_sequentially
    9.41 -    proof (safe intro!: exI)
    9.42 -      fix Z :: real and n assume "0 < Z" "natceiling Z \<le> n"
    9.43 -      with real_natceiling_ge[of Z] `n < s n`
    9.44 -      show "Z \<le> s n"
    9.45 -        by auto
    9.46 -    qed
    9.47 -    moreover then have "eventually (\<lambda>x. P (f (s x))) sequentially"
    9.48 -      by (rule seq[OF *])
    9.49 -    then obtain n where "P (f (s n))"
    9.50 -      by (auto simp: eventually_sequentially)
    9.51 -    then show False
    9.52 -      using not_P by (cases n) auto
    9.53 -  qed
    9.54 -qed
    9.55 -  
    9.56 -lemma tendsto_integral_at_top:
    9.57 -  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
    9.58 -  assumes [simp]: "sets M = sets borel" and f[measurable]: "integrable M f"
    9.59 -  shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
    9.60 -proof (rule tendsto_at_topI_sequentially)
    9.61 -  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
    9.62 -  show "(\<lambda>n. \<integral>x. indicator {..X n} x *\<^sub>R f x \<partial>M) ----> integral\<^sup>L M f"
    9.63 -  proof (rule integral_dominated_convergence)
    9.64 -    show "integrable M (\<lambda>x. norm (f x))"
    9.65 -      by (rule integrable_norm) fact
    9.66 -    show "AE x in M. (\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
    9.67 -    proof
    9.68 -      fix x
    9.69 -      from `filterlim X at_top sequentially` 
    9.70 -      have "eventually (\<lambda>n. x \<le> X n) sequentially"
    9.71 -        unfolding filterlim_at_top_ge[where c=x] by auto
    9.72 -      then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
    9.73 -        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_elim1)
    9.74 -    qed
    9.75 -    fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
    9.76 -      by (auto split: split_indicator)
    9.77 -  qed auto
    9.78 -qed
    9.79 -
    9.80 -lemma filterlim_at_top_imp_at_infinity:
    9.81 -  fixes f :: "_ \<Rightarrow> real"
    9.82 -  shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
    9.83 -  by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
    9.84 -
    9.85 -lemma measurable_discrete_difference:
    9.86 -  fixes f :: "'a \<Rightarrow> 'b::t1_space"
    9.87 -  assumes f: "f \<in> measurable M N"
    9.88 -  assumes X: "countable X"
    9.89 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
    9.90 -  assumes space: "\<And>x. x \<in> X \<Longrightarrow> g x \<in> space N"
    9.91 -  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
    9.92 -  shows "g \<in> measurable M N"
    9.93 -  unfolding measurable_def
    9.94 -proof safe
    9.95 -  fix x assume "x \<in> space M" then show "g x \<in> space N"
    9.96 -    using measurable_space[OF f, of x] eq[of x] space[of x] by (cases "x \<in> X") auto
    9.97 -next
    9.98 -  fix S assume S: "S \<in> sets N"
    9.99 -  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})"
   9.100 -    using sets.sets_into_space[OF sets] eq by auto
   9.101 -  also have "\<dots> \<in> sets M"
   9.102 -    by (safe intro!: sets.Diff sets.Un measurable_sets[OF f] S sets.countable_UN' X countable_Collect sets)
   9.103 -  finally show "g -` S \<inter> space M \<in> sets M" .
   9.104 -qed
   9.105 -
   9.106 -lemma AE_discrete_difference:
   9.107 -  assumes X: "countable X"
   9.108 -  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
   9.109 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   9.110 -  shows "AE x in M. x \<notin> X"
   9.111 -proof -
   9.112 -  have X_sets: "(\<Union>x\<in>X. {x}) \<in> sets M"
   9.113 -    using assms by (intro sets.countable_UN') auto
   9.114 -  have "emeasure M (\<Union>x\<in>X. {x}) = (\<integral>\<^sup>+ i. emeasure M {i} \<partial>count_space X)"
   9.115 -    by (rule emeasure_UN_countable) (auto simp: assms disjoint_family_on_def)
   9.116 -  also have "\<dots> = (\<integral>\<^sup>+ i. 0 \<partial>count_space X)"
   9.117 -    by (intro nn_integral_cong) (simp add: null)
   9.118 -  finally show "AE x in M. x \<notin> X"
   9.119 -    using AE_iff_measurable[of X M "\<lambda>x. x \<notin> X"] X_sets sets.sets_into_space[OF sets] by auto
   9.120 -qed
   9.121 -
   9.122 -lemma integrable_discrete_difference:
   9.123 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   9.124 -  assumes X: "countable X"
   9.125 -  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
   9.126 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   9.127 -  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   9.128 -  shows "integrable M f \<longleftrightarrow> integrable M g"
   9.129 -  unfolding integrable_iff_bounded
   9.130 -proof (rule conj_cong)
   9.131 -  { assume "f \<in> borel_measurable M" then have "g \<in> borel_measurable M"
   9.132 -      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
   9.133 -  moreover
   9.134 -  { assume "g \<in> borel_measurable M" then have "f \<in> borel_measurable M"
   9.135 -      by (rule measurable_discrete_difference[where X=X]) (auto simp: assms) }
   9.136 -  ultimately show "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" ..
   9.137 -next
   9.138 -  have "AE x in M. x \<notin> X"
   9.139 -    by (rule AE_discrete_difference) fact+
   9.140 -  then have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. norm (g x) \<partial>M)"
   9.141 -    by (intro nn_integral_cong_AE) (auto simp: eq)
   9.142 -  then show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity> \<longleftrightarrow> (\<integral>\<^sup>+ x. norm (g x) \<partial>M) < \<infinity>"
   9.143 -    by simp
   9.144 -qed
   9.145 -
   9.146 -lemma integral_discrete_difference:
   9.147 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   9.148 -  assumes X: "countable X"
   9.149 -  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
   9.150 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   9.151 -  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   9.152 -  shows "integral\<^sup>L M f = integral\<^sup>L M g"
   9.153 -proof (rule integral_eq_cases)
   9.154 -  show eq: "integrable M f \<longleftrightarrow> integrable M g"
   9.155 -    by (rule integrable_discrete_difference[where X=X]) fact+
   9.156 -
   9.157 -  assume f: "integrable M f"
   9.158 -  show "integral\<^sup>L M f = integral\<^sup>L M g"
   9.159 -  proof (rule integral_cong_AE)
   9.160 -    show "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   9.161 -      using f eq by (auto intro: borel_measurable_integrable)
   9.162 -
   9.163 -    have "AE x in M. x \<notin> X"
   9.164 -      by (rule AE_discrete_difference) fact+
   9.165 -    with AE_space show "AE x in M. f x = g x"
   9.166 -      by eventually_elim fact
   9.167 -  qed
   9.168 -qed
   9.169 -
   9.170 -lemma has_bochner_integral_discrete_difference:
   9.171 -  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   9.172 -  assumes X: "countable X"
   9.173 -  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
   9.174 -  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   9.175 -  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   9.176 -  shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
   9.177 -  using integrable_discrete_difference[of X M f g, OF assms]
   9.178 -  using integral_discrete_difference[of X M f g, OF assms]
   9.179 -  by (metis has_bochner_integral_iff)
   9.180 -
   9.181 -lemma has_bochner_integral_even_function:
   9.182 -  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   9.183 -  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   9.184 -  assumes even: "\<And>x. f (- x) = f x"
   9.185 -  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
   9.186 -proof -
   9.187 -  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   9.188 -    by (auto split: split_indicator)
   9.189 -  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
   9.190 -    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   9.191 -       (auto simp: indicator even f)
   9.192 -  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)"
   9.193 -    by (rule has_bochner_integral_add)
   9.194 -  then have "has_bochner_integral lborel f (x + x)"
   9.195 -    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   9.196 -       (auto split: split_indicator)
   9.197 -  then show ?thesis
   9.198 -    by (simp add: scaleR_2)
   9.199 -qed
   9.200 -
   9.201 -lemma has_bochner_integral_odd_function:
   9.202 -  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   9.203 -  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   9.204 -  assumes odd: "\<And>x. f (- x) = - f x"
   9.205 -  shows "has_bochner_integral lborel f 0"
   9.206 -proof -
   9.207 -  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   9.208 -    by (auto split: split_indicator)
   9.209 -  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
   9.210 -    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   9.211 -       (auto simp: indicator odd f)
   9.212 -  from has_bochner_integral_minus[OF this]
   9.213 -  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
   9.214 -    by simp 
   9.215 -  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)"
   9.216 -    by (rule has_bochner_integral_add)
   9.217 -  then have "has_bochner_integral lborel f (x + - x)"
   9.218 -    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   9.219 -       (auto split: split_indicator)
   9.220 -  then show ?thesis
   9.221 -    by simp
   9.222 -qed
   9.223 -
   9.224 -
   9.225 -lemma filterlim_power2_at_top[intro]: "filterlim (\<lambda>(x::real). x\<^sup>2) at_top at_top"
   9.226 -  by (auto intro!: filterlim_at_top_mult_at_top filterlim_ident simp: power2_eq_square)
   9.227 -
   9.228 -lemma distributed_integrable_var:
   9.229 -  fixes X :: "'a \<Rightarrow> real"
   9.230 -  shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X"
   9.231 -  using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp
   9.232 -
   9.233 -lemma (in ordered_comm_monoid_add) setsum_pos: 
   9.234 -  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
   9.235 -  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
   9.236 -
   9.237 -lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
   9.238 -  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult_commute)
   9.239 -
   9.240 -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"
   9.241 -  using sets_eq_imp_space_eq[of N L] by (simp add: distr_def Int_def cong: rev_conj_cong)
   9.242 -
   9.243 -lemma AE_borel_affine: 
   9.244 -  fixes P :: "real \<Rightarrow> bool"
   9.245 -  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)"
   9.246 -  by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
   9.247 -     (simp_all add: AE_density AE_distr_iff field_simps)
   9.248 -
   9.249 -lemma density_distr:
   9.250 -  assumes [measurable]: "f \<in> borel_measurable N" "X \<in> measurable M N"
   9.251 -  shows "density (distr M N X) f = distr (density M (\<lambda>x. f (X x))) N X"
   9.252 -  by (intro measure_eqI)
   9.253 -     (auto simp add: emeasure_density nn_integral_distr emeasure_distr
   9.254 -           split: split_indicator intro!: nn_integral_cong)
   9.255 -
   9.256 -lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
   9.257 -  by (simp split: split_indicator)
   9.258 -
   9.259  lemma (in prob_space) distributed_affine:
   9.260    fixes f :: "real \<Rightarrow> ereal"
   9.261    assumes f: "distributed M lborel X f"
   9.262 @@ -1178,7 +926,8 @@
   9.263    proof (rule nn_integral_FTC_atLeast)
   9.264      have "((\<lambda>x::real. - exp (- x\<^sup>2) / 2) ---> - 0 / 2) at_top"
   9.265        by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot]
   9.266 -                   filterlim_compose[OF filterlim_uminus_at_bot_at_top])
   9.267 +                   filterlim_compose[OF filterlim_uminus_at_bot_at_top]
   9.268 +                   filterlim_pow_at_top filterlim_ident)
   9.269           auto
   9.270      then show "((\<lambda>a::real. - exp (- a\<^sup>2) / 2) ---> 0) at_top"
   9.271        by simp
   9.272 @@ -1211,14 +960,17 @@
   9.273          assume "even k"
   9.274          have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top"
   9.275            by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0]
   9.276 -                   filterlim_at_top_imp_at_infinity filterlim_ident filterlim_power2_at_top)
   9.277 +                   filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident)
   9.278 +             auto
   9.279          also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)"
   9.280            using `even k` by (auto simp: even_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
   9.281          finally show ?thesis by simp
   9.282        next
   9.283          assume "odd k"
   9.284          have "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top"
   9.285 -          by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity filterlim_ident filterlim_power2_at_top)
   9.286 +          by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity
   9.287 +                    filterlim_ident filterlim_pow_at_top)
   9.288 +             auto
   9.289          also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)"
   9.290            using `odd k` by (auto simp: odd_Suc_mult_two_ex fun_eq_iff exp_minus field_simps power2_eq_square power_mult)
   9.291          finally show ?thesis by simp
    10.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Jun 18 15:23:40 2014 +0200
    10.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Jun 18 07:31:12 2014 +0200
    10.3 @@ -1274,18 +1274,53 @@
    10.4              =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" 
    10.5    using integral_by_parts[OF assms] by (simp add: mult_ac)
    10.6  
    10.7 -lemma integral_tendsto_at_top:
    10.8 -  fixes f :: "real \<Rightarrow> real"
    10.9 -  assumes [simp, intro]: "\<And>x. isCont f x"
   10.10 -  assumes [simp, arith]: "\<And>x. 0 \<le> f x"
   10.11 -  assumes [simp]: "integrable lborel f"
   10.12 -  assumes [measurable]: "f \<in> borel_measurable borel"
   10.13 -  shows "((\<lambda>x. \<integral>xa. f xa * indicator {0..x} xa \<partial>lborel) ---> \<integral>xa. f xa * indicator {0..} xa \<partial>lborel) at_top"
   10.14 -  apply (auto intro!: borel_integrable_atLeastAtMost monoI integral_mono tendsto_at_topI_sequentially  
   10.15 -    split:split_indicator)
   10.16 -  apply (rule integral_dominated_convergence[where w = " \<lambda>x. f x * indicator {0..} x"])
   10.17 -  unfolding LIMSEQ_def  
   10.18 -  apply (auto intro!: AE_I2 tendsto_mult integrable_mult_indicator split: split_indicator)
   10.19 -  by (metis ge_natfloor_plus_one_imp_gt less_imp_le)
   10.20 +lemma AE_borel_affine: 
   10.21 +  fixes P :: "real \<Rightarrow> bool"
   10.22 +  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)"
   10.23 +  by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
   10.24 +     (simp_all add: AE_density AE_distr_iff field_simps)
   10.25 +
   10.26 +lemma has_bochner_integral_even_function:
   10.27 +  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   10.28 +  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   10.29 +  assumes even: "\<And>x. f (- x) = f x"
   10.30 +  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
   10.31 +proof -
   10.32 +  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   10.33 +    by (auto split: split_indicator)
   10.34 +  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
   10.35 +    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   10.36 +       (auto simp: indicator even f)
   10.37 +  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)"
   10.38 +    by (rule has_bochner_integral_add)
   10.39 +  then have "has_bochner_integral lborel f (x + x)"
   10.40 +    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   10.41 +       (auto split: split_indicator)
   10.42 +  then show ?thesis
   10.43 +    by (simp add: scaleR_2)
   10.44 +qed
   10.45 +
   10.46 +lemma has_bochner_integral_odd_function:
   10.47 +  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   10.48 +  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   10.49 +  assumes odd: "\<And>x. f (- x) = - f x"
   10.50 +  shows "has_bochner_integral lborel f 0"
   10.51 +proof -
   10.52 +  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   10.53 +    by (auto split: split_indicator)
   10.54 +  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
   10.55 +    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   10.56 +       (auto simp: indicator odd f)
   10.57 +  from has_bochner_integral_minus[OF this]
   10.58 +  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
   10.59 +    by simp 
   10.60 +  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)"
   10.61 +    by (rule has_bochner_integral_add)
   10.62 +  then have "has_bochner_integral lborel f (x + - x)"
   10.63 +    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   10.64 +       (auto split: split_indicator)
   10.65 +  then show ?thesis
   10.66 +    by simp
   10.67 +qed
   10.68  
   10.69  end
    11.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 15:23:40 2014 +0200
    11.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 07:31:12 2014 +0200
    11.3 @@ -23,6 +23,9 @@
    11.4  lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
    11.5    by (auto simp: indicator_def one_ereal_def)
    11.6  
    11.7 +lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
    11.8 +  by (simp split: split_indicator)
    11.9 +
   11.10  lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
   11.11    unfolding indicator_def by auto
   11.12  
   11.13 @@ -793,26 +796,42 @@
   11.14      by (auto intro!: antisym)
   11.15  qed
   11.16  
   11.17 -lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
   11.18 +lemma UN_from_nat_into: 
   11.19 +  assumes I: "countable I" "I \<noteq> {}"
   11.20 +  shows "(\<Union>i\<in>I. N i) = (\<Union>i. N (from_nat_into I i))"
   11.21  proof -
   11.22 -  have "\<Union>range N = \<Union>(N ` range from_nat)" by simp
   11.23 -  then have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
   11.24 +  have "(\<Union>i\<in>I. N i) = \<Union>(N ` range (from_nat_into I))"
   11.25 +    using I by simp
   11.26 +  also have "\<dots> = (\<Union>i. (N \<circ> from_nat_into I) i)"
   11.27      by (simp only: SUP_def image_comp)
   11.28 -  then show ?thesis by simp
   11.29 +  finally show ?thesis by simp
   11.30 +qed
   11.31 +
   11.32 +lemma null_sets_UN':
   11.33 +  assumes "countable I"
   11.34 +  assumes "\<And>i. i \<in> I \<Longrightarrow> N i \<in> null_sets M"
   11.35 +  shows "(\<Union>i\<in>I. N i) \<in> null_sets M"
   11.36 +proof cases
   11.37 +  assume "I = {}" then show ?thesis by simp
   11.38 +next
   11.39 +  assume "I \<noteq> {}"
   11.40 +  show ?thesis
   11.41 +  proof (intro conjI CollectI null_setsI)
   11.42 +    show "(\<Union>i\<in>I. N i) \<in> sets M"
   11.43 +      using assms by (intro sets.countable_UN') auto
   11.44 +    have "emeasure M (\<Union>i\<in>I. N i) \<le> (\<Sum>n. emeasure M (N (from_nat_into I n)))"
   11.45 +      unfolding UN_from_nat_into[OF `countable I` `I \<noteq> {}`]
   11.46 +      using assms `I \<noteq> {}` by (intro emeasure_subadditive_countably) (auto intro: from_nat_into)
   11.47 +    also have "(\<lambda>n. emeasure M (N (from_nat_into I n))) = (\<lambda>_. 0)"
   11.48 +      using assms `I \<noteq> {}` by (auto intro: from_nat_into)
   11.49 +    finally show "emeasure M (\<Union>i\<in>I. N i) = 0"
   11.50 +      by (intro antisym emeasure_nonneg) simp
   11.51 +  qed
   11.52  qed
   11.53  
   11.54  lemma null_sets_UN[intro]:
   11.55 -  assumes "\<And>i::'i::countable. N i \<in> null_sets M"
   11.56 -  shows "(\<Union>i. N i) \<in> null_sets M"
   11.57 -proof (intro conjI CollectI null_setsI)
   11.58 -  show "(\<Union>i. N i) \<in> sets M" using assms by auto
   11.59 -  have "0 \<le> emeasure M (\<Union>i. N i)" by (rule emeasure_nonneg)
   11.60 -  moreover have "emeasure M (\<Union>i. N i) \<le> (\<Sum>n. emeasure M (N (Countable.from_nat n)))"
   11.61 -    unfolding UN_from_nat[of N]
   11.62 -    using assms by (intro emeasure_subadditive_countably) auto
   11.63 -  ultimately show "emeasure M (\<Union>i. N i) = 0"
   11.64 -    using assms by (auto simp: null_setsD1)
   11.65 -qed
   11.66 +  "(\<And>i::'i::countable. N i \<in> null_sets M) \<Longrightarrow> (\<Union>i. N i) \<in> null_sets M"
   11.67 +  by (rule null_sets_UN') auto
   11.68  
   11.69  lemma null_set_Int1:
   11.70    assumes "B \<in> null_sets M" "A \<in> sets M" shows "A \<inter> B \<in> null_sets M"
   11.71 @@ -1021,6 +1040,18 @@
   11.72      unfolding eventually_ae_filter by auto
   11.73  qed auto
   11.74  
   11.75 +lemma AE_discrete_difference:
   11.76 +  assumes X: "countable X"
   11.77 +  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
   11.78 +  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   11.79 +  shows "AE x in M. x \<notin> X"
   11.80 +proof -
   11.81 +  have "(\<Union>x\<in>X. {x}) \<in> null_sets M"
   11.82 +    using assms by (intro null_sets_UN') auto
   11.83 +  from AE_not_in[OF this] show "AE x in M. x \<notin> X"
   11.84 +    by auto
   11.85 +qed
   11.86 +
   11.87  lemma AE_finite_all:
   11.88    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)"
   11.89    using f by induct auto
    12.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Jun 18 15:23:40 2014 +0200
    12.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Jun 18 07:31:12 2014 +0200
    12.3 @@ -1990,6 +1990,13 @@
    12.4       (auto intro!: nn_integral_cong_AE
    12.5             simp: measurable_If max_def ereal_zero_le_0_iff nn_integral_density')
    12.6  
    12.7 +lemma density_distr:
    12.8 +  assumes [measurable]: "f \<in> borel_measurable N" "X \<in> measurable M N"
    12.9 +  shows "density (distr M N X) f = distr (density M (\<lambda>x. f (X x))) N X"
   12.10 +  by (intro measure_eqI)
   12.11 +     (auto simp add: emeasure_density nn_integral_distr emeasure_distr
   12.12 +           split: split_indicator intro!: nn_integral_cong)
   12.13 +
   12.14  lemma emeasure_restricted:
   12.15    assumes S: "S \<in> sets M" and X: "X \<in> sets M"
   12.16    shows "emeasure (density M (indicator S)) X = emeasure M (S \<inter> X)"
    13.1 --- a/src/HOL/Probability/Probability_Measure.thy	Wed Jun 18 15:23:40 2014 +0200
    13.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Wed Jun 18 07:31:12 2014 +0200
    13.3 @@ -745,6 +745,11 @@
    13.4    finally show ?thesis .
    13.5  qed
    13.6  
    13.7 +lemma distributed_integrable_var:
    13.8 +  fixes X :: "'a \<Rightarrow> real"
    13.9 +  shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X"
   13.10 +  using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp
   13.11 +
   13.12  lemma (in prob_space) distributed_variance:
   13.13    fixes f::"real \<Rightarrow> real"
   13.14    assumes D: "distributed M lborel X f"
    14.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Jun 18 15:23:40 2014 +0200
    14.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Jun 18 07:31:12 2014 +0200
    14.3 @@ -364,6 +364,17 @@
    14.4    finally show ?thesis .
    14.5  qed
    14.6  
    14.7 +
    14.8 +lemma (in sigma_algebra) countable:
    14.9 +  assumes "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> M" "countable A"
   14.10 +  shows "A \<in> M"
   14.11 +proof -
   14.12 +  have "(\<Union>a\<in>A. {a}) \<in> M"
   14.13 +    using assms by (intro countable_UN') auto
   14.14 +  also have "(\<Union>a\<in>A. {a}) = A" by auto
   14.15 +  finally show ?thesis by auto
   14.16 +qed
   14.17 +
   14.18  lemma ring_of_sets_Pow: "ring_of_sets sp (Pow sp)"
   14.19    by (auto simp: ring_of_sets_iff)
   14.20  
   14.21 @@ -2028,6 +2039,26 @@
   14.22      done
   14.23  qed
   14.24  
   14.25 +lemma measurable_discrete_difference:
   14.26 +  assumes f: "f \<in> measurable M N"
   14.27 +  assumes X: "countable X"
   14.28 +  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   14.29 +  assumes space: "\<And>x. x \<in> X \<Longrightarrow> g x \<in> space N"
   14.30 +  assumes eq: "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   14.31 +  shows "g \<in> measurable M N"
   14.32 +  unfolding measurable_def
   14.33 +proof safe
   14.34 +  fix x assume "x \<in> space M" then show "g x \<in> space N"
   14.35 +    using measurable_space[OF f, of x] eq[of x] space[of x] by (cases "x \<in> X") auto
   14.36 +next
   14.37 +  fix S assume S: "S \<in> sets N"
   14.38 +  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})"
   14.39 +    using sets.sets_into_space[OF sets] eq by auto
   14.40 +  also have "\<dots> \<in> sets M"
   14.41 +    by (safe intro!: sets.Diff sets.Un measurable_sets[OF f] S sets.countable_UN' X countable_Collect sets)
   14.42 +  finally show "g -` S \<inter> space M \<in> sets M" .
   14.43 +qed
   14.44 +
   14.45  lemma measurable_mono1:
   14.46    "M' \<subseteq> Pow \<Omega> \<Longrightarrow> M \<subseteq> M' \<Longrightarrow>
   14.47      measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
    15.1 --- a/src/HOL/Rat.thy	Wed Jun 18 15:23:40 2014 +0200
    15.2 +++ b/src/HOL/Rat.thy	Wed Jun 18 07:31:12 2014 +0200
    15.3 @@ -916,6 +916,8 @@
    15.4    "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
    15.5    by (rule Rats_cases) auto
    15.6  
    15.7 +lemma Rats_infinite: "\<not> finite \<rat>"
    15.8 +  by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def)
    15.9  
   15.10  subsection {* Implementation of rational numbers as pairs of integers *}
   15.11  
    16.1 --- a/src/HOL/Real.thy	Wed Jun 18 15:23:40 2014 +0200
    16.2 +++ b/src/HOL/Real.thy	Wed Jun 18 07:31:12 2014 +0200
    16.3 @@ -1319,7 +1319,6 @@
    16.4  lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
    16.5  by (simp add: real_eq_of_nat)
    16.6  
    16.7 -
    16.8  lemma Rats_eq_int_div_int:
    16.9    "\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
   16.10  proof
   16.11 @@ -1996,6 +1995,9 @@
   16.12    unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
   16.13    by simp
   16.14  
   16.15 +lemma Rats_unbounded: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
   16.16 +  by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
   16.17 +
   16.18  subsection {* Exponentiation with floor *}
   16.19  
   16.20  lemma floor_power:
    17.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 15:23:40 2014 +0200
    17.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
    17.3 @@ -856,15 +856,64 @@
    17.4  lemma setprod_norm:
    17.5    fixes f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
    17.6    shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
    17.7 -proof (cases "finite A")
    17.8 -  case True then show ?thesis 
    17.9 -    by (induct A rule: finite_induct) (auto simp: norm_mult)
   17.10 -next
   17.11 -  case False then show ?thesis
   17.12 -    by (metis norm_one setprod.infinite) 
   17.13 +  by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
   17.14 +
   17.15 +lemma norm_setprod_le: 
   17.16 +  "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1, comm_monoid_mult}))"
   17.17 +proof (induction A rule: infinite_finite_induct)
   17.18 +  case (insert a A)
   17.19 +  then have "norm (setprod f (insert a A)) \<le> norm (f a) * norm (setprod f A)"
   17.20 +    by (simp add: norm_mult_ineq)
   17.21 +  also have "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a))"
   17.22 +    by (rule insert)
   17.23 +  finally show ?case
   17.24 +    by (simp add: insert mult_left_mono)
   17.25 +qed simp_all
   17.26 +
   17.27 +lemma norm_setprod_diff:
   17.28 +  fixes z w :: "'i \<Rightarrow> 'a::{real_normed_algebra_1, comm_monoid_mult}"
   17.29 +  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>
   17.30 +    norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))" 
   17.31 +proof (induction I rule: infinite_finite_induct)
   17.32 +  case (insert i I)
   17.33 +  note insert.hyps[simp]
   17.34 +
   17.35 +  have "norm ((\<Prod>i\<in>insert i I. z i) - (\<Prod>i\<in>insert i I. w i)) =
   17.36 +    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)"
   17.37 +    (is "_ = norm (?t1 + ?t2)")
   17.38 +    by (auto simp add: field_simps)
   17.39 +  also have "... \<le> norm ?t1 + norm ?t2"
   17.40 +    by (rule norm_triangle_ineq)
   17.41 +  also have "norm ?t1 \<le> norm (\<Prod>i\<in>I. z i) * norm (z i - w i)"
   17.42 +    by (rule norm_mult_ineq)
   17.43 +  also have "\<dots> \<le> (\<Prod>i\<in>I. norm (z i)) * norm(z i - w i)"
   17.44 +    by (rule mult_right_mono) (auto intro: norm_setprod_le)
   17.45 +  also have "(\<Prod>i\<in>I. norm (z i)) \<le> (\<Prod>i\<in>I. 1)"
   17.46 +    by (intro setprod_mono) (auto intro!: insert)
   17.47 +  also have "norm ?t2 \<le> norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * norm (w i)"
   17.48 +    by (rule norm_mult_ineq)
   17.49 +  also have "norm (w i) \<le> 1"
   17.50 +    by (auto intro: insert)
   17.51 +  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))"
   17.52 +    using insert by auto
   17.53 +  finally show ?case
   17.54 +    by (auto simp add: add_ac mult_right_mono mult_left_mono)
   17.55 +qed simp_all
   17.56 +
   17.57 +lemma norm_power_diff: 
   17.58 +  fixes z w :: "'a::{real_normed_algebra_1, comm_monoid_mult}"
   17.59 +  assumes "norm z \<le> 1" "norm w \<le> 1"
   17.60 +  shows "norm (z^m - w^m) \<le> m * norm (z - w)"
   17.61 +proof -
   17.62 +  have "norm (z^m - w^m) = norm ((\<Prod> i < m. z) - (\<Prod> i < m. w))"
   17.63 +    by (simp add: setprod_constant)
   17.64 +  also have "\<dots> \<le> (\<Sum>i<m. norm (z - w))"
   17.65 +    by (intro norm_setprod_diff) (auto simp add: assms)
   17.66 +  also have "\<dots> = m * norm (z - w)"
   17.67 +    by (simp add: real_of_nat_def)
   17.68 +  finally show ?thesis .
   17.69  qed
   17.70  
   17.71 -
   17.72  subsection {* Metric spaces *}
   17.73  
   17.74  class metric_space = open_dist +
   17.75 @@ -1734,6 +1783,55 @@
   17.76  instance real :: banach by default
   17.77  
   17.78  lemma tendsto_at_topI_sequentially:
   17.79 +  fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
   17.80 +  assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) ----> y"
   17.81 +  shows "(f ---> y) at_top"
   17.82 +  unfolding filterlim_iff
   17.83 +proof safe
   17.84 +  fix P assume "eventually P (nhds y)"
   17.85 +  then have seq: "\<And>f. f ----> y \<Longrightarrow> eventually (\<lambda>x. P (f x)) at_top"
   17.86 +    unfolding eventually_nhds_iff_sequentially by simp
   17.87 +
   17.88 +  show "eventually (\<lambda>x. P (f x)) at_top"
   17.89 +  proof (rule ccontr)
   17.90 +    assume "\<not> eventually (\<lambda>x. P (f x)) at_top"
   17.91 +    then have "\<And>X. \<exists>x>X. \<not> P (f x)"
   17.92 +      unfolding eventually_at_top_dense by simp
   17.93 +    then obtain r where not_P: "\<And>x. \<not> P (f (r x))" and r: "\<And>x. x < r x"
   17.94 +      by metis
   17.95 +    
   17.96 +    def s \<equiv> "rec_nat (r 0) (\<lambda>_ x. r (x + 1))"
   17.97 +    then have [simp]: "s 0 = r 0" "\<And>n. s (Suc n) = r (s n + 1)"
   17.98 +      by auto
   17.99 +
  17.100 +    { fix n have "n < s n" using r
  17.101 +        by (induct n) (auto simp add: real_of_nat_Suc intro: less_trans add_strict_right_mono) }
  17.102 +    note s_subseq = this
  17.103 +
  17.104 +    have "mono s"
  17.105 +    proof (rule incseq_SucI)
  17.106 +      fix n show "s n \<le> s (Suc n)"
  17.107 +        using r[of "s n + 1"] by simp
  17.108 +    qed
  17.109 +
  17.110 +    have "filterlim s at_top sequentially"
  17.111 +      unfolding filterlim_at_top_gt[where c=0] eventually_sequentially
  17.112 +    proof (safe intro!: exI)
  17.113 +      fix Z :: real and n assume "0 < Z" "natceiling Z \<le> n"
  17.114 +      with real_natceiling_ge[of Z] `n < s n`
  17.115 +      show "Z \<le> s n"
  17.116 +        by auto
  17.117 +    qed
  17.118 +    moreover then have "eventually (\<lambda>x. P (f (s x))) sequentially"
  17.119 +      by (rule seq[OF *])
  17.120 +    then obtain n where "P (f (s n))"
  17.121 +      by (auto simp: eventually_sequentially)
  17.122 +    then show False
  17.123 +      using not_P by (cases n) auto
  17.124 +  qed
  17.125 +qed
  17.126 +
  17.127 +lemma tendsto_at_topI_sequentially_real:
  17.128    fixes f :: "real \<Rightarrow> real"
  17.129    assumes mono: "mono f"
  17.130    assumes limseq: "(\<lambda>n. f (real n)) ----> y"
    18.1 --- a/src/HOL/Series.thy	Wed Jun 18 15:23:40 2014 +0200
    18.2 +++ b/src/HOL/Series.thy	Wed Jun 18 07:31:12 2014 +0200
    18.3 @@ -344,6 +344,14 @@
    18.4  lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
    18.5  lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
    18.6  
    18.7 +lemmas sums_scaleR_left = bounded_linear.sums[OF bounded_linear_scaleR_left]
    18.8 +lemmas summable_scaleR_left = bounded_linear.summable[OF bounded_linear_scaleR_left]
    18.9 +lemmas suminf_scaleR_left = bounded_linear.suminf[OF bounded_linear_scaleR_left]
   18.10 +
   18.11 +lemmas sums_scaleR_right = bounded_linear.sums[OF bounded_linear_scaleR_right]
   18.12 +lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
   18.13 +lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
   18.14 +
   18.15  subsection {* Infinite summability on real normed algebras *}
   18.16  
   18.17  context
    19.1 --- a/src/HOL/Topological_Spaces.thy	Wed Jun 18 15:23:40 2014 +0200
    19.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
    19.3 @@ -789,13 +789,13 @@
    19.4    by (simp add: at_eq_bot_iff not_open_singleton)
    19.5  
    19.6  lemma eventually_at_right:
    19.7 -  fixes x :: "'a :: {no_top, linorder_topology}"
    19.8 +  fixes x :: "'a :: linorder_topology"
    19.9 +  assumes gt_ex: "x < y"
   19.10    shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
   19.11    unfolding eventually_at_topological
   19.12  proof safe
   19.13 -  obtain y where "x < y" using gt_ex[of x] ..
   19.14 +  note gt_ex
   19.15    moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
   19.16 -  moreover note gt_ex[of x]
   19.17    moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
   19.18    ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
   19.19      by (auto simp: subset_eq Ball_def)
   19.20 @@ -806,11 +806,12 @@
   19.21  qed
   19.22  
   19.23  lemma eventually_at_left:
   19.24 -  fixes x :: "'a :: {no_bot, linorder_topology}"
   19.25 +  fixes x :: "'a :: linorder_topology"
   19.26 +  assumes lt_ex: "y < x"
   19.27    shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
   19.28    unfolding eventually_at_topological
   19.29  proof safe
   19.30 -  obtain y where "y < x" using lt_ex[of x] ..
   19.31 +  note lt_ex
   19.32    moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
   19.33    moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
   19.34    ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
   19.35 @@ -821,13 +822,21 @@
   19.36      by (intro exI[of _ "{b <..}"]) auto
   19.37  qed
   19.38  
   19.39 +lemma trivial_limit_at_right_top: "at_right (top::_::{order_top, linorder_topology}) = bot"
   19.40 +  unfolding filter_eq_iff eventually_at_topological by auto
   19.41 +
   19.42 +lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot, linorder_topology}) = bot"
   19.43 +  unfolding filter_eq_iff eventually_at_topological by auto
   19.44 +
   19.45  lemma trivial_limit_at_left_real [simp]:
   19.46 -  "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"
   19.47 -  unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
   19.48 +  "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_order, linorder_topology}))"
   19.49 +  using lt_ex[of x]
   19.50 +  by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense)
   19.51  
   19.52  lemma trivial_limit_at_right_real [simp]:
   19.53 -  "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"
   19.54 -  unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
   19.55 +  "\<not> trivial_limit (at_right (x::'a::{no_top, dense_order, linorder_topology}))"
   19.56 +  using gt_ex[of x]
   19.57 +  by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
   19.58  
   19.59  lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
   19.60    by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
   19.61 @@ -867,6 +876,15 @@
   19.62    "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
   19.63    by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
   19.64  
   19.65 +lemma filterlim_mono_eventually:
   19.66 +  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
   19.67 +  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
   19.68 +  shows "filterlim f' F' G'"
   19.69 +  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
   19.70 +  apply (rule filterlim_mono[OF _ ord])
   19.71 +  apply fact
   19.72 +  done
   19.73 +
   19.74  lemma filterlim_principal:
   19.75    "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   19.76    unfolding filterlim_def eventually_filtermap le_principal ..
   19.77 @@ -1179,7 +1197,7 @@
   19.78    by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
   19.79  
   19.80  lemma filterlim_at_bot_at_right:
   19.81 -  fixes f :: "'a::{no_top, linorder_topology} \<Rightarrow> 'b::linorder"
   19.82 +  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   19.83    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   19.84    assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   19.85    assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b"
   19.86 @@ -1194,14 +1212,14 @@
   19.87      with x have "P z" by auto
   19.88      have "eventually (\<lambda>x. x \<le> g z) (at_right a)"
   19.89        using bound[OF bij(2)[OF `P z`]]
   19.90 -      unfolding eventually_at_right by (auto intro!: exI[of _ "g z"])
   19.91 +      unfolding eventually_at_right[OF bound[OF bij(2)[OF `P z`]]] by (auto intro!: exI[of _ "g z"])
   19.92      with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)"
   19.93        by eventually_elim (metis bij `P z` mono)
   19.94    qed
   19.95  qed
   19.96  
   19.97  lemma filterlim_at_top_at_left:
   19.98 -  fixes f :: "'a::{no_bot, linorder_topology} \<Rightarrow> 'b::linorder"
   19.99 +  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
  19.100    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
  19.101    assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
  19.102    assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a"
  19.103 @@ -1216,7 +1234,7 @@
  19.104      with x have "P z" by auto
  19.105      have "eventually (\<lambda>x. g z \<le> x) (at_left a)"
  19.106        using bound[OF bij(2)[OF `P z`]]
  19.107 -      unfolding eventually_at_left by (auto intro!: exI[of _ "g z"])
  19.108 +      unfolding eventually_at_left[OF bound[OF bij(2)[OF `P z`]]] by (auto intro!: exI[of _ "g z"])
  19.109      with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)"
  19.110        by eventually_elim (metis bij `P z` mono)
  19.111    qed
    20.1 --- a/src/HOL/Transcendental.thy	Wed Jun 18 15:23:40 2014 +0200
    20.2 +++ b/src/HOL/Transcendental.thy	Wed Jun 18 07:31:12 2014 +0200
    20.3 @@ -1303,29 +1303,42 @@
    20.4  lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
    20.5    by simp
    20.6  
    20.7 -lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
    20.8 -  apply (subgoal_tac "isCont ln (exp (ln x))", simp)
    20.9 -  apply (rule isCont_inverse_function [where f=exp], simp_all)
   20.10 -  done
   20.11 +lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
   20.12 +  by (auto simp add: ln_def intro!: arg_cong[where f=The])
   20.13 +
   20.14 +lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
   20.15 +proof cases
   20.16 +  assume "0 < x"
   20.17 +  moreover then have "isCont ln (exp (ln x))"
   20.18 +    by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
   20.19 +  ultimately show ?thesis
   20.20 +    by simp
   20.21 +next
   20.22 +  assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
   20.23 +    unfolding isCont_def
   20.24 +    by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
   20.25 +       (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
   20.26 +                intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
   20.27 +qed
   20.28  
   20.29  lemma tendsto_ln [tendsto_intros]:
   20.30 -  "(f ---> a) F \<Longrightarrow> 0 < a \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
   20.31 +  "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
   20.32    by (rule isCont_tendsto_compose [OF isCont_ln])
   20.33  
   20.34  lemma continuous_ln:
   20.35 -  "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
   20.36 +  "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
   20.37    unfolding continuous_def by (rule tendsto_ln)
   20.38  
   20.39  lemma isCont_ln' [continuous_intros]:
   20.40 -  "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
   20.41 +  "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
   20.42    unfolding continuous_at by (rule tendsto_ln)
   20.43  
   20.44  lemma continuous_within_ln [continuous_intros]:
   20.45 -  "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
   20.46 +  "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
   20.47    unfolding continuous_within by (rule tendsto_ln)
   20.48  
   20.49  lemma continuous_on_ln [continuous_intros]:
   20.50 -  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
   20.51 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
   20.52    unfolding continuous_on_def by (auto intro: tendsto_ln)
   20.53  
   20.54  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
   20.55 @@ -1992,6 +2005,9 @@
   20.56  lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
   20.57  by(simp add: root_powr_inverse ln_powr)
   20.58  
   20.59 +lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
   20.60 +  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult_commute)
   20.61 +
   20.62  lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
   20.63  by(simp add: log_def ln_root)
   20.64  
   20.65 @@ -2085,30 +2101,30 @@
   20.66  qed
   20.67  
   20.68  lemma tendsto_powr [tendsto_intros]:
   20.69 -  "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
   20.70 +  "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
   20.71    unfolding powr_def by (intro tendsto_intros)
   20.72  
   20.73  lemma continuous_powr:
   20.74    assumes "continuous F f"
   20.75      and "continuous F g"
   20.76 -    and "0 < f (Lim F (\<lambda>x. x))"
   20.77 +    and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
   20.78    shows "continuous F (\<lambda>x. (f x) powr (g x))"
   20.79    using assms unfolding continuous_def by (rule tendsto_powr)
   20.80  
   20.81  lemma continuous_at_within_powr[continuous_intros]:
   20.82    assumes "continuous (at a within s) f"
   20.83      and "continuous (at a within s) g"
   20.84 -    and "0 < f a"
   20.85 +    and "f a \<noteq> 0"
   20.86    shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
   20.87    using assms unfolding continuous_within by (rule tendsto_powr)
   20.88  
   20.89  lemma isCont_powr[continuous_intros, simp]:
   20.90 -  assumes "isCont f a" "isCont g a" "0 < f a"
   20.91 +  assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
   20.92    shows "isCont (\<lambda>x. (f x) powr g x) a"
   20.93    using assms unfolding continuous_at by (rule tendsto_powr)
   20.94  
   20.95  lemma continuous_on_powr[continuous_intros]:
   20.96 -  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
   20.97 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
   20.98    shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
   20.99    using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  20.100  
  20.101 @@ -2150,6 +2166,53 @@
  20.102    show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  20.103  qed
  20.104  
  20.105 +(* it is funny that this isn't in the library! It could go in Transcendental *)
  20.106 +lemma tendsto_exp_limit_at_right:
  20.107 +  fixes x :: real
  20.108 +  shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
  20.109 +proof cases
  20.110 +  assume "x \<noteq> 0"
  20.111 +
  20.112 +  have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
  20.113 +    by (auto intro!: derivative_eq_intros)
  20.114 +  then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
  20.115 +    by (auto simp add: has_field_derivative_def field_has_derivative_at) 
  20.116 +  then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
  20.117 +    by (rule tendsto_intros)
  20.118 +  then show ?thesis
  20.119 +  proof (rule filterlim_mono_eventually)
  20.120 +    show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
  20.121 +      unfolding eventually_at_right[OF zero_less_one]
  20.122 +      using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
  20.123 +  qed (simp_all add: at_eq_sup_left_right)
  20.124 +qed (simp add: tendsto_const)
  20.125 +
  20.126 +lemma tendsto_exp_limit_at_top:
  20.127 +  fixes x :: real
  20.128 +  shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
  20.129 +  apply (subst filterlim_at_top_to_right)
  20.130 +  apply (simp add: inverse_eq_divide)
  20.131 +  apply (rule tendsto_exp_limit_at_right)
  20.132 +  done
  20.133 +
  20.134 +lemma tendsto_exp_limit_sequentially:
  20.135 +  fixes x :: real
  20.136 +  shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
  20.137 +proof (rule filterlim_mono_eventually)
  20.138 +  from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
  20.139 +  hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
  20.140 +    apply (intro eventually_sequentiallyI [of n])
  20.141 +    apply (case_tac "x \<ge> 0")
  20.142 +    apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
  20.143 +    apply (subgoal_tac "x / real xa > -1")
  20.144 +    apply (auto simp add: field_simps)
  20.145 +    done
  20.146 +  then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
  20.147 +    by (rule eventually_elim1) (erule powr_realpow)
  20.148 +  show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
  20.149 +    by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
  20.150 +qed auto
  20.151 +
  20.152  subsection {* Sine and Cosine *}
  20.153  
  20.154  definition sin_coeff :: "nat \<Rightarrow> real" where
  20.155 @@ -2374,6 +2437,31 @@
  20.156    using cos_add [where x=x and y=x]
  20.157    by (simp add: power2_eq_square)
  20.158  
  20.159 +lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
  20.160 +proof -
  20.161 +  let ?f = "\<lambda>x. x - sin x"
  20.162 +  from x have "?f x \<ge> ?f 0"
  20.163 +    apply (rule DERIV_nonneg_imp_nondecreasing)
  20.164 +    apply (intro allI impI exI[of _ "1 - cos x" for x])
  20.165 +    apply (auto intro!: derivative_eq_intros simp: field_simps)
  20.166 +    done
  20.167 +  thus "sin x \<le> x" by simp
  20.168 +qed
  20.169 +
  20.170 +lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
  20.171 +proof -
  20.172 +  let ?f = "\<lambda>x. x + sin x"
  20.173 +  from x have "?f x \<ge> ?f 0"
  20.174 +    apply (rule DERIV_nonneg_imp_nondecreasing)
  20.175 +    apply (intro allI impI exI[of _ "1 + cos x" for x])
  20.176 +    apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
  20.177 +    done
  20.178 +  thus "sin x \<ge> -x" by simp
  20.179 +qed
  20.180 +
  20.181 +lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
  20.182 +  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"]
  20.183 +  by (auto simp: abs_real_def)
  20.184  
  20.185  subsection {* The Constant Pi *}
  20.186