author paulson Wed, 11 Jul 2018 09:47:09 +0100 changeset 68613 2fae3e01a2ec parent 68612 ffc3fd6c7498 child 68614 3cb44b0abc5c
patched a continuity proof
```--- a/src/HOL/Probability/Sinc_Integral.thy	Wed Jul 11 09:14:21 2018 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy	Wed Jul 11 09:47:09 2018 +0100
@@ -80,13 +80,15 @@
using cos_gt_zero_pi[of x] by (subst tan_sec) (auto intro!: DERIV_tan simp: power_inverse)
have 2: "- (pi / 2) < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> isCont (\<lambda>x. 1 + (tan x)\<^sup>2) x" for x
using cos_gt_zero_pi[of x] by auto
+  have 3: "\<lbrakk>- (pi / 2) < x; x * 2 < pi\<rbrakk>  \<Longrightarrow> isCont (\<lambda>x. inverse (1 + x\<^sup>2)) (tan x)" for x
show "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi"
by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
-       (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
+       (auto intro: derivative_eq_intros 1 2 3 filterlim_tan_at_right
show "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))"
by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
-       (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
+       (auto intro: derivative_eq_intros 1 2 3 filterlim_tan_at_right
qed

@@ -395,11 +397,7 @@
} note aux2 = this
show ?thesis
using assms unfolding Si_def interval_lebesgue_integral_def set_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
-    apply auto
-    apply (erule aux1)
-    apply (rule aux2)
-    apply auto
-    done
+    by (auto simp: aux1 aux2)
qed

end```