English
The odd kernel satisfies a functional equation relating its values at x and 1/x: for x > 0, oddKernel(a, x) = x^{-3/2} sinKernel(a, 1/x).
Русский
Нечетное ядро удовлетворяет функциональному уравнению, связывающему значения при x и 1/x: при x > 0, oddKernel(a, x) = x^{-3/2} sinKernel(a, 1/x).
LaTeX
$$$$ \text{If } x>0:\quad \operatorname{oddKernel}(a,x) = x^{-3/2} \operatorname{sinKernel}(a,1/x). $$$$
Lean4
theorem oddKernel_functional_equation (a : UnitAddCircle) (x : ℝ) :
oddKernel a x = 1 / x ^ (3 / 2 : ℝ) * sinKernel a (1 / x) := by
-- first reduce to `0 < x`
rcases le_or_gt x 0 with hx | hx
· rw [oddKernel_undef _ hx, sinKernel_undef _ (one_div_nonpos.mpr hx), mul_zero]
induction a using QuotientAddGroup.induction_on with
| H
a =>
have h1 : -1 / (I * ↑(1 / x)) = I * x := by
rw [one_div, ofReal_inv, mul_comm, ← div_div, div_inv_eq_mul, div_eq_mul_inv, inv_I, mul_neg, neg_one_mul,
neg_mul, neg_neg, mul_comm]
have h2 : (-I * (I * ↑(1 / x))) = 1 / x := by
rw [← mul_assoc, neg_mul, I_mul_I, neg_neg, one_mul, ofReal_div, ofReal_one]
have h3 : (x : ℂ) ^ (3 / 2 : ℂ) ≠ 0 := by
simp only [Ne, cpow_eq_zero_iff, ofReal_eq_zero, hx.ne', false_and, not_false_eq_true]
have h4 : arg x ≠ π := by rw [arg_ofReal_of_nonneg hx.le]; exact pi_ne_zero.symm
rw [← ofReal_inj, oddKernel_def, ofReal_mul, sinKernel_def, jacobiTheta₂'_functional_equation', h1, h2]
generalize jacobiTheta₂'' a (I * ↑x) = J
rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le, ofReal_div,
ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero), ← div_eq_inv_mul,
eq_div_iff h3, mul_comm J _, mul_right_comm]
