author | paulson <lp15@cam.ac.uk> |
Wed, 17 Jul 2019 14:02:42 +0100 | |
changeset 70365 | 4df0628e8545 |
parent 68613 | 2fae3e01a2ec |
child 70532 | fcf3b891ccb1 |
permissions | -rw-r--r-- |
63329 | 1 |
(* Title: HOL/Probability/Sinc_Integral.thy |
2 |
Authors: Jeremy Avigad (CMU), Luke Serafin (CMU) |
|
3 |
Authors: Johannes Hölzl, TU München |
|
62083 | 4 |
*) |
5 |
||
6 |
section \<open>Integral of sinc\<close> |
|
7 |
||
8 |
theory Sinc_Integral |
|
9 |
imports Distributions |
|
10 |
begin |
|
11 |
||
12 |
subsection \<open>Various preparatory integrals\<close> |
|
13 |
||
14 |
text \<open> Naming convention |
|
15 |
The theorem name consists of the following parts: |
|
63167 | 16 |
\<^item> Kind of integral: \<open>has_bochner_integral\<close> / \<open>integrable\<close> / \<open>LBINT\<close> |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
17 |
\<^item> Interval: Interval (0 / infinity / open / closed) (infinity / open / closed) |
62083 | 18 |
\<^item> Name of the occurring constants: power, exp, m (for minus), scale, sin, $\ldots$ |
19 |
\<close> |
|
20 |
||
21 |
lemma 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) |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
25 |
(auto simp: nn_integral_set_ennreal split: split_indicator) |
62083 | 26 |
|
27 |
lemma 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 |
||
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
33 |
lemma integrable_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> set_integrable lborel {0 <..} (\<lambda>x. exp (-(x * u)))" |
62083 | 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] |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
36 |
by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros set_integrable_def) |
62083 | 37 |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
38 |
lemma LBINT_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> LBINT x=0..\<infinity>. exp (-(x * u)) = 1 / u" |
62083 | 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] |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
41 |
by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty set_lebesgue_integral_def field_simps |
62083 | 42 |
dest!: has_bochner_integral_integral_eq) |
43 |
||
44 |
lemma 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 |
|
48 |
proof (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) |
|
53 |
qed (auto intro: continuous_at_imp_continuous_on) |
|
54 |
||
55 |
lemma LBINT_I0i_exp_mscale_sin: |
|
56 |
assumes "0 < x" |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
57 |
shows "LBINT u=0..\<infinity>. \<bar>exp (-u * x) * sin x\<bar> = \<bar>sin x\<bar> / x" |
62083 | 58 |
proof (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) |
|
71 |
qed auto |
|
72 |
||
73 |
lemma |
|
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" |
|
78 |
proof - |
|
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 |
|
68613 | 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)+ |
|
62083 | 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"]) |
|
68613 | 87 |
(auto intro: derivative_eq_intros 1 2 3 filterlim_tan_at_right |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
88 |
simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def) |
62083 | 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"]) |
|
68613 | 91 |
(auto intro: derivative_eq_intros 1 2 3 filterlim_tan_at_right |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
92 |
simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def) |
62083 | 93 |
qed |
94 |
||
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
95 |
lemma |
62083 | 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" |
|
100 |
proof - |
|
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 |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
108 |
simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def) |
62083 | 109 |
show "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
110 |
unfolding interval_lebesgue_integrable_def |
62083 | 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 |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
113 |
simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def) |
62083 | 114 |
qed |
115 |
||
116 |
section \<open>The sinc function, and the sine integral (Si)\<close> |
|
117 |
||
118 |
abbreviation sinc :: "real \<Rightarrow> real" where |
|
119 |
"sinc \<equiv> (\<lambda>x. if x = 0 then 1 else sin x / x)" |
|
120 |
||
121 |
lemma 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 |
||
124 |
lemma isCont_sinc: "isCont sinc x" |
|
125 |
proof 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) |
|
129 |
next |
|
130 |
assume "x \<noteq> 0" show ?thesis |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62083
diff
changeset
|
131 |
by (rule continuous_transform_within [where d = "abs x" and f = "\<lambda>x. sin x / x"]) |
62083 | 132 |
(auto simp add: dist_real_def \<open>x \<noteq> 0\<close>) |
133 |
qed |
|
134 |
||
135 |
lemma 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 |
||
140 |
lemma borel_measurable_sinc[measurable]: "sinc \<in> borel_measurable borel" |
|
70365
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
68613
diff
changeset
|
141 |
by (intro borel_measurable_continuous_onI continuous_at_imp_continuous_on ballI isCont_sinc) |
62083 | 142 |
|
143 |
lemma sinc_AE: "AE x in lborel. sin x / x = sinc x" |
|
144 |
by (rule AE_I [where N = "{0}"], auto) |
|
145 |
||
146 |
definition Si :: "real \<Rightarrow> real" where "Si t \<equiv> LBINT x=0..t. sin x / x" |
|
147 |
||
148 |
lemma sinc_neg [simp]: "sinc (- x) = sinc x" |
|
149 |
by auto |
|
150 |
||
151 |
(* TODO: Determine whether this can reasonably be eliminated by redefining Si. *) |
|
152 |
lemma Si_alt_def : "Si t = LBINT x=0..t. sinc x" |
|
153 |
proof 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) |
|
157 |
next |
|
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) |
|
162 |
qed |
|
163 |
||
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
164 |
lemma Si_neg: |
62083 | 165 |
assumes "T \<ge> 0" shows "Si (- T) = - Si T" |
166 |
proof - |
|
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]) |
|
177 |
qed |
|
178 |
||
179 |
lemma integrable_sinc': |
|
180 |
"interval_lebesgue_integrable lborel (ereal 0) (ereal T) (\<lambda>t. sin (t * \<theta>) / t)" |
|
181 |
proof - |
|
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) |
|
188 |
qed |
|
189 |
||
190 |
(* TODO: need a better version of FTC2 *) |
|
191 |
lemma DERIV_Si: "(Si has_real_derivative sinc x) (at x)" |
|
192 |
proof - |
|
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 |
|
62390 | 201 |
split del: if_split) |
62083 | 202 |
qed |
203 |
||
204 |
lemma isCont_Si: "isCont Si x" |
|
205 |
using DERIV_Si by (rule DERIV_isCont) |
|
206 |
||
207 |
lemma borel_measurable_Si[measurable]: "Si \<in> borel_measurable borel" |
|
70365
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
68613
diff
changeset
|
208 |
by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_onI) |
62083 | 209 |
|
210 |
lemma 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" |
|
212 |
proof - |
|
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] |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
217 |
by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def) |
62083 | 218 |
|
219 |
have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top" |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
220 |
unfolding set_lebesgue_integral_def |
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
221 |
proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]], |
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
222 |
simp_all del: abs_divide split: split_indicator) |
62083 | 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) |
|
65578
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
63886
diff
changeset
|
226 |
then have "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real |
62083 | 227 |
by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right |
228 |
intro!: mult_mono) |
|
65578
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
63886
diff
changeset
|
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)" |
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
63886
diff
changeset
|
230 |
by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"]) |
62083 | 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" |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
248 |
by (simp add: interval_lebesgue_integral_0_infty set_lebesgue_integral_def) |
62083 | 249 |
qed |
250 |
||
251 |
lemma 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 |
|
255 |
proof |
|
256 |
assume "0 = t" then show ?thesis |
|
257 |
using integrable_I0i_1_div_plus_square by simp |
|
258 |
next |
|
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) |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
265 |
(auto dest!: integrable.intros simp: ac_simps set_integrable_def) |
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
266 |
from lborel_integrable_real_affine[OF this [unfolded set_integrable_def], of t 0] |
62083 | 267 |
show ?thesis |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
268 |
unfolding interval_lebesgue_integral_0_infty set_integrable_def |
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63329
diff
changeset
|
269 |
by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator) |
62083 | 270 |
qed |
271 |
||
272 |
lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top" |
|
273 |
proof - |
|
274 |
have "\<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)))" |
|
63167 | 279 |
unfolding Si_def using \<open>0 \<le> t\<close> |
62083 | 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)))" |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
282 |
using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def) |
62083 | 283 |
also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))" |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
284 |
apply (subst interval_integral_Ioi) |
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
285 |
unfolding set_lebesgue_integral_def by(simp_all add: indicator_times ac_simps ) |
62083 | 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" |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
296 |
have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> = |
62083 | 297 |
LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x" |
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63329
diff
changeset
|
298 |
by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult) |
62083 | 299 |
also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>. exp (- (y * x)))" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
300 |
by (cases "x > 0") |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
301 |
(auto simp: field_simps interval_lebesgue_integral_0_infty set_lebesgue_integral_def split: split_indicator) |
62083 | 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 |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
309 |
moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)" |
62083 | 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 |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
313 |
|
62083 | 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))" |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
317 |
by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator) |
62083 | 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> |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
321 |
by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps |
63886
685fb01256af
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
hoelzl
parents:
63329
diff
changeset
|
322 |
split: split_indicator intro!: Bochner_Integration.integral_cong) |
62083 | 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 |
then show ?thesis |
|
330 |
by (rule Lim_transform_eventually) |
|
331 |
(auto intro!: tendsto_eq_intros Si_at_top_LBINT) |
|
332 |
qed |
|
333 |
||
334 |
subsection \<open>The final theorems: boundedness and scalability\<close> |
|
335 |
||
336 |
lemma bounded_Si: "\<exists>B. \<forall>T. \<bar>Si T\<bar> \<le> B" |
|
337 |
proof - |
|
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) |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
357 |
qed |
62083 | 358 |
|
359 |
lemma 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>)" |
|
362 |
proof - |
|
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" |
|
63167 | 376 |
using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
377 |
by (auto simp: ac_simps set_lebesgue_integral_def) |
62083 | 378 |
} note aux1 = this |
379 |
{ assume "0 > \<theta>" |
|
380 |
have [simp]: "integrable lborel (\<lambda>x. sin (x * \<theta>) * indicator {0<..<T} x / x)" |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
381 |
using integrable_sinc' [of T \<theta>] assms |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
382 |
by (simp add: interval_lebesgue_integrable_def set_integrable_def ac_simps) |
62083 | 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)" |
|
63167 | 395 |
using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def |
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
396 |
by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm) |
62083 | 397 |
} note aux2 = this |
398 |
show ?thesis |
|
67977
557ea2740125
Probability builds with new definitions
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
399 |
using assms unfolding Si_def interval_lebesgue_integral_def set_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def |
68613 | 400 |
by (auto simp: aux1 aux2) |
62083 | 401 |
qed |
402 |
||
403 |
end |