analyticAt — Mathlib

English

If d: 𝕜 → ℤ is such that 0 ≤ d(x), then the factorized rational function F(x) = ∏ᶠ u, (· − u)^{d(u)} is analytic at x.

Русский

Если d: 𝕜 → ℤ удовлетворяет условию 0 ≤ d(x), то функция F(·) = ∏ᶠ u (· − u)^{d(u)} аналитична в окрестности x.

LaTeX

$$$ 0 \le d(x) \quad\Rightarrow\quad \AnalyticAt_{\mathbb{K}} \Big( \prod^{\mathrm{fin}}_{u} (\cdot - u)^{d(u)} \Big) x $$$

Lean4

/-- Factorized rational functions are analytic wherever the exponent is non-negative.
-/
theorem analyticAt {d : 𝕜 → ℤ} {x : 𝕜} (h : 0 ≤ d x) : AnalyticAt 𝕜 (∏ᶠ u, (· - u) ^ d u) x :=
  by
  apply analyticAt_finprod
  intro u
  by_cases h₂ : x = u
  · apply AnalyticAt.fun_zpow_nonneg (by fun_prop)
    rwa [← h₂]
  · apply AnalyticAt.fun_zpow (by fun_prop)
    rwa [sub_ne_zero]

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