src/HOL/Probability/Sinc_Integral.thy
 changeset 65578 e4997c181cce parent 63886 685fb01256af child 67977 557ea2740125
1.1 --- a/src/HOL/Probability/Sinc_Integral.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Probability/Sinc_Integral.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -219,12 +219,11 @@
1.4      have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
1.5        by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
1.6           (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
1.7 -    then have **: "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
1.8 +    then have "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
1.9          by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
1.10                   intro!:  mult_mono)
1.11 -
1.12 -    show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
1.13 -      using eventually_ge_at_top[of "1::real"] ** by (auto elim: eventually_mono)
1.14 +    then show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
1.15 +      by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"])
1.16      show "AE x in lborel. 0 < x \<longrightarrow> (?F x \<longlongrightarrow> 0) at_top"
1.17      proof (intro always_eventually impI allI)
1.18        fix x :: real assume "0 < x"