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))"