continuousOn_sinKernel — Mathlib

English

For every a on the unit circle, the function x ↦ sinKernel(a, x) is continuous on (0, ∞).

Русский

Для каждого a на единичном круге функция x ↦ sinKernel(a, x) непрерывна на (0, ∞).

LaTeX

$$$\\forall a\,\\ContinuousOn(\\sinKernel(a), (0, \infty)).$$$

Lean4

theorem continuousOn_sinKernel (a : UnitAddCircle) : ContinuousOn (sinKernel a) (Ioi 0) := by
  induction a using QuotientAddGroup.induction_on with
  | H
    a =>
    suffices ContinuousOn (fun x ↦ (sinKernel a x : ℂ)) (Ioi 0) from
      (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
    simp_rw [sinKernel_def]
    apply (continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)).div_const
    have h := continuousAt_jacobiTheta₂' a (by rwa [I_mul_im, ofReal_re])
    fun_prop

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