Theory Bessel_Hankel_Integral
section ‹A Hankel-style integral formula for the Bessel $I$ function›
theory Bessel_Hankel_Integral
imports
"Bessel.Bessel"
"Path_Automation.Path_Automation"
"Prime_Number_Theorem.Prime_Number_Theorem_Library"
"Incomplete_Gamma.More_Beta"
begin
hide_fact (open) Zeta_Library.has_absolute_integral_change_of_variables_1'
subsection ‹Auxiliary integrals›
text ‹
Later on, we will need the integral
\[
\int_{-\infty}^\infty (c^2 + t^2)^{-a}\,\text{d}t =
\frac{1}{2} c^{1-2a} B(\frac{1}{2}, a-\frac{1}{2})
\]
for $c > 0$, $a > \frac{1}{2}$. We first show the $\int_0^\infty$ version. To this end,
we perform the substitution $x = (t/c)^2$ to get
\[\frac{1}{2}c^{1-2e} \int_0^\infty x^{-\frac{1}{2}} (1+x)^{-e} \,\text{d}x\ ,\]
which is one of the various equivalent integral definitions of the Beta function.
›
lemma Bessel_I_aux_integral1:
fixes c e :: real
assumes c: "c > 0" and e: "e > 1/2"
shows "(λt. (c⇧2 + t⇧2) powr -e) absolutely_integrable_on {0<..}"
"integral {0<..} (λt. (c⇧2 + t⇧2) powr -e) = c powr (1 - 2 * e) / 2 * Beta (1/2) (e - 1/2)"
proof -
define C where "C = c powr (1-2*e) / 2"
define f where "f = (λx. C * (x powr (-1/2) / (1 + x) powr e))"
define g where "g = (λx. (x / c) ^ 2)"
define g' where "g' = (λx. 2 * x / c ^ 2)"
define h where "h = (λx. (c⇧2 + x⇧2) powr (-e))"
define I where "I = c powr (1-2*e) / 2 * Beta (1/2) (e - 1/2)"
have bij: "bij_betw g {0<..} {0<..}"
by (rule bij_betwI[of _ _ _ "λy. sqrt y * c"]) (use c in ‹auto simp: g_def›)
have eq: "¦g' x¦ *⇩R f (g x) = h x" if x: "x > 0" for x
proof -
have "¦g' x¦ *⇩R f (g x) = c powr (-2 * e) * (c ^ 2) powr e / (c⇧2 + x⇧2) powr e" using x c
by (auto simp: g'_def f_def g_def field_simps powr_divide powr_minus
powr_half_sqrt power2_eq_square C_def powr_diff)
also have "(c ^ 2) powr e = c powr (2*e)"
by (subst powr_powr [symmetric]) (use c in simp_all)
also have "c powr (-2 * e) * … = 1"
by (subst powr_add [symmetric]) (use c in auto)
finally show ?thesis
by (simp add: powr_minus field_simps h_def)
qed
have "(f has_integral I) {0<..}"
using has_integral_mult_right[OF has_integral_Beta_0_infinity_real[of "1/2" "e - 1/2"], of C] e
by (simp add: f_def I_def C_def)
hence "f absolutely_integrable_on {0<..} ∧ integral {0<..} f = I"
using c by (simp add: f_def has_integral_iff absolutely_integrable_on_iff_nonneg C_def)
also have "{0<..} = g ` {0<..}"
using bij by (simp add: bij_betw_def)
also have "f absolutely_integrable_on g ` {0<..} ∧ integral (g ` {0<..}) f = I ⟷
(λx. ¦g' x¦ * f (g x)) absolutely_integrable_on {0<..} ∧
integral {0<..} (λx. ¦g' x¦ * f (g x)) = I"
by (subst (2) eq_commute, intro has_absolute_integral_change_of_variables_1')
(use c bij in ‹auto simp: g_def g'_def power2_eq_square bij_betw_def
intro!: derivative_eq_intros›)
also have "(λx. ¦g' x¦ * f (g x)) absolutely_integrable_on {0<..} ⟷
h absolutely_integrable_on {0<..}"
by (rule set_integrable_cong) (use eq in auto)
also have "integral {0<..} (λx. ¦g' x¦ * f (g x)) = integral {0<..} h"
by (rule integral_cong) (use eq in auto)
finally show "h absolutely_integrable_on {0<..}" "integral {0<..} h = I"
by (simp_all add: h_def)
qed
text ‹
The $\int_{-\infty}^\infty$ version then easily follows by symmetry.
›
lemma Bessel_I_aux_integral2:
fixes c e :: real
assumes c: "c > 0" and e: "e > 1/2"
shows "integrable lebesgue (λt. (c⇧2 + t⇧2) powr -e)"
and "lebesgue_integral lebesgue (λt. (c⇧2 + t⇧2) powr -e) = c powr (1-2*e) * Beta (1/2) (e - 1/2)"
proof -
define I where "I = c powr (1-2*e) / 2 * Beta (1/2) (e - 1/2)"
have integrable: "(λt. (c⇧2 + t⇧2) powr -e) absolutely_integrable_on {0<..}"
and integral: "integral {0<..} (λt. (c⇧2 + t⇧2) powr -e) = I"
using Bessel_I_aux_integral1[of c e] c e by (simp_all add: I_def)
show integrable': "integrable lebesgue (λt. (c⇧2 + t⇧2) powr -e)"
proof -
have "(λt. (c⇧2 + t⇧2) powr -e) absolutely_integrable_on {..<0}"
using lebesgue_integrable_real_affine_iff[of "-1" "λt. indicator {0<..} t * (c⇧2 + t⇧2) powr -e" 0]
integrable unfolding set_integrable_def by (simp add: indicator_def)
hence "(λt. (c⇧2 + t⇧2) powr -e) absolutely_integrable_on ({0<..} ∪ {..<0} ∪ {0})"
by (intro set_integrable_Un integrable) (auto intro: absolutely_integrable_negligible)
also have "({0<..} ∪ {..<0} ∪ {0}) = (UNIV :: real set)"
by auto
finally show ?thesis
by (simp add: set_integrable_def)
qed
show "lebesgue_integral lebesgue (λt. (c⇧2 + t⇧2) powr -e) = c powr (1-2*e) * Beta (1/2) (e - 1/2)"
proof -
have integrable'': "set_integrable lebesgue UNIV (λt. (c⇧2 + t⇧2) powr -e)"
using integrable' by (simp add: set_integrable_def)
have "I = integral {0<..} (λt. (c⇧2 + t⇧2) powr -e)"
using integral by simp
also have "… = (LINT t:{0<..}|lebesgue. (c⇧2 + t⇧2) powr -e)"
using integrable by (rule set_lebesgue_integral_eq_integral(2) [symmetric])
finally have *: "(LINT t:{0<..}|lebesgue. (c⇧2 + t⇧2) powr -e) = I" ..
have **: "(LINT t:{..<0}|lebesgue. (c⇧2 + t⇧2) powr -e) = I"
unfolding set_lebesgue_integral_def
by (subst lebesgue_integral_real_affine[of "-1" _ 0])
(use * in ‹simp_all add: set_lebesgue_integral_def indicator_def›)
have "(LINT t|lebesgue. (c⇧2 + t⇧2) powr -e) = (LINT t:-{0}|lebesgue. (c⇧2 + t⇧2) powr -e)"
unfolding set_lebesgue_integral_def
proof (rule integral_cong_AE)
have "AE x in lebesgue. x ≠ 0"
by (metis AE_completion_iff AE_lborel_singleton)
thus "AE x in lebesgue. (c⇧2 + x⇧2) powr -e = indicator (-{0}) x *⇩R (c⇧2 + x⇧2) powr -e"
by eventually_elim (auto simp: indicator_def)
qed (auto intro!: measurable_completion)
also have "-{0} = {0<..} ∪ {..<0::real}"
by auto
also have "(LINT x:({0<..} ∪ {..<0::real})|lebesgue. (c⇧2 + x⇧2) powr -e) =
(LINT x:{0<..}|lebesgue. (c⇧2 + x⇧2) powr -e) + (LINT x:{..<0}|lebesgue. (c⇧2 + x⇧2) powr -e)"
by (rule set_integral_Un) (auto intro!: set_integrable_subset[OF integrable''])
also have "… = 2 * I"
using * ** by simp
finally show ?thesis
by (simp add: I_def)
qed
qed
subsection ‹A Hankel-style representation for $1/\Gamma(s)$›
text ‹
The biggest piece of work in this section will be to derive the following Hankel-style contour
integral formula for $\Gamma$:
\[
\frac{1}{\Gamma(s)} = \frac{1}{2\pi i} \int_{c-i\infty}^{c+i\infty}e^z z^{-s}\,\text{d}z
\]
For $\text{Re}(s)>1$, the integral clearly converges absolutely as a Lebesgue integral.
For $\text{Re}(s)\in (0,1]$ it has to be interpreted as a Cauchy principal value, i.e.\
$\int_{c-i\infty}^{c+i\infty} = \lim_{T\to\infty}\int_{c-iT}^{c+IT}$.
We first show the existence of the integral as a Lebesgue integral if $\text{Re}(s) > 1$. This
is fairly easy to see by a comparison test, since it is $O(|t|^{-\text{Re}(s)})$ uniformly
for all $t$.
›
lemma rGamma_hankel_integrable:
assumes c: "c > 0" and s: "Re s > 1"
shows "((λz. exp z * z powr (-s)) ∘ (λt. Complex c t)) absolutely_integrable_on UNIV"
proof -
have *: "((λz. exp z * z powr (-s)) ∘ (λt. Complex c (a*t))) absolutely_integrable_on {1..}"
if [simp]: "¦a¦ = 1" for a :: real
proof (rule set_integrable_bound)
have "AE t in lebesgue. t ≠ 0"
by (simp add: AE_completion_iff AE_lborel_singleton)
thus "AE t∈{1..} in lebesgue. norm (((λz. exp z * z powr (-s)) ∘ (λt. Complex c (a*t))) t) ≤
norm (exp c * exp (pi * ¦Im s¦) * ¦t¦ powr -Re s)"
proof eventually_elim
case (elim t)
have "norm (exp (Complex c (a*t)) * Complex c (a*t) powr - s) =
exp c * norm (Complex c (a*t)) powr -Re s * exp (Im s * Arg (Complex c (a*t)))"
using c by (simp add: norm_mult norm_exp norm_powr_complex)
also have "… ≤ exp c * ¦t¦ powr -Re s * exp (¦Im s¦ * pi)"
proof (intro mult_mono)
show "norm (Complex c (a*t)) powr -Re s ≤ ¦t¦ powr -Re s"
by (rule powr_mono2')
(use s elim abs_Im_le_cmod[of "Complex c (a*t)"] in ‹auto simp: abs_mult›)
next
have "Im s * Arg (Complex c (a*t)) ≤ ¦Im s * Arg (Complex c (a*t))¦"
by linarith
also have "… ≤ ¦Im s¦ * pi"
unfolding abs_mult using Arg_bounded[of "Complex c (a*t)"] by (auto intro!: mult_left_mono)
finally show "exp (Im s * Arg (Complex c (a*t))) ≤ exp (¦Im s¦ * pi)"
by simp
qed auto
finally show ?case
by (auto simp: mult_ac)
qed
next
have "(λx. x powr -Re s) absolutely_integrable_on {1<..}"
using s set_integrable_powr_at_top[of 1 0 "-Re s"] by simp
hence "(λx. x powr -Re s) integrable_on {1<..}"
using set_lebesgue_integral_eq_integral(1) by blast
also have "?this ⟷ (λx. x powr -Re s) integrable_on {1..}"
proof (rule integrable_spike_set_eq)
have "negligible {1::real}"
by simp
also have "… = sym_diff {1<..} {1..}"
by auto
finally show "negligible (sym_diff {1<..} {1..} :: real set)" .
qed
finally have "(λx. exp c * exp (pi * ¦Im s¦) * x powr - Re s) integrable_on {1..}"
by (rule integrable_on_mult_right)
also have "?this ⟷ (λx. exp c * exp (pi * ¦Im s¦) * ¦x¦ powr - Re s) integrable_on {1..}"
by (rule integrable_cong) auto
finally show "(λx. exp c * exp (pi * ¦Im s¦) * ¦x¦ powr - Re s) absolutely_integrable_on {1..}"
by (rule nonnegative_absolutely_integrable_1) auto
qed (auto simp: set_borel_measurable_def Complex_eq intro!: measurable_completion)
have "integrable lebesgue (λt. indicator {1..} t *⇩R (((λz. exp z * z powr (-s)) ∘ (λt. Complex c (-t))) t))"
using *[of "-1"] by (simp add: set_integrable_def)
from lebesgue_integrable_real_affine[OF this, of "-1" 0]
have "((λz. exp z * z powr (-s)) ∘ (λt. Complex c t)) absolutely_integrable_on {..-1}"
unfolding set_integrable_def by (simp add: indicator_def)
moreover have "((λz. exp z * z powr (-s)) ∘ (λt. Complex c t)) absolutely_integrable_on {1..}"
using *[of 1] by simp
moreover have "((λz. exp z * z powr (-s)) ∘ (λt. Complex c t)) absolutely_integrable_on {-1..1}"
by (rule absolutely_integrable_continuous_real)
(use c in ‹auto intro!: continuous_intros simp: complex_eq_iff›)
ultimately have "((λz. exp z * z powr (-s)) ∘ (λt. Complex c t)) absolutely_integrable_on
({-1..1} ∪ {1..} ∪ {..-1})"
by (intro set_integrable_Un) auto
also have "{-1..1} ∪ {1..} ∪ {..-1::real} = UNIV"
by auto
finally show ?thesis .
qed
text ‹
Next, we show the actual integral formula in the case that $\text{Re}(s) > 0$.
The proof works is modelled after Lemma~2.3 by Kong and Teo~\<^cite>‹kong_teo› and goes roughly
like this:
▪ We consider the Hankel-style integration contour sketched in Figure~\ref{fig:contour}.
▪ Since two of the horizontal lines lie directly on the branch cut, this integral is very
awkward to handle. We instead only consider the part of the contour in the upper half plane,
adding a horizontal line on the positive real axis to connect the part we cut off,
and then also move the branch cut out of the way to the negative real axis by using the
alternative branch of the logarithm $\widehat{\ln} z = \ln (-iz) + \tfrac{1}{2}i\pi$.
▪ We apply the Cauchy integral theorem to this contour and note that the integrand has no
singularities inside, so its value must be 0.
▪ We do the same for the portion of the contour that is in the lower half of the complex plane
and add the two values, noting that the horizontal lines we added cancel out.
To save some work, we note that we can get this result for the lower half plane from that
for the upper half plane (which we already have) by complex conjugation due to the fact that
the integrand is symmetric under conjugation.
▪ Denote the vertical integral at $\text{Re}(z) = c$ as $\text{lhs}(T,s)$ and the sum of
the other ones as $\text{rhs}(r,T,s)$. The above shows that
$\text{lhs}(T,s) = \text{rhs}(r,T,s)$ holds for all $s$ with $\text{Re}(s) > 0$.
▪ This immediately means that the value of $\text{rhs}(r,T,s)$ is actually independent of $r$.
▪ Note also that $\lim_{T\to\infty} \text{rhs}(r,T,s)$ exists for any $s$ with
$\text{Re}(s) > 0$, and of course this limit is also independent of $r$.
Write $\text{RHS}(r,s)$ for this limit. In particular, this already shows that
$\text{lhs}(T,s)$ also has a limit for $T\to\infty$ and its value is $\text{RHS}(r,s)$.
▪ In fact, $\text{RHS}(r,s)$ can be expressed in terms of the incomplete Gamma function
$\Gamma(1-s,r)$ and some error terms corresponding to the small circle around the origin.
▪ Thus, if $\text{Re}(s) < 1$, we can let $r\to 0$ and find that the error terms in
$\text{RHS}(r,s)$ vanish and $\lim_{r\to 0} \Gamma(1-s,r) = \Gamma(1-s)$. Together with the
reflection formula for $\Gamma$, we obtain $\text{RHS}(s) = 2\pi/\Gamma(s)$,
exactly as we wanted. This establishes the result we wanted in the strip
$0 < \text{Re}(s) < 1$.
▪ Moreover, both $\Gamma(1-s,r)$ and the error terms and other factors occurring in
$\text{RHS}(r,s)$ are holomorphic functions in $s$ for $\text{Re}(s) > 0$, so we can use
analytic continuation to lift the above equality to all $s$ with $\text{Re}(s) > 0$
and we are done.
\begin{figure}[t]
\begin{center}
\begin{tikzpicture}[>=Latex, thick]
% ---- colors matching the five contour pieces ----
\definecolor{myblue}{HTML}{378ADD} % Lv
\definecolor{myteal}{HTML}{1D9E75} % Cb
\definecolor{mycoral}{HTML}{D85A30} % Lh
\definecolor{myamber}{HTML}{BA7517} % Cs
\definecolor{mypink}{HTML}{D4537E} % Lh'
% ---- illustrative values: c, y, r ----
\coordinate (A) at (1.5,0); % c
\coordinate (B) at (1.5,4.5); % c+iy
\coordinate (C) at (-4.5,4.5); % -y+iy
\coordinate (D) at (-4.5,0); % -y
\coordinate (E) at (-0.6,0); % -r
\coordinate (F) at (0.6,0); % r
\coordinate (O) at (0,0); % origin (excluded)
% ---- axes ----
\draw[->, gray, line width=0.4pt] (-5.8,0) -- (3,0);
\draw[->, gray, line width=0.4pt] (0,-0.6) -- (0,5.1);
% ---- contour segments, in order ----
\draw[myblue, ->] (A) -- node [midway, right] {\color{myblue} $L_v$} (B); % Lv
\draw[myteal, ->] (B) -- (C); % Cb (top)
\draw[myteal, ->] (C) -- node [midway, right] {\color{myteal} $C_b$} (D); % Cb (left side)
\draw[mycoral, ->] (D) -- node [midway, above] {\color{mycoral} $L_h$} (E); % Lh
\draw[myamber, ->] (E) arc (180:0:0.6) node [midway, above left] {\color{myamber} $C_s$}; % Cs, semicircle over 0
\draw[mypink, ->] (F) -- node [midway, above] {\color{mypink} $L_h'$} (A); % Lh'
% ---- vertices ----
\foreach \p in {A,B,C,D,E,F} \fill (\p) circle (1.6pt);
% ---- point labels ----
\node[below] at (A) {$\mathstrut c$};
\node[above] at (B) {$\mathstrut c+iy$};
\node[above] at (C) {$\mathstrut -y+iy$};
\node[below] at (D) {$\mathstrut -y$};
\node[below] at (E) {$\mathstrut -r$};
\node[below] at (F) {$\mathstrut r$};
\end{tikzpicture}
\end{center}
\caption{The Hankel-style integration contour used in the proof of the
$\int_{c-i\infty}^{c+i\infty}$-style integral representation for $1/\Gamma(s)$.}
\label{fig:contour}
\end{figure}
›
theorem rGamma_hankel_strong:
assumes c: "c > 0" and s: "Re s > 0"
shows "((λT. integral {-T..T} ((λz. exp z * z powr (-s)) ∘ (λt. Complex c t)))
⤏ (2 * of_real pi * rGamma s)) at_top"
proof -
define A where "A = {z. Re z = 0 ∧ Im z ≤ 0}"
define Ln' where "Ln' ≡ (λz. ln (-𝗂 * z) + 𝗂 * pi / 2)"
have [holomorphic_intros]: "Ln' holomorphic_on X" if "X ∩ A = {}" for X
unfolding Ln'_def using that
by (auto intro!: holomorphic_intros simp: A_def complex_nonpos_Reals_iff)
have [analytic_intros]: "Ln' analytic_on X" if "X ∩ A = {}" for X
unfolding Ln'_def using that
by (auto intro!: analytic_intros simp: A_def complex_nonpos_Reals_iff)
have Ln'_of_real_pos: "Ln' (of_real x) = of_real (ln x)" if "x > 0" for x
proof -
have "Ln' (of_real x) = Ln (of_real x * (-𝗂)) + 𝗂 * pi / 2"
by (simp add: Ln'_def mult_ac)
also have "… = of_real (ln x)" using that
by (subst Ln_times_of_real) (auto simp: Ln_of_real)
finally show ?thesis .
qed
have Ln'_of_real_neg: "Ln' (of_real x) = of_real (ln (-x)) + 𝗂 * pi" if "x < 0" for x
proof -
have "Ln' (of_real x) = Ln (of_real (-x) * 𝗂) + 𝗂 * pi / 2"
by (simp add: Ln'_def mult_ac)
also have "… = of_real (ln (-x)) + 𝗂 * pi" using that
by (subst Ln_times_of_real) (auto simp: Ln_Reals_eq)
finally show ?thesis .
qed
have Ln'_eq_Ln: "Ln' z = Ln z" if z: "z ≠ 0" "Im z ≥ 0" for z
proof -
have "0 ≤ Im (Ln z)" "Im (Ln z) ≤ pi"
using z Im_Ln_pos_le[of z] by auto
moreover from this have "Im (Ln z) > -pi/2"
using pi_gt_zero by linarith
ultimately show ?thesis
unfolding Ln'_def using z
by (subst Ln_times_simple) auto
qed
define f where "f = (λs z. exp z * z powr (-s) :: complex)"
define fr where "fr = (λs z. exp z * complex_of_real z powr (-s))"
define g where "g = (λs z. exp (z - s * Ln' z))"
define h :: "complex ⇒ real ⇒ complex"
where "h = (λs t. exp (of_real t - s * of_real (ln (-t))))"
define Lv :: "real ⇒ real ⇒ complex" where "Lv = (λy. linepath (of_real c) (Complex c y))"
define Lh :: "real ⇒ real ⇒ real ⇒ complex"
where "Lh = (λr y. linepath (-of_real y) (-of_real r))"
define Lh' :: "real ⇒ real ⇒ complex"
where "Lh' = (λr. linepath (of_real r) (of_real c))"
define Cb :: "real ⇒ real ⇒ complex"
where "Cb = (λy. linepath (Complex c y) (Complex (-y) y) +++ linepath (Complex (-y) y) (-of_real y))"
define Cs :: "real ⇒ real ⇒ complex"
where "Cs = (λr. part_circlepath 0 r pi 0)"
define err1 where "err1 = (λs y. contour_integral (Cb y) (g s))"
define err2 where "err2 = (λs r. contour_integral (Cs r) (g s))"
have "pathstart (Lv y) = of_real c" "pathfinish (Lv y) = Complex c y" for y
by (auto simp: Lv_def)
have "pathstart (Cb y) = Complex c y" "pathfinish (Cb y) = of_real (-y)" for y
by (auto simp: Cb_def complex_eq_iff Im_exp Re_exp)
have path_image_Cb: "z ∉ A" if z: "z ∈ path_image (Cb T)" and T: "T > c" for z T
using that T c by (auto simp: A_def Cb_def path_image_join closed_segment_same_Re closed_segment_same_Im)
have path_image_Cs: "z ∉ A" if z: "z ∈ path_image (Cs r)" and r: "r > 0" for z r
proof
assume "z ∈ A"
have "z ∈ path_image (part_circlepath 0 r 0 pi)"
using z unfolding Cs_def by (metis reversepath_part_circlepath path_image_reversepath)
then obtain t where t: "z = rcis r t" "t ∈ {0..pi}"
by (auto simp: path_image_part_circlepath rcis_def cis_conv_exp)
with ‹z ∈ A› and r have "cos t = 0"
by (auto simp: A_def t(1))
with t(2) have "t = pi / 2"
by (metis arccos_0 arccos_cos atLeastAtMost_iff)
with t(2) and ‹z ∈ A› and r show False
by (auto simp: t(1) A_def)
qed
text ‹
The horizontal line integral on the left half of the real axis can be extended to infinity
for any $s$ due to the exponential decay of the integrand.
›
have integrable: "set_integrable lborel {r..} (λt. h s (-t))" if r: "r > 0" for r s
using absolutely_integrable_incomplete_Gamma[of r s] r
by (simp add: h_def set_integrable_def integrable_completion)
text ‹
We first consider a ``half-Hankel'' contour consisting only of the half of the Hankel
contour lying in the upper half plane.
›
define γ where "γ = (λr y. Lv y +++ Cb y +++ Lh r y +++ Cs r +++ Lh' r)"
have γ: "valid_path (γ r y)" "pathfinish (γ r y) = pathstart (γ r y)"
if "y ≥ c" "r ≥ 0" for r y using that c
by (auto simp: γ_def Lv_def Lh_def Cb_def Cs_def Lh'_def A_def complex_eq_iff Re_exp Im_exp
path_image_join closed_segment_same_Re closed_segment_same_Im
closed_segment_eq_real_ivl intro!: valid_path_join)
have path_image_γ: "path_image (γ r T) ⊆ -A"
if "T > c" "r > 0" "r < c" for r T
using path_image_Cs[of _ r] path_image_Cb[of _ T] that
by (auto simp: γ_def Cs_def Cb_def Lv_def Lh_def Lh'_def path_image_join
closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl A_def)
text ‹
Applying Cauchy's theorem to this contour, we obtain a term relating the horizontal
integral on the real axis with the vertical one, modulo some error terms.
›
have 1: "𝗂 * integral {0..y} (λx. f s (Complex c x)) + integral {-y..-r} (fr s) =
-(integral {r..c} (fr s) + err1 s y + err2 s r)"
if yr: "y > c" "r > 0" "r < c" for s :: complex and r y :: real
proof -
have "(g s has_contour_integral 0) (γ r y)"
proof (rule Cauchy_theorem_simply_connected)
show "open (-A)"
proof -
have "closed ({z. Re z = 0} ∩ {z. Im z ≤ 0})"
by (intro closed_Int closed_halfspace_Re_eq closed_halfspace_Im_le)
also have "… = A"
by (auto simp: A_def)
finally show ?thesis
by auto
qed
next
show "simply_connected (-A)"
proof (rule simply_connected_retraction_gen)
show "simply_connected (-complex_of_real ` {..0})"
by (rule simply_connected_slotted_complex_plane_left)
next
show "continuous_on (-A) (λz. -𝗂 * z)" "continuous_on (-complex_of_real ` {..0}) (λz. 𝗂 * z)"
by (auto intro!: continuous_intros)
next
have "bij_betw (λz. 𝗂 * z) (- complex_of_real ` {..0}) (-A)"
by (rule bij_betwI[of _ _ _ "λz. -𝗂 * z"]) (auto simp: A_def complex_eq_iff)
thus "(*) 𝗂 ` (- complex_of_real ` {..0}) = - A"
by (simp add: bij_betw_def)
qed (auto simp: complex_eq_iff A_def)
next
show "g s holomorphic_on -A"
by (auto simp: g_def intro!: holomorphic_intros)
qed (use γ[of y r] path_image_γ[of y r] yr in simp_all)
hence "contour_integral (γ r y) (g s) = 0"
using contour_integral_unique by blast
also have "contour_integral (γ r y) (g s) =
contour_integral (Lv y) (g s) + contour_integral (Cb y) (g s) +
contour_integral (Lh r y) (g s) + contour_integral (Cs r) (g s) +
contour_integral (Lh' r) (g s)"
unfolding γ_def
proof path
show "g s analytic_on path_image (Lv y +++ Cb y +++ Lh r y +++ Cs r +++ Lh' r)"
proof (rule analytic_on_subset)
show "path_image (Lv y +++ Cb y +++ Lh r y +++ Cs r +++ Lh' r) ⊆ -A"
using path_image_Cb[of _ y] path_image_Cs[of _ r] yr c
unfolding Lv_def Cb_def Lh_def Cs_def Lh'_def
by (fastforce simp: path_image_join A_def closed_segment_same_Re closed_segment_same_Im
closed_segment_eq_real_ivl)
qed (auto intro!: analytic_intros simp: g_def)
qed (auto simp: Cs_def Lh'_def Lh_def Cb_def Lv_def)
also have "contour_integral (Lh r y) (g s) = integral {-y..-r} (λx. g s (of_real x))"
unfolding Lh_def by (subst contour_integral_linepath_Reals_eq) (use yr c in simp_all)
also have "… = integral {-y..-r} (fr s)"
unfolding g_def fr_def using c yr
by (intro integral_cong)
(auto simp: Ln'_of_real_neg powr_def Ln_of_real' field_simps exp_diff exp_minus exp_add)
also have "contour_integral (Lh' r) (g s) = integral {r..c} (λx. g s (of_real x))"
unfolding Lh'_def by (subst contour_integral_linepath_Reals_eq) (use yr c in simp_all)
also have "… = integral {r..c} (fr s)"
unfolding g_def fr_def using c yr
by (intro integral_cong)
(auto simp: Ln'_of_real_pos powr_def Ln_of_real' field_simps exp_diff exp_minus exp_add)
also have "contour_integral (Lv y) (g s) = 𝗂 * integral {0..y} (λx. g s (Complex c x))"
unfolding Lv_def by (rule contour_integral_linepath_same_Re) (use yr in auto)
also have "integral {0..y} (λx. g s (Complex c x)) = integral {0..y} (λx. f s (Complex c x))"
unfolding g_def f_def
by (intro integral_cong, subst Ln'_eq_Ln)
(use c in ‹auto simp: g_def powr_def field_simps exp_diff exp_minus exp_add complex_eq_iff›)
finally show ?thesis
unfolding err1_def err2_def by (Groebner_Basis.algebra)
qed
text ‹
We combine this result with a flipped copy of itself to get the full Hankel contour.
One of the error terms, namely the horizontal line along the positive real axis, cancels.
›
have 2: "integral {-y..y} (λt. f s (Complex c t)) =
2 * sin (pi * s) * (CLBINT t=r..y. h s (-t)) -
𝗂 * (cnj (err1 (cnj s) y) + cnj (err2 (cnj s) r) - err2 s r - err1 s y)"
if yr: "y > c + r" "r > 0" "r < c" for s :: complex and y r :: real
proof -
have "𝗂 * integral {0..y} (λx. f s (Complex c x)) + integral {-y..-r} (fr s) -
cnj (𝗂 * integral {0..y} (λx. f (cnj s) (Complex c x)) + integral {-y..-r} (fr (cnj s))) =
-(integral {r..c} (fr s) + err1 s y + err2 s r) -
cnj (-(integral {r..c} (fr (cnj s)) + err1 (cnj s) y + err2 (cnj s) r))"
by (subst (1 2) 1) (use yr in auto)
also have "cnj (-(integral {r..c} (fr (cnj s)) + err1 (cnj s) y + err2 (cnj s) r)) =
-integral {r..c} (λx. cnj (fr (cnj s) x)) - cnj (err1 (cnj s) y) - cnj (err2 (cnj s) r)"
by (simp add: integral_cnj)
also have "integral {r..c} (λx. cnj (fr (cnj s) x)) = integral {r..c} (fr s)"
by (intro integral_cong) (use c yr in ‹auto simp: exp_cnj fr_def cnj_powr›)
also have "-(integral {r..c} (fr s) + err1 s y + err2 s r) -
(-… - cnj (err1 (cnj s) y) - cnj (err2 (cnj s) r)) =
cnj (err1 (cnj s) y) + cnj (err2 (cnj s) r) - err2 s r - err1 s y"
by simp
also have "cnj (𝗂 * integral {0..y} (λx. f (cnj s) (Complex c x)) + integral {-y..-r} (fr (cnj s))) =
integral {-y..-r} (λx. cnj (fr (cnj s) x)) -
𝗂 * integral {0..y} (λx. cnj (f (cnj s) (Complex c x)))"
by (simp add: integral_cnj)
also have "𝗂 * integral {0..y} (λx. f s (Complex c x)) + integral {-y..-r} (fr s) - … =
𝗂 * (integral {0..y} (λx. cnj (f (cnj s) (Complex c x))) + integral {0..y} (λx. f s (Complex c x))) +
(integral {-y..-r} (fr s) - integral {-y..-r} (λx. cnj (fr (cnj s) x)))"
by (Groebner_Basis.algebra)
also have "integral {-y..-r} (fr s) =
integral {-y..-r} (λt. exp (t - s * complex_of_real (ln (-t)) - 𝗂 * s * pi))"
by (intro integral_cong)
(use yr in ‹auto simp: fr_def powr_def exp_cnj Ln_of_real' ring_distribs exp_diff
exp_minus exp_add field_simps simp flip: of_real_minus›)
also have "integral {-y..-r} (λx. cnj (fr (cnj s) x)) =
integral {-y..-r} (λt. exp (t - s * complex_of_real (ln (-t)) + 𝗂 * s * pi))"
by (intro integral_cong)
(use yr in ‹auto simp: fr_def powr_def exp_cnj Ln_of_real' ring_distribs exp_diff
exp_minus exp_add field_simps simp flip: of_real_minus›)
also have "integral {-y..-r} (λt. exp (t - s * complex_of_real (ln (-t)) - 𝗂 * s * pi)) - … =
integral {-y..-r} (λt. exp (t - s * complex_of_real (ln (-t)) - 𝗂 * s * pi) -
exp (t - s * complex_of_real (ln (-t)) + 𝗂 * s * pi))"
by (rule integral_diff [symmetric]; rule integrable_continuous_interval)
(use yr c in ‹auto intro!: continuous_intros simp: fr_def›)
also have "(λt. exp (t - s * complex_of_real (ln (-t)) - 𝗂 * s * pi) -
exp (t - s * complex_of_real (ln (-t)) + 𝗂 * s * pi)) =
(λt. exp (t - s * complex_of_real (ln (-t))) * (exp (-𝗂 * s * pi) - exp (𝗂 * s * pi)))"
by (simp add: exp_diff exp_add exp_minus field_simps)
also have "… = (λt. -2 * 𝗂 * sin (pi * s) * h s t)"
by (simp add: h_def sin_exp_eq algebra_simps add_divide_distrib diff_divide_distrib)
also have "integral {-y..-r} … = -2 * 𝗂 * sin (pi * s) * integral {-y..-r} (h s)"
unfolding h_def by (rule integral_mult_right)
also have "integral {-y..-r} (h s) = integral {r..y} (λt. h s (-t))"
by (subst Henstock_Kurzweil_Integration.integral_reflect_real [symmetric]) auto
also have "… = (CLBINT t=r..y. h s (-t))"
by (intro interval_integral_eq_integral [symmetric] borel_integrable_atLeastAtMost')
(use yr in ‹auto simp: h_def complex_eq_iff intro!: continuous_intros›)
also have "integral {0..y} (λx. cnj (f (cnj s) (Complex c x))) =
integral {-y..0} (λx. cnj (f (cnj s) (Complex c (-x))))"
by (subst Henstock_Kurzweil_Integration.integral_reflect_real [symmetric]) simp_all
also have "… = integral {-y..0} (λx. f s (Complex c x))"
using c yr by (intro integral_cong) (auto simp: f_def exp_cnj cnj_powr complex_cnj)
also have "integral {-y..0} (λx. f s (Complex c x)) + integral {0..y} (λx. f s (Complex c x)) =
integral {-y..y} (λx. f s (Complex c x))"
by (intro Henstock_Kurzweil_Integration.integral_combine integrable_continuous_real)
(use yr in ‹auto intro!: continuous_intros simp: f_def complex_eq_iff›)
finally show ?thesis using power2_i
by (Groebner_Basis.algebra)
qed
text ‹
The four error terms vanish under diffrent preconditions: some only for
$\text{Re}(s) > 0$ and some for $\text{Re}(s) < 1$.
›
have lim_err1: "(err1 s ⤏ 0) at_top" if s: "Re s > 0" for s
proof (rule Lim_null_comparison)
define C1 where "C1 = exp (c + pi * ¦Im s¦)"
define C2 where "C2 = exp (pi * ¦Im s¦)"
show "eventually (λT. norm (err1 s T) ≤ C1 * T powr (-Re s) + C2 * exp (-T) * T powr (-Re s) * T) at_top"
using eventually_gt_at_top[of c]
proof eventually_elim
case (elim T)
define err1_1 where "err1_1 = contour_integral (linepath (Complex c T) (Complex (-T) T)) (g s)"
define err1_2 where "err1_2 = contour_integral (linepath (Complex (- T) T) (-of_real T)) (g s)"
have "err1 s T = err1_1 + err1_2"
unfolding err1_def err1_1_def err1_2_def Cb_def g_def using path_image_Cb[of _ T] elim
by (subst contour_integral_join)
(auto intro!: analytic_imp_contour_integrable analytic_intros
simp: A_def Cb_def path_image_join)
also have "norm … ≤ norm err1_1 + norm err1_2"
by norm
also have "err1_1 = -contour_integral (linepath (Complex (-T) T) (Complex c T)) (g s)"
unfolding err1_1_def using contour_integral_reversepath by fastforce
also have "norm … = norm (integral {-T..c} (λx. g s (of_real x + of_real T * 𝗂)))"
using elim c by (subst contour_integral_linepath_same_Im) auto
also have "… ≤ T powr (-Re s) * exp (¦Im s¦ * pi) * (exp c - exp (-T))"
proof (rule integral_norm_bound_integral')
fix t assume t: "t ∈ {-T..c}"
define z where "z = (of_real t + of_real T * 𝗂)"
have "z ≠ 0"
using c elim by (auto simp: complex_eq_iff z_def)
hence "g s z = f s z" using t elim
unfolding f_def g_def powr_def
by (subst Ln'_eq_Ln) (auto simp: z_def exp_diff exp_minus field_simps)
also have "norm … = exp t * (norm z) powr (-Re s) * exp (Im s * Arg z)"
by (simp add: z_def f_def norm_mult norm_powr_complex)
also have "… ≤ exp t * T powr (-Re s) * exp (¦Im s¦ * pi)"
proof (intro mult_mono powr_mono2')
have "T = Im z"
by (auto simp: z_def)
also have "… ≤ norm z"
using abs_Im_le_cmod[of z] by simp
finally show "T ≤ norm z" .
next
have "Im s * Arg z ≤ ¦Im s * Arg z¦"
by linarith
also have "… ≤ ¦Im s¦ * pi"
unfolding abs_mult using Arg_bounded[of z] by (intro mult_left_mono) auto
finally show "exp (Im s * Arg z) ≤ exp (¦Im s¦ * pi)"
by simp
qed (use s elim c in auto)
also have "… = T powr (-Re s) * exp (¦Im s¦ * pi) * exp t"
by (simp add: C1_def algebra_simps)
finally show "norm (g s z) ≤ T powr (-Re s) * exp (¦Im s¦ * pi) * exp t" .
next
have "((λx. T powr (-Re s) * exp (¦Im s¦ * pi) * exp x) has_integral
(T powr (-Re s) * exp (¦Im s¦ * pi) * exp c -
T powr (-Re s) * exp (¦Im s¦ * pi) * exp (-T))) {-T..c}" using elim c
by (intro fundamental_theorem_of_calculus)
(auto simp flip: has_real_derivative_iff_has_vector_derivative
intro!: derivative_eq_intros)
thus "((λx. T powr (-Re s) * exp (¦Im s¦ * pi) * exp x) has_integral
(T powr (-Re s) * exp (¦Im s¦ * pi) * (exp c - exp (-T)))) {-T..c}"
by (simp add: algebra_simps)
qed (auto simp: g_def Ln'_def intro!: measurable_completion borel_measurable_if_D)
also have "… ≤ C1 * T powr (-Re s)"
by (simp add: C1_def algebra_simps exp_add)
also have "norm err1_2 ≤ C2 * exp (-T) * T powr (-Re s) * norm (-of_real T - Complex (-T) T)"
unfolding err1_2_def
proof (rule contour_integral_bound_linepath)
show "g s contour_integrable_on linepath (Complex (- T) T) (-of_real T)" using c elim
by (auto intro!: analytic_imp_contour_integrable analytic_intros
simp: g_def A_def Cb_def path_image_join closed_segment_same_Re)
next
fix z assume "z ∈ closed_segment (Complex (-T) T) (-complex_of_real T)"
then obtain t where t: "t ∈ {0..T}" "z = Complex (-T) t"
using c elim by (auto simp: closed_segment_same_Re closed_segment_eq_real_ivl complex_eq_iff)
have "z ≠ 0"
using c elim by (auto simp: complex_eq_iff t(2))
hence "g s z = f s z" using t elim
unfolding f_def g_def powr_def
by (subst Ln'_eq_Ln) (auto simp: t(2) exp_diff exp_minus field_simps)
also have "norm (f s z) = exp (-T) * (norm z) powr (-Re s) * exp (Im s * Arg z)"
by (simp add: f_def norm_mult t(2) norm_powr_complex)
also have "… ≤ exp (-T) * T powr (-Re s) * exp (¦Im s¦ *pi)"
proof (intro mult_mono powr_mono2')
from c elim have "T = ¦Re z¦"
by (auto simp: t)
also have "… ≤ norm z"
using abs_Re_le_cmod[of z] by simp
finally show "T ≤ norm z" .
next
have "Im s * Arg z ≤ ¦Im s * Arg z¦"
by linarith
also have "… ≤ ¦Im s¦ * pi"
unfolding abs_mult using Arg_bounded[of z] by (intro mult_left_mono) auto
finally show "exp (Im s * Arg z) ≤ exp (¦Im s¦ * pi)"
by simp
qed (use c elim s in auto)
finally show "norm (g s z) ≤ C2 * exp (-T) * T powr (-Re s)"
by (simp add: C2_def algebra_simps)
qed (auto simp: C2_def)
also have "norm (-of_real T - Complex (-T) T) = T"
using elim c by (simp add: cmod_def)
finally show ?case
by simp_all
qed
show "((λT. C1 * T powr (-Re s) + C2 * exp (-T) * T powr (-Re s) * T) ⤏ 0) at_top"
using s by real_asymp
qed
have lim_err2: "(err2 s ⤏ 0) (at_right 0)" if s: "Re s < 1" for s
proof (rule Lim_null_comparison)
define C where "C = pi * exp (c + ¦Im s¦ * pi)"
have "eventually (λr::real. r > 0) (at_right 0)"
"eventually (λr::real. r < c) (at_right 0)"
using c by real_asymp+
thus "eventually (λr. norm (err2 s r) ≤ C * r powr (1 - Re s)) (at_right 0)"
proof eventually_elim
case (elim r)
have "norm (err2 s r) ≤ exp c * r powr - Re s * exp (¦Im s¦ * pi) * r * ¦0 - pi¦"
unfolding err2_def Cs_def
proof (rule contour_integral_bound_part_circlepath)
show "g s contour_integrable_on part_circlepath 0 r pi 0"
using path_image_Cs[of _ r] elim unfolding g_def Cs_def
by (auto intro!: analytic_imp_contour_integrable analytic_intros simp: A_def)
next
show "norm (g s z) ≤ exp c * r powr - Re s * exp (¦Im s¦ * pi)"
if z: "z ∈ path_image (part_circlepath 0 r pi 0)" for z
proof -
have "z ∈ path_image (part_circlepath 0 r 0 pi)"
using z by (metis reversepath_part_circlepath path_image_reversepath)
then obtain t where t: "z = rcis r t" "t ∈ {0..pi}"
by (auto simp: path_image_part_circlepath rcis_def cis_conv_exp)
have "g s z = f s z" unfolding g_def f_def using t(2) elim
by (subst Ln'_eq_Ln)
(auto simp: t(1) exp_diff powr_def exp_minus field_simps sin_ge_zero)
also have "norm (f s z) = exp (r * cos t) * r powr -Re s * exp (Im s * Arg z)"
using elim t by (simp add: t f_def norm_mult norm_powr_complex Arg_rcis)
also have "… ≤ exp c * r powr -Re s * exp (¦Im s¦ * pi)"
proof (intro mult_mono)
have "r * cos t ≤ r * 1"
by (rule mult_left_mono) (use elim in auto)
also have "… ≤ c"
using elim by simp
finally show "exp (r * cos t) ≤ exp c"
by simp
next
have "Im s * Arg z ≤ ¦Im s * Arg z¦"
by linarith
also have "… ≤ ¦Im s¦ * pi"
unfolding abs_mult using Arg_bounded[of z] by (intro mult_left_mono) auto
finally show "exp (Im s * Arg z) ≤ exp (¦Im s¦ * pi)"
by simp
qed (use elim in auto)
finally show "norm (g s z) ≤ exp c * r powr (-Re s) * exp (¦Im s¦ * pi)" .
qed
qed (use elim in auto)
also have "exp c * r powr (-Re s) * exp (¦Im s¦ * pi) * r * ¦0 - pi¦ = C * r powr (1-Re s)"
using elim by (auto simp: C_def powr_diff powr_minus field_simps exp_add)
finally show "norm (err2 s r) ≤ C * r powr (1 - Re s)" .
qed
show "((λr. C * r powr (1 - Re s)) ⤏ 0) (at_right 0)"
using s by real_asymp
qed
text ‹
We now arbitrarily pick some suitable radius (we will soon see that all the values are
independent of it anyway).
›
define r where "r = c / 2"
have r: "r > 0" "r < c"
using c by (auto simp: r_def)
define lhs where "lhs = (λs T. integral {-T..T} (λt. f s (Complex c t)))"
define rhs where "rhs = (λs r T. 2 * sin (complex_of_real pi * s) * (CLBINT t=r..T. h s (-t)) -
𝗂 * (cnj (err1 (cnj s) T) + cnj (err2 (cnj s) r) -
err2 s r - err1 s T))"
define RHS where "RHS = (λs r. 2 * sin (complex_of_real pi * s) * (CLBINT t:{r..}. h s (- t)) +
𝗂 * (err2 s r - cnj (err2 (cnj s) r)))"
text ‹
For $\text{Re}(s) > 0$, we now let $T\to\infty$ and let two of the error terms vanish.
What we obtain from this is that the vertical integral we are interested in (\<^term>‹lhs›)
converges to a slightly deformed version of the horizontal integrals we want (\<^term>‹RHS›).
The deformation is the small circle around the origin to avoid the singularity there.
›
have lim_lhs: "(lhs s ⤏ RHS s r) at_top"
if r: "r > 0" "r < c" and s: "Re s > 0" for s :: complex and r :: real
proof -
have "(rhs s r ⤏ 2 * sin (pi * s) *
(CLBINT t:{r..}. h s (-t)) - 𝗂 * (cnj 0 + cnj (err2 (cnj s) r) - err2 s r - 0)) at_top"
unfolding rhs_def
proof (intro tendsto_intros lim_err1 lim_err2)
have "((λx. set_lebesgue_integral lborel {r..x} (λt. h s (-t))) ⤏
set_lebesgue_integral lborel {r..} (λt. h s (-t))) at_top"
proof (rule tendsto_set_lebesgue_integral_at_top)
show "set_integrable lborel {r..} (λt. h s (- t))"
by (rule integrable) (use r in auto)
qed auto
moreover have "eventually (λx. set_lebesgue_integral lborel {r..x} (λt. h s (-t)) =
(CLBINT t=ereal r..ereal x. h s (-t))) at_top"
using eventually_ge_at_top[of r] by eventually_elim (simp_all add: interval_integral_Icc)
ultimately have *: "((λx. (CLBINT t=ereal r..ereal x. h s (-t))) ⤏
set_lebesgue_integral lborel {r..} (λt. h s (-t))) at_top"
by (rule Lim_transform_eventually)
show "((λx. CLBINT t=ereal r..ereal x. h s (- t)) ⤏
CLBINT t:{r..}. h s (- t)) at_top"
by (rule filterlim_compose[OF *]) real_asymp
qed (use s in auto)
hence "(rhs s r ⤏ 2 * sin (pi * s) * (CLBINT t:{r..}. h s (-t)) +
𝗂 * (err2 s r - cnj (err2 (cnj s) r))) at_top"
by (simp add: algebra_simps)
moreover have "eventually (λT. lhs s T = rhs s r T) at_top"
proof -
have "eventually (λT. c + r < T) at_top"
by real_asymp
thus ?thesis
proof eventually_elim
case (elim T)
thus ?case using 2[of r T s] r
by (simp add: lhs_def rhs_def)
qed
qed
ultimately show "(lhs s ⤏ RHS s r) at_top"
using filterlim_cong unfolding RHS_def by blast
qed
text ‹
Next, we show that \<^term>‹RHS s r› is equal to $2\pi/\Gamma(s)$ for all $s$ with $\text{Re}(s)<1$,
independently of the radius $r$.
›
have RHS_eq: "RHS s r = 2 * pi * rGamma s" if s: "Re s ∈ {0<..<1}" for s :: complex
proof -
have "((λr. LBINT t. indicator {r..} t * h s (-t)) ⤏
(LBINT t. indicator {0..} t * h s (-t))) (at_right 0)"
proof (rule tendsto_at_right_sequentially)
show "0 < (1::real)"
by simp
next
fix l :: "nat ⇒ real"
assume l: "l ⇢ 0" "⋀n. l n > 0"
show "(λx. LBINT t. indicator {l x..} t * h s (-t)) ⇢ (LBINT t. indicator {0..} t * h s (-t))"
proof (rule integral_dominated_convergence)
have "integrable lebesgue (λt. norm (indicator {0<..} t * complex_of_real t powr (-s) / of_real (exp t)))"
by (intro integrable_norm)
(use absolutely_integrable_Gamma_integral'[of "1-s"] s
in ‹simp_all add: set_integrable_def scaleR_conv_of_real of_real_indicator›)
hence "integrable lborel (λt. norm (indicator {0<..} t * complex_of_real t powr (-s) / of_real (exp t)))"
by (subst (asm) integrable_completion) auto
also have "?this ⟷ integrable lborel (λt. indicator {0<..} t * norm (h s (-t)))"
by (intro Bochner_Integration.integrable_cong)
(auto simp: norm_mult indicator_def norm_divide h_def powr_def field_simps exp_diff exp_minus)
finally show "integrable lborel (λt. indicator {0<..} t * norm (h s (-t)))" .
next
show "AE t in lborel. norm (indicator {l n..} t * h s (- t))
≤ indicat_real {0<..} t * cmod (h s (- t))" for n
using l(2)[of n] by (intro always_eventually) (auto simp: indicator_def)
next
have "AE t in lborel. t ≠ 0"
by (metis AE_lborel_singleton)
thus "AE t in lborel. (λn. indicator {l n..} t * h s (-t)) ⇢ indicator {0..} t * h s (-t)"
proof eventually_elim
case (elim t)
show ?case
proof (cases "t > 0")
case True
hence "eventually (λn. l n < t) at_top"
using l(1) order_tendsto_iff by blast
hence "eventually (λn. indicator {l n..} t * h s (-t) =
indicator {0..} t * h s (-t)) sequentially"
by eventually_elim (use True in auto)
thus ?thesis
by (metis tendsto_eventually)
next
case False
hence "indicator {l n..} t * h s (-t) = indicator {0..} t * h s (-t)" for n
using l(2)[of n] elim by (auto simp: indicator_def)
thus ?thesis
by fastforce
qed
qed
qed (auto simp: h_def)
qed
hence lim_integral: "((λr. CLBINT t:{r..}. h s (- t)) ⤏ CLBINT t:{0..}. h s (-t)) (at_right 0)"
by (simp add: set_lebesgue_integral_def scaleR_conv_of_real of_real_indicator)
text ‹
For $r\to 0$, the integral in \<^term>‹RHS s r› becomes the integral over the entire positive
real line. This integral is also exactly the one from the definition of $\Gamma$.
›
have "filterlim (λr. RHS s r)
(nhds (2 * sin (pi * s) * (CLBINT t:{0..}. h s (-t)) + 𝗂 * (0 - cnj 0))) (at_right 0)"
unfolding RHS_def by (intro tendsto_intros lim_err2 lim_integral) (use s in auto)
hence "filterlim (λr. RHS s r) (nhds (2 * sin (pi * s) * (CLBINT t:{0..}. h s (-t)))) (at_right 0)"
by simp
text ‹
Moreover, since ‹lhs s T› is independent of $r$ but also tends to ‹RHS s r› for $T\to\infty$
for any $r$, we know that the value of ‹RHS s r› is actually also independent of $r$ (at least
for sufficiently small $r$).
›
moreover have "eventually (λr'::real. r' > 0) (at_right 0)" "eventually (λr'. r' < c) (at_right 0)"
using c by real_asymp+
hence "eventually (λr'. RHS s r' = RHS s r) (at_right 0)"
proof eventually_elim
case (elim r')
have "(lhs s ⤏ RHS s r') at_top"
by (rule lim_lhs) (use elim s in auto)
moreover have "(lhs s ⤏ RHS s r) at_top"
by (rule lim_lhs) (use r s in auto)
ultimately show "RHS s r' = RHS s r"
using tendsto_unique trivial_limit_at_top_linorder by blast
qed
ultimately have "filterlim (λr'. RHS s r)
(nhds (2 * sin (pi * s) * (CLBINT t:{0..}. h s (-t)))) (at_right (0::real))"
by (rule Lim_transform_eventually)
hence "RHS s r = 2 * sin (pi * s) * (CLBINT t:{0..}. h s (-t))"
by (simp add: tendsto_const_iff)
text ‹
All that remains now is some massaging of terms and using the definition of the Gamma function
as well as the reflection identity.
›
also have "(CLBINT t:{0..}. h s (-t)) = (CLBINT t:{0<..}. of_real t powr (-s) / of_real (exp t))"
unfolding set_lebesgue_integral_def
proof (intro integral_cong_AE)
have "AE t in lborel. t ≠ (0::real)"
using AE_lborel_singleton by blast
thus "AE t in lborel. indicator {0..} t *⇩R h s (-t) =
indicator {0<..} t *⇩R (of_real t powr -s / of_real (exp t))"
by eventually_elim
(auto simp: powr_def h_def exp_add exp_diff exp_minus field_simps
Ln_of_real exp_of_real indicator_def)
qed (auto simp: h_def)
also have "… = integral {0<..} (λt. of_real t powr (-s) / of_real (exp t))"
by (rule set_borel_integral_eq_integral(2))
(use absolutely_integrable_Gamma_integral'[of "1-s"] s
in ‹simp_all add: set_integrable_def integrable_completion›)
also have "… = Gamma (1-s)"
using Gamma_integral_complex'[of "1-s"] s by (simp add: has_integral_iff)
also have "2 * sin (pi * s) * Gamma (1 - s) = 2 * pi * rGamma s * (Gamma (1 - s) * rGamma (1 - s))"
using rGamma_reflection_complex[of s] by (simp add: field_simps)
also have "1 - s ∉ ℤ⇩≤⇩0"
using s by (auto elim!: nonpos_Ints_cases simp: complex_eq_iff)
hence "Gamma (1 - s) * rGamma (1 - s) = 1"
by (simp add: rGamma_inverse_Gamma field_simps Gamma_eq_zero_iff)
finally show "RHS s r = 2 * pi * rGamma s"
by simp
qed
text ‹
Also, for any $r > 0$, the term \<^term>‹RHS s r› defines a holomorphic function on the half-plane
with $\text{Re}(s) > 0$.
›
have RHS_holo: "(λs. RHS s r) holomorphic_on {s. Re s > 0}"
proof -
have "(λz. err2 z r) = (λz. -contour_integral (part_circlepath 0 r 0 pi) (g z))"
unfolding err2_def Cs_def by (metis contour_integral_part_circlepath_reverse)
also have "… = (λz. -integral {0..pi} (λt. 𝗂 * g z (rcis r t) * rcis r t))"
by (subst contour_integral_part_circlepath_eq) (simp_all add: mult_ac rcis_def)
finally have err2_eq: "err2 z r = -integral (cbox 0 pi) (λt. 𝗂 * g z (rcis r t) * rcis r t)" for z
by (auto simp: fun_eq_iff)
define err2' where
"err2' = (λa b s. integral {a..b} (λt. 𝗂 * exp (rcis r t - s * Complex (ln r) t) * rcis r t))"
have err2'_holomorphic: "err2' a b holomorphic_on {s. Re s > 0}" for a b
proof -
define l where "l = (λs t. 𝗂 * exp (rcis r t + (1 - s) * Complex (ln r) t))"
define l' where "l' = (λs t. -𝗂 * exp (rcis r t + (1 - s) * Complex (ln r) t) * Complex (ln r) t)"
have "(λs. integral (cbox a b) (l s)) holomorphic_on {s. Re s > 0}"
proof (rule leibniz_rule_holomorphic)
show "((λs. l s t) has_field_derivative l' s t) (at s within {s. Re s > 0})"
if s: "s ∈ {s. Re s > 0}" and t: "t ∈ cbox a b" for s t
unfolding l_def l'_def by (auto intro!: derivative_eq_intros)
next
show "l s integrable_on cbox a b" if "s ∈ {s. Re s > 0}" for s
unfolding l_def by (intro integrable_continuous continuous_intros)
next
show "continuous_on ({s. 0 < Re s} × cbox a b) (λ(s, t). l' s t)"
unfolding l'_def case_prod_unfold by (auto intro!: continuous_intros)
qed (auto simp: convex_halfspace_Re_gt)
also have "(λs. integral (cbox a b) (l s)) = err2' a b"
unfolding err2'_def cbox_interval using r
by (intro ext integral_cong)
(auto simp: exp_diff l_def exp_add ring_distribs rcis_def cis_conv_exp Complex_eq exp_of_real)
finally show ?thesis .
qed
have "err2 s r = -err2' 0 pi s" for s
proof -
have "err2 s r = -integral {0..pi} (λx. 𝗂 * exp (rcis r x - s * Ln' (rcis r x)) * rcis r x)"
unfolding err2_eq by (simp add: integral_cnj g_def exp_cnj rcis_def cis_cnj)
also have "integral {0..pi} (λt. 𝗂 * exp (rcis r t - s * Ln' (rcis r t)) * rcis r t) =
integral {0..pi} (λt. 𝗂 * exp (rcis r t - s * Complex (ln r) t) * rcis r t)"
proof (intro integral_cong)
fix t assume t: "t ∈ {0..pi}"
have "Ln' (rcis r t) = Ln (rcis r (t - pi / 2)) + 𝗂 * pi / 2"
unfolding Ln'_def by (simp add: rcis_def mult_ac flip: cis_divide)
also have "… = Complex (ln r) t"
by (subst Ln_rcis) (use r t pi_gt_zero in ‹auto simp del: pi_gt_zero simp: complex_eq_iff›)
finally show "𝗂 * exp (rcis r t - s * Ln' (rcis r t)) * rcis r t =
𝗂 * exp (rcis r t - s * Complex (ln r) t) * rcis r t" by simp
qed
finally show ?thesis
by (simp add: err2'_def)
qed
hence err2_holomorphic1: "(λs. err2 s r) holomorphic_on {s. Re s > 0}"
using holomorphic_on_minus[OF err2'_holomorphic[of 0 pi]] by simp
have "cnj (err2 (cnj s) r) = err2' (-pi) 0 s" for s
proof -
have "cnj (err2 (cnj s) r) =
integral {0..pi} (λx. 𝗂 * exp (rcis r (-x) - s * cnj (Ln' (rcis r x))) * (rcis r (-x)))"
unfolding err2_eq by (simp add: integral_cnj g_def exp_cnj rcis_def cis_cnj)
also have "… = integral {0..pi} (λt. 𝗂 * exp (rcis r (-t) - s * Complex (ln r) (-t)) * rcis r (-t))"
proof (intro integral_cong)
fix t assume t: "t ∈ {0..pi}"
have "Ln' (rcis r t) = Ln (rcis r (t - pi / 2)) + 𝗂 * pi / 2"
unfolding Ln'_def by (simp add: rcis_def mult_ac flip: cis_divide)
also have "… = Complex (ln r) t"
by (subst Ln_rcis) (use r t pi_gt_zero in ‹auto simp del: pi_gt_zero simp: complex_eq_iff›)
also have "cnj … = Complex (ln r) (-t)"
by (simp add: complex_eq_iff)
finally show "𝗂 * exp (rcis r (-t) - s * cnj (Ln' (rcis r t))) * rcis r (-t) =
𝗂 * exp (rcis r (-t) - s * Complex (ln r) (-t)) * rcis r (-t)" by simp
qed
also have "… = integral {-pi..0} (λt. 𝗂 * exp (rcis r t - s * Complex (ln r) t) * rcis r t)"
by (subst Henstock_Kurzweil_Integration.integral_reflect_real [symmetric]) simp_all
finally show ?thesis
by (simp add: err2'_def)
qed
hence err2_holomorphic2: "(λs. cnj (err2 (cnj s) r)) holomorphic_on {s. Re s > 0}"
using err2'_holomorphic[of "-pi" 0] by simp
have holo_integral: "(λz. CLBINT t:{r..}. h z (-t)) holomorphic_on UNIV"
proof -
have "(λz. Gamma_incu (1-z) (of_real r)) holomorphic_on UNIV"
using r by (auto intro!: analytic_imp_holomorphic analytic_intros)
also have "(λz. Gamma_incu (1-z) (of_real r)) = (λz. LBINT t:{r..}. h z (-t))"
proof
fix z :: complex
have "Gamma_incu (1-z) (of_real r) = integral {r..} (λt. h z (-t))"
using has_integral_Gamma_incu_complex_of_real'[of r "1-z"] r
by (simp add: h_def minus_diff_commute has_integral_iff)
also have "… = (LBINT t:{r..}. h z (-t))"
by (intro set_borel_integral_eq_integral(2) [symmetric] integrable r)
finally show "Gamma_incu (1 - z) (complex_of_real r) = (LBINT t:{r..}. h z (- t))" .
qed
finally show ?thesis .
qed
show "(λs. RHS s r) holomorphic_on {s. Re s > 0}" unfolding RHS_def
by (intro holomorphic_intros err2_holomorphic1 err2_holomorphic2
holomorphic_on_subset[OF holo_integral]) auto
qed
text ‹
Thus, we can extend the validity of our equation to the half-plane $\text{Re}(s)>0$
by analytic continuation.
›
have RHS_eq': "RHS s r = 2 * pi * rGamma s"
proof (rule analytic_continuation_open[where f = "λs. RHS s r"])
have "Re (1/2) ∈ {0<..<1}"
by simp
thus "{s. Re s ∈ {0<..<1}} ≠ {}"
by blast
next
have "open ({s. Re s > 0} ∩ {s. Re s < 1})"
by (intro open_Int open_halfspace_Re_lt open_halfspace_Re_gt)
also have "… = {s. Re s ∈ {0<..<1}}"
by auto
finally show "open {s. Re s ∈ {0<..<1}}" .
next
show "(λa. complex_of_real (2 * pi) * rGamma a) holomorphic_on {s. Re s > 0}"
by (intro holomorphic_intros)
next
show "RHS s r = complex_of_real (2 * pi) * rGamma s" if s: "s ∈ {s. Re s ∈ {0<..<1}}" for s
using RHS_eq[of s] s r by simp
qed (use s RHS_holo in ‹auto simp: open_halfspace_Re_gt›)
show ?thesis
using lim_lhs[of r s] RHS_eq' r s by (simp add: RHS_def lhs_def f_def o_def)
qed
text ‹
If $\text{Re}(s) > 1$, the integral exists not only as an improper/Cauchy principal value
style integral, but as a Lebesgue integral.
›
corollary rGamma_hankel:
assumes c: "c > 0" and s: "Re s > 1"
shows "(((λz. exp z * z powr (-s)) ∘ (λt. Complex c t))
has_integral (2 * of_real pi * rGamma s)) UNIV"
proof -
have "((λT. integral {-T..T} ((λz. exp z * z powr - s) ∘ Complex c)) ⤏
2 * of_real pi * rGamma s) at_top"
by (rule rGamma_hankel_strong) (use assms in auto)
also have "(λT. integral {-T..T} ((λz. exp z * z powr - s) ∘ Complex c)) =
(λT. set_lebesgue_integral lebesgue {-T..T} ((λz. exp z * z powr - s) ∘ Complex c))"
by (intro ext set_lebesgue_integral_eq_integral(2) [symmetric]
absolutely_integrable_continuous_real)
(use c s in ‹auto simp: complex_eq_iff intro!: continuous_intros›)
finally have "((λT. set_lebesgue_integral lebesgue {-T..T} ((λz. exp z * z powr - s) ∘ Complex c)) ⤏
2 * of_real pi * rGamma s) at_top" .
hence "((λT. set_lebesgue_integral lebesgue {-real T..real T} ((λz. exp z * z powr - s) ∘ Complex c)) ⤏
2 * of_real pi * rGamma s) at_top"
by (rule filterlim_compose) (rule filterlim_real_sequentially)
moreover have
"(λT. set_lebesgue_integral lebesgue {-T..T} ((λz. exp z * z powr - s) ∘ Complex c)) ⇢
lebesgue_integral lebesgue ((λz. exp z * z powr - s) ∘ Complex c)"
unfolding set_lebesgue_integral_def
proof (intro integral_dominated_convergence always_eventually allI)
show "integrable lebesgue (λt. norm (exp (Complex c t) * Complex c t powr -s))"
using rGamma_hankel_integrable[of c s] c s
by (intro integrable_norm) (simp_all add: set_integrable_def)
next
fix t :: real
have "eventually (λT. real T ≥ ¦t¦) at_top"
by real_asymp
hence "eventually (λT. indicat_real {-real T..real T} t *⇩R ((λz. exp z * z powr - s) ∘ Complex c) t =
((λz. exp z * z powr - s) ∘ Complex c) t) at_top"
by eventually_elim (auto simp: indicator_def)
thus "(λT. indicat_real {-real T..real T} t *⇩R ((λz. exp z * z powr - s) ∘ Complex c) t)
⇢ ((λz. exp z * z powr - s) ∘ Complex c) t"
by (rule tendsto_eventually)
qed (auto intro!: measurable_completion simp: indicator_def o_def Complex_eq)
ultimately have "2 * of_real pi * rGamma s =
lebesgue_integral lebesgue ((λz. exp z * z powr - s) ∘ Complex c)"
using LIMSEQ_unique by blast
also have "… = integral UNIV ((λz. exp z * z powr - s) ∘ Complex c)"
using rGamma_hankel_integrable[OF c s]
by (intro integral_lebesgue [symmetric]) (simp_all add: set_integrable_def)
moreover have "((λz. exp z * z powr - s) ∘ Complex c) integrable_on UNIV"
using rGamma_hankel_integrable[OF c s] absolutely_integrable_on_def by blast
ultimately show ?thesis
by (simp add: has_integral_iff)
qed
subsection ‹The integral for the Bessel function›
text ‹
We now show the main result of this section: A Hankel-style contour-integral representation for
the modified Bessel function of the first kind $I(\nu, s)$, valid for all $s$ and $\nu$ with
$\text{Re}(\nu) > 0$.
The integral is of the form $\int_{c-i\infty}^{c+i\infty}$ for any real $c > 0$ and converges
absolutely. The proof is modelled after Proposition~2.4 by Kong and Teo~\<^cite>‹kong_teo› and
works by taking the similar integral formula for $1/\Gamma(s)$, summing over it, and
exchanging the order of summation and integration.
The proof is fairly quick since the main work was already done in other lemmas. The main bit of
work that we still have to do here is to justify exchanging summation and integration.
This is done by showing that the integrals over the absolute value exist for every summand,
and then the sum over these integrals also exists.
The integrals over the summand can be brought into the form
\[\int_{-\infty}^\infty (c^2 + t^2)^a\,\text{d}t\]
for some suitable $a > \frac{1}{2}$, which we showed earlier to have a closed form in terms
of the Beta function.
›
theorem
fixes c :: real and s v :: complex
assumes v: "Re v > 0" and c: "c > 0"
shows has_integral_Bessel_I_complex:
"(((λz. 1 / (2*pi) * (s/2) powr v * exp (z + s⇧2/(4*z)) / z powr (v+1)) ∘ Complex c)
has_integral Bessel_I v s) UNIV"
and absolutely_integrable_Bessel_I_complex:
"((λz. 1 / (2*pi) * (s/2) powr v * exp (z + s⇧2/(4*z)) / z powr (v+1)) ∘ Complex c)
absolutely_integrable_on UNIV"
proof -
from v have v': "v ∉ ℤ⇩≤⇩0"
by (auto elim!: nonpos_Ints_cases)
define LINTL :: "(real ⇒ complex) ⇒ complex" ("∫")
where "LINTL = lebesgue_integral lebesgue"
have 1: "integrable lebesgue (λx. (s/2)^(2*j) / fact j * exp (Complex c x) *
Complex c x powr - (v + of_nat j + 1))" for j
proof -
have "integrable lebesgue (λx. (s/2)^(2*j) / fact j *
(exp (Complex c x) * Complex c x powr - (v + of_nat j + 1)))"
using rGamma_hankel_integrable[of c "v + of_nat j + 1"] c v
by (intro integrable_mult_right) (simp add: set_integrable_def)
thus ?thesis
by (simp add: algebra_simps)
qed
have 2: "summable (λj. norm ((s/2)^(2*j) / fact j * exp (Complex c t) *
Complex c t powr -(v + of_nat j + 1)))" for t :: real
proof -
define z where "z = Complex c t"
define C where "C = exp c * exp (Im v * Arg z) * norm z powr (-Re v-1)"
have "summable (λj. C * (inverse (fact j) * (norm s ^ 2 / (4 * norm z)) ^ j))"
by (intro summable_mult summable_exp)
also have "… = (λj. norm ((s/2)^(2*j) / fact j * exp (Complex c t) *
Complex c t powr -(v + of_nat j + 1)))"
by (intro ext)
(simp_all add: norm_mult norm_divide norm_power power_mult norm_powr_complex z_def
powr_diff powr_minus divide_simps exp_minus powr_add C_def powr_realpow)
finally show "summable …" .
qed
have 3: "summable (λj. LINT t|lebesgue. norm ((s/2)^(2*j) / fact j *
exp (Complex c t) * Complex c t powr - (v + of_nat j + 1)))"
proof -
define C where "C = exp c * (Beta (1 / 2) (Re v / 2) * exp (¦Im v¦ * pi)) * c powr (-Re v)"
show ?thesis
proof (rule summable_comparison_test')
fix j :: nat
assume j: "j ≥ 0"
show "norm (LINT t|lebesgue. norm ((s/2)^(2*j) / fact j *
exp (Complex c t) * Complex c t powr - (v + of_nat j + 1))) ≤
C * (inverse (fact j) * (norm s ^ 2 / (4 * c)) ^ j)"
proof -
define e where "e = (Re v + real j + 1)/2"
define I where "I = c powr (1-2*e) / 2 * Beta (1/2) (e - 1/2)"
have integrable': "integrable lebesgue (λt. (c⇧2 + t⇧2) powr -e)"
and integral': "lebesgue_integral lebesgue (λt. (c⇧2 + t⇧2) powr -e) = 2 * I"
using Bessel_I_aux_integral2[of c e] assms by (simp_all add: e_def I_def)
have "norm (LINT t|lebesgue. norm ((s/2)^(2*j) / fact j * exp (Complex c t) *
Complex c t powr -(v + of_nat j + 1))) =
(LINT t|lebesgue. norm ((s/2)^(2*j) / fact j * exp (Complex c t) *
Complex c t powr -(v + of_nat j + 1)))"
unfolding real_norm_def
by (intro abs_of_nonneg Bochner_Integration.integral_nonneg) auto
also have "… = exp c * (norm s / 2) ^ (2 * j) / fact j *
(LINT t|lebesgue. norm (Complex c t) powr (-Re v - real j - 1) *
exp (Im v * Arg (Complex c t)))"
by (simp add: norm_power norm_mult norm_divide norm_powr_complex)
also have "(LINT t|lebesgue. norm (Complex c t) powr (-Re v - real j - 1) *
exp (Im v * Arg (Complex c t))) =
(LINT t|lebesgue. (c⇧2 + t⇧2) powr (-e) * exp (Im v * Arg (Complex c t)))"
by (intro Bochner_Integration.integral_cong)
(auto simp: cmod_def powr_powr e_def add_divide_distrib diff_divide_distrib
simp flip: powr_half_sqrt)
also have "… ≤ (LINT t|lebesgue. (c⇧2 + t⇧2) powr (-e) * exp (¦Im v¦ * pi))"
proof (rule integral_mono')
show "integrable lebesgue (λx. (c⇧2 + x⇧2) powr -e * exp (¦Im v¦ * pi))"
using integrable' unfolding set_integrable_def by (intro integrable_mult_left)
show "(c⇧2 + t⇧2) powr -e * exp (Im v * Arg (Complex c t)) ≤
(c⇧2 + t⇧2) powr -e * exp (¦Im v¦ * pi)" for t
proof -
have "Im v * Arg (Complex c t) ≤ ¦Im v * Arg (Complex c t)¦"
by linarith
also have "… ≤ ¦Im v¦ * pi"
unfolding abs_mult using Arg_bounded[of "Complex c t"] by (intro mult_left_mono) auto
finally show ?thesis
by (intro mult_mono) auto
qed
qed auto
also have "… = exp (¦Im v¦ * pi) * (LINT t|lebesgue. (c⇧2 + t⇧2) powr (-e))"
by simp
also have "… = 2 * I * exp (¦Im v¦ * pi)"
by (subst integral') simp
also have "I ≤ Beta (1 / 2) (Re v / 2) / 2 * c powr (1 - 2 * e)"
proof -
have "I = Beta (1 / 2) (e - 1 / 2) / 2 * c powr (1 - 2 * e)"
by (simp add: I_def mult_ac)
also have "Beta (1 / 2) (e - 1 / 2) ≤ Beta (1 / 2) (Re v / 2)"
by (rule Beta_real_mono) (use v in ‹simp_all add: e_def add_divide_distrib›)
finally show ?thesis
using c by simp
qed
also have "exp c * (cmod s / 2) ^ (2 * j) / fact j *
(2 * (Beta (1 / 2) (Re v / 2) / 2 * c powr (1 - 2 * e)) * exp (¦Im v¦ * pi)) =
C * (inverse (fact j) * ((cmod s)⇧2 / (4 * c)) ^ j)" using c
by (simp add: C_def divide_simps e_def powr_diff powr_minus powr_realpow power_mult diff_divide_distrib)
finally show ?thesis
by (simp add: mult_left_mono mult_right_mono divide_right_mono)
qed
next
show "summable (λj. C * (inverse (fact j) * (norm s ^ 2 / (4 * c)) ^ j))"
by (intro summable_mult summable_exp)
qed
qed
have sum_eq:
"(λt. ∑j. (s/2)^(2*j) / fact j * exp (Complex c t) * Complex c t powr -(v + of_nat j + 1)) =
(λz. exp (z + s⇧2/(4*z)) * z powr -(v+1)) ∘ (λt. Complex c t)"
(is "?lhs = ?rhs")
proof
fix t :: real
define z where "z = Complex c t"
have "(λj. exp z * z powr -(v+1) * ((s⇧2/(4 * z))^j /⇩R fact j)) sums
((exp z * z powr -(v+1)) * exp (s⇧2/(4 * z)))"
by (intro sums_mult exp_converges)
also have "(exp z * z powr -(v+1)) * exp (s⇧2/(4*z)) = exp (z + s⇧2/(4*z)) * z powr -(v+1)"
by (simp add: exp_add field_simps)
also have "(λj. exp z * z powr -(v+1) * ((s⇧2/(4 * z))^j /⇩R fact j)) =
(λj. (s/2)^(2*j) / fact j * exp z * z powr -(v + of_nat j + 1))"
apply (rule ext)
apply (simp add: powr_diff powr_minus power_divide power_mult powr_nat scaleR_conv_of_real)
apply (simp add: field_simps)?
done
finally show "?lhs t = ?rhs t"
by (simp add: sums_iff z_def)
qed
have "integrable lebesgue
(λt. ∑j. (s/2)^(2*j) / fact j * exp (Complex c t) * Complex c t powr -(v + of_nat j + 1))"
by (intro integrable_suminf always_eventually allI 1 2 3)
hence "integrable lebesgue ((λz. exp (z + s⇧2 / (4 * z)) * z powr - (v + 1)) ∘ Complex c)"
unfolding sum_eq .
hence "integrable lebesgue ((λz. ((s/2) powr v / (2*pi)) *
(exp (z + s⇧2 / (4 * z)) * z powr - (v + 1))) ∘ Complex c)"
unfolding o_def by (intro integrable_mult_right)
thus integrable:
"((λz. 1 / (2*pi) * (s/2) powr v * exp (z + s⇧2 / (4 * z)) / z powr (v + 1))) ∘ Complex c
absolutely_integrable_on UNIV"
by (simp add: o_def set_integrable_def powr_minus powr_diff powr_add field_simps)
have "(λj. ∫((λz. (s/2)^(2*j) / fact j * exp z * z powr -(v + of_nat j + 1)) ∘ Complex c)) sums
∫(λt. ∑j. (s/2)^(2*j) / fact j * exp (Complex c t) * Complex c t powr -(v + of_nat j + 1))"
unfolding LINTL_def o_def by (intro sums_integral always_eventually allI 1 2 3)
also have "(λj. ∫ ((λz. (s/2)^(2*j) / fact j * exp z * z powr -(v + of_nat j + 1)) ∘ Complex c)) =
(λj. (s/2)^(2*j) / fact j * 2 * pi * rGamma (v + of_nat j + 1))" (is "?lhs = ?rhs")
proof
fix j :: nat
have "∫ ((λz. (s/2)^(2*j) / fact j * exp z * z powr -(v + of_nat j + 1)) ∘ Complex c) =
(s/2)^(2*j) / fact j * ∫ ((λz. exp z * z powr -(v + of_nat j + 1)) ∘ Complex c)"
unfolding o_def LINTL_def
by (subst integral_mult_right_zero [symmetric], rule Bochner_Integration.integral_cong) simp_all
also have "∫ ((λz. exp z * z powr -(v + of_nat j + 1)) ∘ Complex c) =
integral UNIV ((λz. exp z * z powr -(v + of_nat j + 1)) ∘ Complex c)" unfolding LINTL_def
by (rule integral_lebesgue [symmetric])
(use rGamma_hankel_integrable[of c "v + of_nat j + 1"] c v in ‹simp_all add: set_integrable_def›)
also have "… = 2 * pi * rGamma (v + of_nat j + 1)"
using rGamma_hankel[of c "v + of_nat j + 1"] c v
by (simp add: has_integral_iff field_simps)
finally show "?lhs j = ?rhs j" by (simp add: o_def)
qed
also note sum_eq
finally have "(λj. ((s/2) powr v / (2*pi)) *
((s/2)^(2*j) / fact j * 2 * of_real pi * rGamma (v + of_nat j + 1))) sums
(((s/2) powr v / (2*pi)) * (∫ ((λz. exp (z + s⇧2/(4*z)) * z powr -(v+1)) ∘ Complex c)))"
by (intro sums_mult)
also have "(λj. ((s/2) powr v / (2*pi)) * ((s/2)^(2*j) / fact j * 2 * of_real pi * rGamma (v + of_nat j + 1))) =
(λj. (s/2) powr (v + 2 * of_nat j) * rGamma (v + of_nat j + 1) / fact j)"
by (intro ext; cases "s = 0") (auto simp: powr_add simp flip: powr_nat')
finally have "(λj. (s/2) powr (v + 2 * of_nat j) * rGamma (v + of_nat j + 1) / fact j) sums
(((s/2) powr v / (2 * pi)) * (∫ ((λz. exp (z + s⇧2 / (4 * z)) * z powr - (v + 1)) ∘ Complex c)))" .
also have "((s/2) powr v / (2 * pi)) * ∫ ((λz. exp (z + s⇧2 / (4 * z)) * z powr - (v + 1)) ∘ Complex c) =
(∫ ((λz. 1 / (2 * pi) * (s/2) powr v * exp (z + s⇧2 / (4 * z)) / z powr (v+1)) ∘ Complex c))"
unfolding LINTL_def
by (subst integral_mult_right_zero [symmetric], rule Bochner_Integration.integral_cong)
(simp_all add: o_def powr_diff powr_add powr_minus field_simps)
finally have "(λj. (s/2) powr (v + 2 * of_nat j) * rGamma (v + of_nat j + 1) / fact j) sums
(∫ ((λz. 1 / (2 * pi) * (s/2) powr v * exp (z + s⇧2/(4*z)) / z powr (v+1)) ∘ Complex c))" .
moreover have "(λj. (s/2) powr (v + 2 * of_nat j) * rGamma (v + of_nat j + 1) / fact j) sums
Bessel_I v s"
proof -
have "(λj. (s/2) powr' (v + 2 * of_nat j) * rGamma (v + of_nat j + 1) / fact j) sums
Bessel_I v s"
using sums_Bessel_I_complex[of s v] v' by (simp add: rGamma_inverse_Gamma field_simps)
also have "(λj. (s/2) powr' (v + 2 * of_nat j)) = (λj. (s/2) powr (v + 2 * of_nat j))"
(is "?lhs = ?rhs")
proof
fix j :: nat
from v' have "v + 2 * complex_of_nat j ≠ 0"
by (metis v' add.commute left_add_twice plus_of_nat_eq_0_imp plus_of_nat_notin_nonpos_Ints)
thus "?lhs j = ?rhs j"
by (cases "s = 0") (auto simp: powr'_complex powr'_0_left_if)
qed
finally show ?thesis .
qed
ultimately have eq:
"Bessel_I v s =
(∫ ((λz. 1 / (2 * pi) * (s/2) powr v * exp (z + s⇧2/(4*z)) / z powr (v+1)) ∘ Complex c))"
using sums_unique2 by blast
also have "… = integral UNIV ((λz. 1 / (2 * pi) * (s/2) powr v *
exp (z + s⇧2/(4*z)) / z powr (v+1)) ∘ Complex c)"
unfolding LINTL_def using integrable unfolding set_integrable_def
by (intro integral_lebesgue [symmetric]) simp
finally show "(((λz. 1 / (2*pi) * (s/2) powr v * exp (z + s⇧2/(4*z)) / z powr (v+1)) ∘ Complex c)
has_integral Bessel_I v s) UNIV"
using set_lebesgue_integral_eq_integral(1)[OF integrable] assms
by (simp add: has_integral_iff)
qed
lemma has_integral_Bessel_I_complex':
fixes x :: complex and c :: real and v :: complex and f :: "complex ⇒ complex"
defines "f ≡ (λt. exp (t + x⇧2 / t) / t powr v)"
assumes c: "c > 0" and v: "Re v > 1" and x: "x ≠ 0"
shows "((f ∘ (λt. Complex c t)) has_integral
(2 * pi * Bessel_I (v-1) (2*x)) / (x powr (v-1))) UNIV"
proof -
define a where "a = 2 * pi / (x powr (v - 1))"
define g where "g = (λt. (1 / (2 * pi)) * x powr (v - 1) * exp (t + x⇧2 / t) / t powr v) ∘ (λt. Complex c t)"
have "(g has_integral Bessel_I (v - 1) (2 * x)) UNIV"
using has_integral_Bessel_I_complex[of "v-1" c "2*x"] assms unfolding g_def by (simp add: o_def)
hence "((λt. a * g t) has_integral (a * Bessel_I (v - 1) (2 * x))) UNIV"
by (rule has_integral_mult_right)
also have "(λt. a * g t) = f ∘ (λt. Complex c t)"
using x by (auto simp: a_def g_def f_def fun_eq_iff)
finally show "((f ∘ (λt. Complex c t)) has_integral
(2 * pi * Bessel_I (v - 1) (2 * x)) / (x powr (v - 1))) UNIV"
by (simp add: a_def o_def)
qed
lemma absolutely_integrable_Bessel_I_complex':
fixes c :: real and s v :: complex
assumes v: "Re v > 1" and c: "c > 0"
shows "((λz. exp (z + s/z) / z powr v) ∘ Complex c) absolutely_integrable_on UNIV"
proof (cases "s = 0")
case [simp]: False
define x where "x = csqrt s"
define C where "C = 1 / (2*pi) * (2 * csqrt s / 2) powr (v-1)"
have [simp]: "C ≠ 0"
by (simp add: C_def)
have "(λz. inverse C * ((λz. C * exp (z + (2 * csqrt s)⇧2/(4*z)) / z powr (v-1+1)) ∘ Complex c) z)
absolutely_integrable_on UNIV" unfolding C_def
by (intro set_integrable_mult_right absolutely_integrable_Bessel_I_complex) (use v c in auto)
also have "(λz. inverse C * ((λz. C * exp (z + (2 * csqrt s)⇧2/(4*z)) / z powr (v-1+1)) ∘ Complex c) z) =
(λz. exp (z + s / z) / z powr v) ∘ Complex c"
by (simp add: fun_eq_iff)
finally show ?thesis .
next
case [simp]: True
show ?thesis using rGamma_hankel_integrable[of c v] c v
by (simp add: powr_minus field_simps)
qed
end