src/HOL/Probability/Sinc_Integral.thy
 changeset 63886 685fb01256af parent 63329 6b26c378ab35 child 65578 e4997c181cce
```     1.1 --- a/src/HOL/Probability/Sinc_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
1.2 +++ b/src/HOL/Probability/Sinc_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
1.3 @@ -263,7 +263,7 @@
1.4    from lborel_integrable_real_affine[OF this, of t 0]
1.5    show ?thesis
1.6      unfolding interval_lebesgue_integral_0_infty
1.7 -    by (rule integrable_bound) (auto simp: field_simps * split: split_indicator)
1.8 +    by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
1.9  qed
1.10
1.11  lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top"
1.12 @@ -291,7 +291,7 @@
1.13          fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t"
1.14          have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> =
1.15              LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
1.16 -          by (intro integral_cong) (auto split: split_indicator simp: abs_mult)
1.17 +          by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
1.18          also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>.  exp (- (y * x)))"
1.19            by (cases "x > 0")
1.20               (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
1.21 @@ -315,7 +315,7 @@
1.22      also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
1.23        using \<open>0\<le>t\<close>
1.24        by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
1.25 -               split: split_indicator intro!: integral_cong)
1.26 +               split: split_indicator intro!: Bochner_Integration.integral_cong)
1.27      also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
1.28        by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
1.29      also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"
```