continuousOn_cosKernel — Mathlib

English

cosKernel(a) is continuous on (0, ∞) as a function of x for each a.

Русский

cosKernel(a) непрерывно по x на (0, ∞) для каждого a.

LaTeX

$$$$\\text{ContinuousOn}(\\cosKernel(a), (0,\\infty)).$$$$

Lean4

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

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