src/HOL/Probability/Sinc_Integral.thy
changeset 67977 557ea2740125
parent 65578 e4997c181cce
child 68613 2fae3e01a2ec
     1.1 --- a/src/HOL/Probability/Sinc_Integral.thy	Thu Apr 12 12:16:34 2018 +0100
     1.2 +++ b/src/HOL/Probability/Sinc_Integral.thy	Fri Apr 13 15:58:27 2018 +0100
     1.3 @@ -33,12 +33,12 @@
     1.4  lemma integrable_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> set_integrable lborel {0 <..} (\<lambda>x. exp (-(x * u)))"
     1.5    using lborel_integrable_real_affine_iff[of u "\<lambda>x. indicator {0 <..} x *\<^sub>R exp (- x)" 0]
     1.6          has_bochner_integral_I0i_power_exp_m[of 0]
     1.7 -  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros)
     1.8 +  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros set_integrable_def)
     1.9  
    1.10  lemma LBINT_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> LBINT x=0..\<infinity>. exp (-(x * u)) = 1 / u"
    1.11    using lborel_integral_real_affine[of u "\<lambda>x. indicator {0<..} x *\<^sub>R exp (- x)" 0]
    1.12          has_bochner_integral_I0i_power_exp_m[of 0]
    1.13 -  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty field_simps
    1.14 +  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty set_lebesgue_integral_def field_simps
    1.15             dest!: has_bochner_integral_integral_eq)
    1.16  
    1.17  lemma LBINT_I0c_exp_mscale_sin:
    1.18 @@ -83,11 +83,11 @@
    1.19    show "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi"
    1.20      by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
    1.21         (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
    1.22 -             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
    1.23 +             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
    1.24    show "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))"
    1.25      by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
    1.26         (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
    1.27 -             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
    1.28 +             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
    1.29  qed
    1.30  
    1.31  lemma
    1.32 @@ -103,12 +103,12 @@
    1.33    show "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2"
    1.34      by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
    1.35         (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
    1.36 -             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
    1.37 +             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
    1.38    show "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))"
    1.39      unfolding interval_lebesgue_integrable_def
    1.40      by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
    1.41         (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
    1.42 -             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
    1.43 +             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
    1.44  qed
    1.45  
    1.46  section \<open>The sinc function, and the sine integral (Si)\<close>
    1.47 @@ -212,10 +212,12 @@
    1.48    have int: "set_integrable lborel {0<..} (\<lambda>x. exp (- x) * (x + 1) :: real)"
    1.49      unfolding distrib_left
    1.50      using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
    1.51 -    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps)
    1.52 +    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
    1.53  
    1.54    have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top"
    1.55 -  proof (rule integral_dominated_convergence_at_top[OF _ _ int], simp_all del: abs_divide split: split_indicator)
    1.56 +    unfolding set_lebesgue_integral_def
    1.57 +  proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]], 
    1.58 +         simp_all del: abs_divide split: split_indicator)
    1.59      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.60        by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
    1.61           (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
    1.62 @@ -241,7 +243,7 @@
    1.63      qed
    1.64    qed
    1.65    then show "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
    1.66 -    by (simp add: interval_lebesgue_integral_0_infty)
    1.67 +    by (simp add: interval_lebesgue_integral_0_infty set_lebesgue_integral_def)
    1.68  qed
    1.69  
    1.70  lemma Si_at_top_integrable:
    1.71 @@ -258,10 +260,10 @@
    1.72    have "set_integrable lborel {0<..} (\<lambda>x. (exp (- x) * x) * (sin t/t) + exp (- x) * cos t)"
    1.73      using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
    1.74      by (intro set_integral_add set_integrable_mult_left)
    1.75 -       (auto dest!: integrable.intros simp: ac_simps)
    1.76 -  from lborel_integrable_real_affine[OF this, of t 0]
    1.77 +       (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
    1.78 +  from lborel_integrable_real_affine[OF this [unfolded set_integrable_def], of t 0]
    1.79    show ?thesis
    1.80 -    unfolding interval_lebesgue_integral_0_infty
    1.81 +    unfolding interval_lebesgue_integral_0_infty set_integrable_def
    1.82      by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
    1.83  qed
    1.84  
    1.85 @@ -275,9 +277,10 @@
    1.86        unfolding Si_def using \<open>0 \<le> t\<close>
    1.87        by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
    1.88      also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))"
    1.89 -      using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac)
    1.90 +      using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def)
    1.91      also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
    1.92 -      by (subst interval_integral_Ioi) (simp_all add: indicator_times ac_simps)
    1.93 +      apply (subst interval_integral_Ioi)
    1.94 +      unfolding set_lebesgue_integral_def  by(simp_all add: indicator_times ac_simps )
    1.95      also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
    1.96      proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
    1.97        show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x))))
    1.98 @@ -293,7 +296,7 @@
    1.99            by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
   1.100          also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>.  exp (- (y * x)))"
   1.101            by (cases "x > 0")
   1.102 -             (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
   1.103 +             (auto simp: field_simps interval_lebesgue_integral_0_infty set_lebesgue_integral_def split: split_indicator)
   1.104          also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (1 / x)"
   1.105            by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
   1.106          also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>"
   1.107 @@ -301,7 +304,7 @@
   1.108          finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
   1.109            by simp
   1.110        qed
   1.111 -      moreover have "set_integrable lborel {0 .. t} (\<lambda>x. abs (sinc x))"
   1.112 +      moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)"
   1.113          by (auto intro!: borel_integrable_compact continuous_intros simp del: real_scaleR_def)
   1.114        ultimately show "integrable lborel (\<lambda>x. LBINT y. norm (?f (x, y)))"
   1.115          by (rule integrable_cong_AE_imp[rotated 2]) simp
   1.116 @@ -309,11 +312,11 @@
   1.117        have "0 < x \<Longrightarrow> set_integrable lborel {0<..} (\<lambda>y. sin x * exp (- (y * x)))" for x :: real
   1.118            by (intro set_integrable_mult_right integrable_I0i_exp_mscale)
   1.119        then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))"
   1.120 -        by (intro AE_I2) (auto simp: indicator_times split: split_indicator)
   1.121 +        by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator)
   1.122      qed
   1.123      also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
   1.124        using \<open>0\<le>t\<close>
   1.125 -      by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
   1.126 +      by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps
   1.127                 split: split_indicator intro!: Bochner_Integration.integral_cong)
   1.128      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.129        by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
   1.130 @@ -369,12 +372,12 @@
   1.131      hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
   1.132          LBINT x. indicator {0<..<T * \<theta>} x * sin x / x"
   1.133        using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
   1.134 -        by (auto simp: ac_simps)
   1.135 +        by (auto simp: ac_simps set_lebesgue_integral_def)
   1.136    } note aux1 = this
   1.137    { assume "0 > \<theta>"
   1.138      have [simp]: "integrable lborel (\<lambda>x. sin (x * \<theta>) * indicator {0<..<T} x / x)"
   1.139        using integrable_sinc' [of T \<theta>] assms
   1.140 -      by (simp add: interval_lebesgue_integrable_def ac_simps)
   1.141 +      by (simp add: interval_lebesgue_integrable_def set_integrable_def ac_simps)
   1.142      have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T. -\<theta> *\<^sub>R sinc (t * -\<theta>))"
   1.143        by (rule interval_integral_discrete_difference[of "{0}"]) auto
   1.144      also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sinc t)"
   1.145 @@ -388,10 +391,10 @@
   1.146      hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
   1.147         - (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
   1.148        using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
   1.149 -        by (auto simp add: field_simps mult_le_0_iff split: if_split_asm)
   1.150 +        by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm)
   1.151    } note aux2 = this
   1.152    show ?thesis
   1.153 -    using assms unfolding Si_def interval_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
   1.154 +    using assms unfolding Si_def interval_lebesgue_integral_def set_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
   1.155      apply auto
   1.156      apply (erule aux1)
   1.157      apply (rule aux2)