English
Let a be a point of UnitAddCircle and x be a real number. For all nonzero x, the even kernel satisfies the relation evenKernel(a, x) = x^{-1/2} cosKernel(a, 1/x).
Русский
Пусть a принадлежит UnitAddCircle и x — вещественное число. Для всех ненулевых x выполняется равенство evenKernel(a, x) = x^{-1/2} cosKernel(a, 1/x).
LaTeX
$$$\\\\text{Let } a \\\\in \\\\\\mathrm{UnitAddCircle}, \\\\ x \\\\in \\\\\\mathbb{R}. \\\\text{Then, for } x \\\\neq 0, \\\\ \\\\operatorname{evenKernel}(a, x) = x^{-1/2} \\,\\\\cosKernel(a, 1/x).$$$
Lean4
theorem evenKernel_functional_equation (a : UnitAddCircle) (x : ℝ) :
evenKernel a x = 1 / x ^ (1 / 2 : ℝ) * cosKernel a (1 / x) :=
by
rcases le_or_gt x 0 with hx | hx
· rw [evenKernel_undef _ hx, cosKernel_undef, mul_zero]
exact div_nonpos_of_nonneg_of_nonpos zero_le_one hx
induction a using QuotientAddGroup.induction_on with
| H a =>
rw [← ofReal_inj, ofReal_mul, evenKernel_def, cosKernel_def, jacobiTheta₂_functional_equation]
have h1 : I * ↑(1 / x) = -1 / (I * x) := by
push_cast
rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')
have h2 : a * I * x / (I * x) = a := by
rw [div_eq_iff hx']
ring
have h3 : 1 / (-I * (I * x)) ^ (1 / 2 : ℂ) = 1 / ↑(x ^ (1 / 2 : ℝ)) := by
rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div, ofReal_one, ofReal_ofNat]
have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = -(-π * a ^ 2 * x) :=
by
rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
ring
rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _), ← Complex.exp_add,
neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]
