English
For every a on the unit circle, the function x ↦ oddKernel(a, x) is continuous on the positive real axis (0, ∞).
Русский
Для каждого a на единичном круге функция x ↦ oddKernel(a, x) непрерывна на (0, ∞).
LaTeX
$$$\\forall a\,\\ContinuousOn(\\text{oddKernel}(a), (0, \infty)).$$$
Lean4
/-- The odd kernel is continuous on `Ioi 0`. -/
theorem continuousOn_oddKernel (a : UnitAddCircle) : ContinuousOn (oddKernel a) (Ioi 0) := by
induction a using QuotientAddGroup.induction_on with
| H
a =>
suffices ContinuousOn (fun x ↦ (oddKernel a x : ℂ)) (Ioi 0) from
(continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
simp_rw [oddKernel_def' a]
refine fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt
· fun_prop
· have hf : Continuous fun u : ℝ ↦ (a * I * u, I * u) := by fun_prop
apply ContinuousAt.add
·
exact
((continuousAt_jacobiTheta₂' (a * I * x) (by rwa [I_mul_im, ofReal_re])).comp (f := fun u : ℝ ↦
(a * I * u, I * u)) hf.continuousAt).div_const
_
·
exact
continuousAt_const.mul <|
(continuousAt_jacobiTheta₂ (a * I * x) (by rwa [I_mul_im, ofReal_re])).comp (f := fun u : ℝ ↦
(a * I * u, I * u)) hf.continuousAt
