exp_analytic

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.exp_analytic

English

The exponential map is analytic at every point of the Banach algebra.

Русский

Экспонента аналитична во всех точках банаховой алгебры.

LaTeX

$$$\text{AnalyticAt } 𝕂 (\exp 𝕂) x$ for all x$$

Lean4

theorem exp_analytic (x : 𝔸) : AnalyticAt 𝕂 (exp 𝕂) x :=
  analyticAt_exp_of_mem_ball x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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

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

Разделы

Аффилиация

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