sigmoid'

Mathlib.Analysis.SpecialFunctions.Sigmoid

URI: https://scilib.ai/kg/mathlib#AnalyticAt.sigmoid'

English

If f is analytic at x, then z ↦ Real.sigmoid(f(z)) is analytic at x.

Русский

Пусть f аналитична в точке x; тогда z ↦ сигмоид(f(z)) аналитична в x.

LaTeX

$$$\mathrm{AnalyticAt}_{\mathbb{R}}(f, x) \Rightarrow \mathrm{AnalyticAt}_{\mathbb{R}}(\operatorname{sigmoid} \circ f, x)$$$

Lean4

@[fun_prop]
theorem sigmoid' {x : E} (fa : AnalyticAt ℝ f x) : AnalyticAt ℝ (fun z ↦ Real.sigmoid (f z)) x :=
  fa.sigmoid

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru