MeromorphicAt.congr
theorem MeromorphicAt.congr :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜},
MeromorphicAt f x → (nhdsWithin x {x}ᶜ).EventuallyEq f g → MeromorphicAt g x
The theorem `MeromorphicAt.congr` states that for any nontrivially normed field `𝕜`, normed addition commutative group `E`, and normed space over `𝕜` and `E`, if `f` and `g` are functions from `𝕜` to `E` and `x` is an element of `𝕜`, then the meromorphy of `f` at `x` implies the meromorphy of `g` at `x`, provided that `f` and `g` are eventually equal in the punctured neighborhood of `x`. In other words, the meromorphy of a function at a point depends only on the function's values in a punctured neighborhood of that point and not on the function's value at the point itself.
More concisely: If `f` and `g` are functions from a nontrivially normed field to a normed space, with the same meromorphic behavior in a punctured neighborhood of `x`, then `f` being meromorphic at `x` implies that `g` is meromorphic at `x` as well.
|
AnalyticAt.meromorphicAt
theorem AnalyticAt.meromorphicAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, AnalyticAt 𝕜 f x → MeromorphicAt f x
This theorem states that for any nontrivially normed field `𝕜` and any normed space `E` over `𝕜`, if a function `f` from `𝕜` to `E` is analytic at a point `x` in `𝕜`, then `f` is meromorphic at `x`. Here, a function `f` being analytic at a point `x` means that it admits a convergent power series expansion around `x`, while `f` being meromorphic at `x` signifies that it is analytic on a punctured neighbourhood of `x`, i.e., the function can be expressed as a power series except possibly at `x` itself.
More concisely: If `f` is an analytic function from a nontrivially normed field `𝕜` to a normed space `E` over `𝕜` at a point `x` in `𝕜`, then `f` is meromorphic at `x`.
|
MeromorphicAt.inv
theorem MeromorphicAt.inv :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜}, MeromorphicAt f x → MeromorphicAt f⁻¹ x
This theorem states that for any nontrivially normed field `𝕜`, for any function `f : 𝕜 → 𝕜`, and any value `x` in `𝕜`, if `f` is meromorphic at `x`, then the reciprocal function `f⁻¹` is also meromorphic at `x`.
In mathematical terms, being meromorphic means that the function can be written as a ratio of two analytic functions (with the denominator not identically zero) in a punctured neighborhood of `x`, i.e., a neighborhood of `x` without the point `x` itself. The theorem asserts that this property is preserved under taking reciprocals, i.e., if `f` is meromorphic at a point, then so is `1/f`, provided `f` is not zero at that point.
More concisely: If `f : 𝕜 -> 𝕜` is a meromorphic function at `x` in a nontrivially normed field `𝕜` with `f(x) != 0`, then the reciprocal function `f⁻¹` is also meromorphic at `x`.
|
MeromorphicAt.mul
theorem MeromorphicAt.mul :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {x : 𝕜},
MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (f * g) x
The theorem `MeromorphicAt.mul` states that if two functions `f` and `g` are meromorphic at a point `x` in the domain of a nontrivially normed field `𝕜`, then their product function `(f * g)` is also meromorphic at `x`. In other words, the meromorphicity at a point is preserved under multiplication of functions. This is analogous to the property in complex analysis that the product of two meromorphic functions is again a meromorphic function.
More concisely: If `f` and `g` are meromorphic at a point `x` in a nontrivially normed field `𝕜`, then their product `(f * g)` is also meromorphic at `x`.
|