continuousOn_evenKernel — Mathlib

English

The function x ↦ evenKernel(a) is continuous on (0, ∞) for each a ∈ UnitAddCircle.

Русский

Функция x ↦ evenKernel(a,x) непрерывна на (0, ∞) для каждого a ∈ UnitAddCircle.

LaTeX

$$$$\\text{ContinuousOn}(\\lambda x. \\operatorname{evenKernel}(a,x), (0,\\infty)).$$$$

Lean4

theorem continuousOn_evenKernel (a : UnitAddCircle) : ContinuousOn (evenKernel a) (Ioi 0) := by
  induction a using QuotientAddGroup.induction_on with
  | H a' =>
    apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))
    simp only [evenKernel_def]
    refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)
    exact (continuousAt_jacobiTheta₂ (a' * I * x) <| by simpa).comp (f := fun u : ℝ ↦ (a' * I * u, I * u)) (by fun_prop)

Похожие утверждения