analyticOnNhd_circleMap — Mathlib

English

The circle map is real-analytic on ℝ.

Русский

Круговая карта является вещественно аналитической на ℝ.

LaTeX

$$$ circleMap\,c\,R : \mathbb{R} \to \mathbb{C} \text{ is real-analytic on } \mathbb{R}. $$$

Lean4

/-- The circleMap is real analytic. -/
theorem analyticOnNhd_circleMap (c : ℂ) (R : ℝ) : AnalyticOnNhd ℝ (circleMap c R) Set.univ :=
  by
  intro z hz
  apply analyticAt_const.add
  apply analyticAt_const.mul
  rw [← Function.comp_def]
  apply analyticAt_cexp.restrictScalars.comp ((ofRealCLM.analyticAt z).mul (by fun_prop))

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