eval_continuousLinearMap — Mathlib

English

If for all i the coordinates f i are analytic at every point in s in a neighborhood sense, then x ↦ aeval(f(x)) p is analytic on s.

Русский

Если для всех i координаты f i аналитичны в каждой точке из множества s в окрестности, то x ↦ aeval(f(x)) p аналитично на s.

LaTeX

$$$(\\forall i, AnalyticOnNhd\\, 𝕜 (f\\cdot i)\\, s) \\Rightarrow AnalyticOnNhd\\, 𝕜 ( x \\mapsto \\operatorname{aeval}(f(x), p) )\\, s.$$$

Lean4

theorem eval_continuousLinearMap (f : E →L[𝕜] σ → B) (p : MvPolynomial σ B) :
    AnalyticOnNhd 𝕜 (fun x ↦ eval (f x) p) Set.univ := fun x _ ↦
  .aeval_mvPolynomial (fun i ↦ ((ContinuousLinearMap.proj i).comp f).analyticAt x) p

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