toMeromorphicNFAt

Mathlib.Analysis.Meromorphic.NormalForm

URI: https://scilib.ai/kg/mathlib#toMeromorphicNFAt

Lean4

/-- If `f` is meromorphic at `x`, convert `f` to normal form at `x` by changing its value at `x`.
Otherwise, returns the 0 function. -/
noncomputable def toMeromorphicNFAt : 𝕜 → E :=
  by
  by_cases hf : MeromorphicAt f x
  ·
    classical -- do not complain about decidability issues in Function.update

    apply Function.update f x
    by_cases h₁f : meromorphicOrderAt f x = (0 : ℤ)
    · rw [meromorphicOrderAt_eq_int_iff hf] at h₁f
      exact (Classical.choose h₁f) x
    · exact 0
  · exact 0

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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