English
There is a WeakFEPair (a pair of functions) linking evenKernel a and cosKernel a, with specified integrability, decay, and a half-integer index k = 1/2, satisfying a functional equation.
Русский
Существует слабый пары Фурье-элемент, связывающий evenKernel a и cosKernel a, с заданной интегрируемостью, распадом и индексом k = 1/2, удовлетворяющий функциональному уравнению.
LaTeX
$$$$ \\text{There exists a WeakFEPair } (f,g) \\text{ with } f(x) = \\operatorname{Real}(f_0 \\circ \\, \\operatorname{evenKernel} a)(x), \; g(x) = \\operatorname{Real}(g_0 \\circ \\, \\operatorname{cosKernel} a)(x), $$ and with the specified decay and normalization constants, satisfying a functional equation between f and g.$$
Lean4
theorem hasSum_nat_cosKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) :
HasSum (fun n : ℕ ↦ 2 * Real.cos (2 * π * a * (n + 1)) * rexp (-π * (n + 1) ^ 2 * t)) (cosKernel a t - 1) :=
by
rw [← hasSum_ofReal, ofReal_sub, ofReal_one]
have := (hasSum_int_cosKernel a ht).nat_add_neg
rw [← hasSum_nat_add_iff' 1] at this
simp_rw [Finset.sum_range_one, Nat.cast_zero, neg_zero, Int.cast_zero, zero_pow two_ne_zero, mul_zero, zero_mul,
Complex.exp_zero, Real.exp_zero, ofReal_one, mul_one, Int.cast_neg, Int.cast_natCast, neg_sq, ← add_mul,
add_sub_assoc, ← sub_sub, sub_self, zero_sub, ← sub_eq_add_neg, mul_neg] at this
refine this.congr_fun fun n ↦ ?_
push_cast
rw [Complex.cos, mul_div_cancel₀ _ two_ne_zero]
congr 3 <;> ring
