1(* Title: HOL/Probability/Sinc_Integral.thy 2 Authors: Jeremy Avigad (CMU), Luke Serafin (CMU) 3 Authors: Johannes H��lzl, TU M��nchen 4*) 5 6section \<open>Integral of sinc\<close> 7 8theory Sinc_Integral 9 imports Distributions 10begin 11 12subsection \<open>Various preparatory integrals\<close> 13 14text \<open> Naming convention 15The theorem name consists of the following parts: 16 \<^item> Kind of integral: \<open>has_bochner_integral\<close> / \<open>integrable\<close> / \<open>LBINT\<close> 17 \<^item> Interval: Interval (0 / infinity / open / closed) (infinity / open / closed) 18 \<^item> Name of the occurring constants: power, exp, m (for minus), scale, sin, $\ldots$ 19\<close> 20 21lemma has_bochner_integral_I0i_power_exp_m': 22 "has_bochner_integral lborel (\<lambda>x. x^k * exp (-x) * indicator {0 ..} x::real) (fact k)" 23 using nn_intergal_power_times_exp_Ici[of k] 24 by (intro has_bochner_integral_nn_integral) 25 (auto simp: nn_integral_set_ennreal split: split_indicator) 26 27lemma has_bochner_integral_I0i_power_exp_m: 28 "has_bochner_integral lborel (\<lambda>x. x^k * exp (-x) * indicator {0 <..} x::real) (fact k)" 29 using AE_lborel_singleton[of 0] 30 by (intro has_bochner_integral_cong_AE[THEN iffD1, OF _ _ _ has_bochner_integral_I0i_power_exp_m']) 31 (auto split: split_indicator) 32 33lemma integrable_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> set_integrable lborel {0 <..} (\<lambda>x. exp (-(x * u)))" 34 using lborel_integrable_real_affine_iff[of u "\<lambda>x. indicator {0 <..} x *\<^sub>R exp (- x)" 0] 35 has_bochner_integral_I0i_power_exp_m[of 0] 36 by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros set_integrable_def) 37 38lemma LBINT_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> LBINT x=0..\<infinity>. exp (-(x * u)) = 1 / u" 39 using lborel_integral_real_affine[of u "\<lambda>x. indicator {0<..} x *\<^sub>R exp (- x)" 0] 40 has_bochner_integral_I0i_power_exp_m[of 0] 41 by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty set_lebesgue_integral_def field_simps 42 dest!: has_bochner_integral_integral_eq) 43 44lemma LBINT_I0c_exp_mscale_sin: 45 "LBINT x=0..t. exp (-(u * x)) * sin x = 46 (1 / (1 + u^2)) * (1 - exp (-(u * t)) * (u * sin t + cos t))" (is "_ = ?F t") 47 unfolding zero_ereal_def 48proof (subst interval_integral_FTC_finite) 49 show "(?F has_vector_derivative exp (- (u * x)) * sin x) (at x within {min 0 t..max 0 t})" for x 50 by (auto intro!: derivative_eq_intros 51 simp: has_field_derivative_iff_has_vector_derivative[symmetric] power2_eq_square) 52 (simp_all add: field_simps add_nonneg_eq_0_iff) 53qed (auto intro: continuous_at_imp_continuous_on) 54 55lemma LBINT_I0i_exp_mscale_sin: 56 assumes "0 < x" 57 shows "LBINT u=0..\<infinity>. \<bar>exp (-u * x) * sin x\<bar> = \<bar>sin x\<bar> / x" 58proof (subst interval_integral_FTC_nonneg) 59 let ?F = "\<lambda>u. 1 / x * (1 - exp (- u * x)) * \<bar>sin x\<bar>" 60 show "\<And>t. (?F has_real_derivative \<bar>exp (- t * x) * sin x\<bar>) (at t)" 61 using \<open>0 < x\<close> by (auto intro!: derivative_eq_intros simp: abs_mult) 62 show "((?F \<circ> real_of_ereal) \<longlongrightarrow> 0) (at_right 0)" 63 using \<open>0 < x\<close> by (auto simp: zero_ereal_def ereal_tendsto_simps intro!: tendsto_eq_intros) 64 have *: "((\<lambda>t. exp (- t * x)) \<longlongrightarrow> 0) at_top" 65 using \<open>0 < x\<close> 66 by (auto intro!: exp_at_bot[THEN filterlim_compose] filterlim_tendsto_pos_mult_at_top filterlim_ident 67 simp: filterlim_uminus_at_bot mult.commute[of _ x]) 68 show "((?F \<circ> real_of_ereal) \<longlongrightarrow> \<bar>sin x\<bar> / x) (at_left \<infinity>)" 69 using \<open>0 < x\<close> unfolding ereal_tendsto_simps 70 by (intro filterlim_compose[OF _ *]) (auto intro!: tendsto_eq_intros filterlim_ident) 71qed auto 72 73lemma 74 shows integrable_inverse_1_plus_square: 75 "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))" 76 and LBINT_inverse_1_plus_square: 77 "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi" 78proof - 79 have 1: "- (pi / 2) < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> (tan has_real_derivative 1 + (tan x)\<^sup>2) (at x)" for x 80 using cos_gt_zero_pi[of x] by (subst tan_sec) (auto intro!: DERIV_tan simp: power_inverse) 81 have 2: "- (pi / 2) < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> isCont (\<lambda>x. 1 + (tan x)\<^sup>2) x" for x 82 using cos_gt_zero_pi[of x] by auto 83 have 3: "\<lbrakk>- (pi / 2) < x; x * 2 < pi\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (1 + x\<^sup>2)) (tan x)" for x 84 by (rule continuous_intros | simp add: add_nonneg_eq_0_iff)+ 85 show "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi" 86 by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"]) 87 (auto intro: derivative_eq_intros 1 2 3 filterlim_tan_at_right 88 simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def) 89 show "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))" 90 by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"]) 91 (auto intro: derivative_eq_intros 1 2 3 filterlim_tan_at_right 92 simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def) 93qed 94 95lemma 96 shows integrable_I0i_1_div_plus_square: 97 "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))" 98 and LBINT_I0i_1_div_plus_square: 99 "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2" 100proof - 101 have 1: "0 < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> (tan has_real_derivative 1 + (tan x)\<^sup>2) (at x)" for x 102 using cos_gt_zero_pi[of x] by (subst tan_sec) (auto intro!: DERIV_tan simp: power_inverse) 103 have 2: "0 < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> isCont (\<lambda>x. 1 + (tan x)\<^sup>2) x" for x 104 using cos_gt_zero_pi[of x] by auto 105 show "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2" 106 by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"]) 107 (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros 108 simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def) 109 show "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))" 110 unfolding interval_lebesgue_integrable_def 111 by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"]) 112 (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros 113 simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def) 114qed 115 116section \<open>The sinc function, and the sine integral (Si)\<close> 117 118abbreviation sinc :: "real \<Rightarrow> real" where 119 "sinc \<equiv> (\<lambda>x. if x = 0 then 1 else sin x / x)" 120 121lemma sinc_at_0: "((\<lambda>x. sin x / x::real) \<longlongrightarrow> 1) (at 0)" 122 using DERIV_sin [of 0] by (auto simp add: has_field_derivative_def field_has_derivative_at) 123 124lemma isCont_sinc: "isCont sinc x" 125proof cases 126 assume "x = 0" then show ?thesis 127 using LIM_equal [where g = "\<lambda>x. sin x / x" and a=0 and f=sinc and l=1] 128 by (auto simp: isCont_def sinc_at_0) 129next 130 assume "x \<noteq> 0" show ?thesis 131 by (rule continuous_transform_within [where d = "abs x" and f = "\<lambda>x. sin x / x"]) 132 (auto simp add: dist_real_def \<open>x \<noteq> 0\<close>) 133qed 134 135lemma continuous_on_sinc[continuous_intros]: 136 "continuous_on S f \<Longrightarrow> continuous_on S (\<lambda>x. sinc (f x))" 137 using continuous_on_compose[of S f sinc, OF _ continuous_at_imp_continuous_on] 138 by (auto simp: isCont_sinc) 139 140lemma borel_measurable_sinc[measurable]: "sinc \<in> borel_measurable borel" 141 by (intro borel_measurable_continuous_onI continuous_at_imp_continuous_on ballI isCont_sinc) 142 143lemma sinc_AE: "AE x in lborel. sin x / x = sinc x" 144 by (rule AE_I [where N = "{0}"], auto) 145 146definition Si :: "real \<Rightarrow> real" where "Si t \<equiv> LBINT x=0..t. sin x / x" 147 148lemma sinc_neg [simp]: "sinc (- x) = sinc x" 149 by auto 150 151(* TODO: Determine whether this can reasonably be eliminated by redefining Si. *) 152lemma Si_alt_def : "Si t = LBINT x=0..t. sinc x" 153proof cases 154 assume "0 \<le> t" then show ?thesis 155 using AE_lborel_singleton[of 0] 156 by (auto simp: Si_def intro!: interval_lebesgue_integral_cong_AE) 157next 158 assume "\<not> 0 \<le> t" then show ?thesis 159 unfolding Si_def using AE_lborel_singleton[of 0] 160 by (subst (1 2) interval_integral_endpoints_reverse) 161 (auto simp: Si_def intro!: interval_lebesgue_integral_cong_AE) 162qed 163 164lemma Si_neg: 165 assumes "T \<ge> 0" shows "Si (- T) = - Si T" 166proof - 167 have "LBINT x=ereal 0..T. -1 *\<^sub>R sinc (- x) = LBINT y= ereal (- 0)..ereal (- T). sinc y" 168 by (rule interval_integral_substitution_finite [OF assms]) 169 (auto intro: derivative_intros continuous_at_imp_continuous_on isCont_sinc) 170 also have "(LBINT x=ereal 0..T. -1 *\<^sub>R sinc (- x)) = -(LBINT x=ereal 0..T. sinc x)" 171 by (subst sinc_neg) (simp_all add: interval_lebesgue_integral_uminus) 172 finally have *: "-(LBINT x=ereal 0..T. sinc x) = LBINT y= ereal 0..ereal (- T). sinc y" 173 by simp 174 show ?thesis 175 using assms unfolding Si_alt_def 176 by (subst zero_ereal_def)+ (auto simp add: * [symmetric]) 177qed 178 179lemma integrable_sinc': 180 "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (\<lambda>t. sin (t * \<theta>) / t)" 181proof - 182 have *: "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (\<lambda>t. \<theta> * sinc (t * \<theta>))" 183 by (intro interval_lebesgue_integrable_mult_right interval_integrable_isCont continuous_within_compose3 [OF isCont_sinc]) 184 auto 185 show ?thesis 186 by (rule interval_lebesgue_integrable_cong_AE[THEN iffD1, OF _ _ _ *]) 187 (insert AE_lborel_singleton[of 0], auto) 188qed 189 190(* TODO: need a better version of FTC2 *) 191lemma DERIV_Si: "(Si has_real_derivative sinc x) (at x)" 192proof - 193 have "(at x within {min 0 (x - 1)..max 0 (x + 1)}) = at x" 194 by (intro at_within_interior) auto 195 moreover have "min 0 (x - 1) \<le> x" "x \<le> max 0 (x + 1)" 196 by auto 197 ultimately show ?thesis 198 using interval_integral_FTC2[of "min 0 (x - 1)" 0 "max 0 (x + 1)" sinc x] 199 by (auto simp: continuous_at_imp_continuous_on isCont_sinc Si_alt_def[abs_def] zero_ereal_def 200 has_field_derivative_iff_has_vector_derivative 201 split del: if_split) 202qed 203 204lemma isCont_Si: "isCont Si x" 205 using DERIV_Si by (rule DERIV_isCont) 206 207lemma borel_measurable_Si[measurable]: "Si \<in> borel_measurable borel" 208 by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_onI) 209 210lemma Si_at_top_LBINT: 211 "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top" 212proof - 213 let ?F = "\<lambda>x t. exp (- (x * t)) * (x * sin t + cos t) / (1 + x\<^sup>2) :: real" 214 have int: "set_integrable lborel {0<..} (\<lambda>x. exp (- x) * (x + 1) :: real)" 215 unfolding distrib_left 216 using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1] 217 by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def) 218 219 have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top" 220 unfolding set_lebesgue_integral_def 221 proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]], 222 simp_all del: abs_divide split: split_indicator) 223 have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real 224 by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono) 225 (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono) 226 then have "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real 227 by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right 228 intro!: mult_mono) 229 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)" 230 by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"]) 231 show "AE x in lborel. 0 < x \<longrightarrow> (?F x \<longlongrightarrow> 0) at_top" 232 proof (intro always_eventually impI allI) 233 fix x :: real assume "0 < x" 234 show "((\<lambda>t. exp (- (x * t)) * (x * sin t + cos t) / (1 + x\<^sup>2)) \<longlongrightarrow> 0) at_top" 235 proof (rule Lim_null_comparison) 236 show "\<forall>\<^sub>F t in at_top. norm (?F x t) \<le> exp (- (x * t)) * (x + 1)" 237 using eventually_ge_at_top[of "1::real"] * \<open>0 < x\<close> 238 by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right 239 intro!: mult_mono elim: eventually_mono) 240 show "((\<lambda>t. exp (- (x * t)) * (x + 1)) \<longlongrightarrow> 0) at_top" 241 by (auto simp: filterlim_uminus_at_top [symmetric] 242 intro!: filterlim_tendsto_pos_mult_at_top[OF tendsto_const] \<open>0<x\<close> filterlim_ident 243 tendsto_mult_left_zero filterlim_compose[OF exp_at_bot]) 244 qed 245 qed 246 qed 247 then show "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top" 248 by (simp add: interval_lebesgue_integral_0_infty set_lebesgue_integral_def) 249qed 250 251lemma Si_at_top_integrable: 252 assumes "t \<ge> 0" 253 shows "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. exp (- (x * t)) * (x * sin t + cos t) / (1 + x\<^sup>2))" 254 using \<open>0 \<le> t\<close> unfolding le_less 255proof 256 assume "0 = t" then show ?thesis 257 using integrable_I0i_1_div_plus_square by simp 258next 259 assume [arith]: "0 < t" 260 have *: "0 \<le> a \<Longrightarrow> 0 < x \<Longrightarrow> a / (1 + x\<^sup>2) \<le> a" for a x :: real 261 using zero_le_power2[of x, arith] using divide_left_mono[of 1 "1+x\<^sup>2" a] by auto 262 have "set_integrable lborel {0<..} (\<lambda>x. (exp (- x) * x) * (sin t/t) + exp (- x) * cos t)" 263 using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1] 264 by (intro set_integral_add set_integrable_mult_left) 265 (auto dest!: integrable.intros simp: ac_simps set_integrable_def) 266 from lborel_integrable_real_affine[OF this [unfolded set_integrable_def], of t 0] 267 show ?thesis 268 unfolding interval_lebesgue_integral_0_infty set_integrable_def 269 by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator) 270qed 271 272lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top" 273proof - 274 have \<dagger>: "\<forall>\<^sub>F t in at_top. pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t" 275 using eventually_ge_at_top[of 0] 276 proof eventually_elim 277 fix t :: real assume "t \<ge> 0" 278 have "Si t = LBINT x=0..t. sin x * (LBINT u=0..\<infinity>. exp (-(u * x)))" 279 unfolding Si_def using \<open>0 \<le> t\<close> 280 by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale) 281 also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))" 282 using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def) 283 also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))" 284 apply (subst interval_integral_Ioi) 285 unfolding set_lebesgue_integral_def by(simp_all add: indicator_times ac_simps ) 286 also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))" 287 proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable) 288 show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))) 289 \<in> borel_measurable (lborel \<Otimes>\<^sub>M lborel)" (is "?f \<in> borel_measurable _") 290 by measurable 291 292 have "AE x in lborel. indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))" 293 using AE_lborel_singleton[of 0] AE_lborel_singleton[of t] 294 proof eventually_elim 295 fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t" 296 have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> = 297 LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x" 298 by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult) 299 also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>. exp (- (y * x)))" 300 by (cases "x > 0") 301 (auto simp: field_simps interval_lebesgue_integral_0_infty set_lebesgue_integral_def split: split_indicator) 302 also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (1 / x)" 303 by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale) 304 also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>" 305 using x by (simp add: field_simps split: split_indicator) 306 finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))" 307 by simp 308 qed 309 moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)" 310 by (auto intro!: borel_integrable_compact continuous_intros simp del: real_scaleR_def) 311 ultimately show "integrable lborel (\<lambda>x. LBINT y. norm (?f (x, y)))" 312 by (rule integrable_cong_AE_imp[rotated 2]) simp 313 314 have "0 < x \<Longrightarrow> set_integrable lborel {0<..} (\<lambda>y. sin x * exp (- (y * x)))" for x :: real 315 by (intro set_integrable_mult_right integrable_I0i_exp_mscale) 316 then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))" 317 by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator) 318 qed 319 also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)" 320 using \<open>0\<le>t\<close> 321 by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps 322 split: split_indicator intro!: Bochner_Integration.integral_cong) 323 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))" 324 by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong) 325 also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))" 326 using Si_at_top_integrable[OF \<open>0\<le>t\<close>] by (simp add: integrable_I0i_1_div_plus_square LBINT_I0i_1_div_plus_square) 327 finally show "pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t" .. 328 qed 329 show ?thesis 330 by (rule Lim_transform_eventually [OF _ \<dagger>]) 331 (auto intro!: tendsto_eq_intros Si_at_top_LBINT) 332qed 333 334subsection \<open>The final theorems: boundedness and scalability\<close> 335 336lemma bounded_Si: "\<exists>B. \<forall>T. \<bar>Si T\<bar> \<le> B" 337proof - 338 have *: "0 \<le> y \<Longrightarrow> dist x y < z \<Longrightarrow> abs x \<le> y + z" for x y z :: real 339 by (simp add: dist_real_def) 340 341 have "eventually (\<lambda>T. dist (Si T) (pi / 2) < 1) at_top" 342 using Si_at_top by (elim tendstoD) simp 343 then have "eventually (\<lambda>T. 0 \<le> T \<and> \<bar>Si T\<bar> \<le> pi / 2 + 1) at_top" 344 using eventually_ge_at_top[of 0] by eventually_elim (insert *[of "pi/2" "Si _" 1], auto) 345 then have "\<exists>T. 0 \<le> T \<and> (\<forall>t \<ge> T. \<bar>Si t\<bar> \<le> pi / 2 + 1)" 346 by (auto simp add: eventually_at_top_linorder) 347 then obtain T where T: "0 \<le> T" "\<And>t. t \<ge> T \<Longrightarrow> \<bar>Si t\<bar> \<le> pi / 2 + 1" 348 by auto 349 moreover have "t \<le> - T \<Longrightarrow> \<bar>Si t\<bar> \<le> pi / 2 + 1" for t 350 using T(1) T(2)[of "-t"] Si_neg[of "- t"] by simp 351 moreover have "\<exists>M. \<forall>t. -T \<le> t \<and> t \<le> T \<longrightarrow> \<bar>Si t\<bar> \<le> M" 352 by (rule isCont_bounded) (auto intro!: isCont_Si continuous_intros \<open>0 \<le> T\<close>) 353 then obtain M where M: "\<And>t. -T \<le> t \<and> t \<le> T \<Longrightarrow> \<bar>Si t\<bar> \<le> M" 354 by auto 355 ultimately show ?thesis 356 by (intro exI[of _ "max M (pi/2 + 1)"]) (meson le_max_iff_disj linorder_not_le order_le_less) 357qed 358 359lemma LBINT_I0c_sin_scale_divide: 360 assumes "T \<ge> 0" 361 shows "LBINT t=0..T. sin (t * \<theta>) / t = sgn \<theta> * Si (T * \<bar>\<theta>\<bar>)" 362proof - 363 { assume "0 < \<theta>" 364 have "(LBINT t=ereal 0..T. sin (t * \<theta>) / t) = (LBINT t=ereal 0..T. \<theta> *\<^sub>R sinc (t * \<theta>))" 365 by (rule interval_integral_discrete_difference[of "{0}"]) auto 366 also have "\<dots> = (LBINT t=ereal (0 * \<theta>)..T * \<theta>. sinc t)" 367 apply (rule interval_integral_substitution_finite [OF assms]) 368 apply (subst mult.commute, rule DERIV_subset) 369 by (auto intro!: derivative_intros continuous_at_imp_continuous_on isCont_sinc) 370 also have "\<dots> = (LBINT t=ereal (0 * \<theta>)..T * \<theta>. sin t / t)" 371 by (rule interval_integral_discrete_difference[of "{0}"]) auto 372 finally have "(LBINT t=ereal 0..T. sin (t * \<theta>) / t) = (LBINT t=ereal 0..T * \<theta>. sin t / t)" 373 by simp 374 hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x = 375 LBINT x. indicator {0<..<T * \<theta>} x * sin x / x" 376 using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def 377 by (auto simp: ac_simps set_lebesgue_integral_def) 378 } note aux1 = this 379 { assume "0 > \<theta>" 380 have [simp]: "integrable lborel (\<lambda>x. sin (x * \<theta>) * indicator {0<..<T} x / x)" 381 using integrable_sinc' [of T \<theta>] assms 382 by (simp add: interval_lebesgue_integrable_def set_integrable_def ac_simps) 383 have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T. -\<theta> *\<^sub>R sinc (t * -\<theta>))" 384 by (rule interval_integral_discrete_difference[of "{0}"]) auto 385 also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sinc t)" 386 apply (rule interval_integral_substitution_finite [OF assms]) 387 apply (subst mult.commute, rule DERIV_subset) 388 by (auto intro!: derivative_intros continuous_at_imp_continuous_on isCont_sinc) 389 also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sin t / t)" 390 by (rule interval_integral_discrete_difference[of "{0}"]) auto 391 finally have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T * -\<theta>. sin t / t)" 392 by simp 393 hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x = 394 - (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)" 395 using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def 396 by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm) 397 } note aux2 = this 398 show ?thesis 399 using assms unfolding Si_def interval_lebesgue_integral_def set_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def 400 by (auto simp: aux1 aux2) 401qed 402 403end 404