English
There is a uniform bound for the norm of the integrand along the vertical edges, leading to an L^1 estimate for the integral.
Русский
Существует единичная граница нормы интегранта вдоль вертикальных граней, дающая априорную оценку интеграла.
LaTeX
$$$$ \| \mathrm{verticalIntegral}(b,c,T) \| \le 2|c| \exp\big(-\Re(b) T^2 + 2|\Im(b)| |c| T - \Re(b) c^2\big). $$$$
Lean4
theorem verticalIntegral_norm_le (hb : 0 < b.re) (c : ℝ) {T : ℝ} (hT : 0 ≤ T) :
‖verticalIntegral b c T‖ ≤ (2 : ℝ) * |c| * exp (-(b.re * T ^ 2 - (2 : ℝ) * |b.im| * |c| * T - b.re * c ^ 2)) := by
-- first get uniform bound for integrand
have vert_norm_bound :
∀ {T : ℝ},
0 ≤ T →
∀ {c y : ℝ},
|y| ≤ |c| →
‖cexp (-b * (T + y * I) ^ 2)‖ ≤ exp (-(b.re * T ^ 2 - (2 : ℝ) * |b.im| * |c| * T - b.re * c ^ 2)) :=
by
intro T hT c y hy
rw [norm_cexp_neg_mul_sq_add_mul_I b]
gcongr exp (-(_ - ?_ * _ - _ * ?_))
· (conv_lhs => rw [mul_assoc]); (conv_rhs => rw [mul_assoc])
gcongr _ * ?_
refine (le_abs_self _).trans ?_
rw [abs_mul]
gcongr
·
rwa [sq_le_sq]
-- now main proof
apply (intervalIntegral.norm_integral_le_of_norm_le_const _).trans
· rw [sub_zero]
conv_lhs => simp only [mul_comm _ |c|]
conv_rhs =>
conv =>
congr
rw [mul_comm]
rw [mul_assoc]
· intro y hy
have absy : |y| ≤ |c| := by
rcases le_or_gt 0 c with (h | h)
· rw [uIoc_of_le h] at hy
rw [abs_of_nonneg h, abs_of_pos hy.1]
exact hy.2
· rw [uIoc_of_ge h.le] at hy
rw [abs_of_neg h, abs_of_nonpos hy.2, neg_le_neg_iff]
exact hy.1.le
rw [norm_mul, norm_I, one_mul, two_mul]
refine (norm_sub_le _ _).trans (add_le_add (vert_norm_bound hT absy) ?_)
rw [← abs_neg y] at absy
simpa only [neg_mul, ofReal_neg] using vert_norm_bound hT absy
