The Trailing Coefficient of a Meromorphic Function

This file defines the trailing coefficient of a meromorphic function. If f is meromorphic at a point x, the trailing coefficient is defined as the (unique!) value g x for a presentation of f in the form (z - x) ^ order • g z with g analytic at x.

The lemma meromorphicTrailingCoeffAt_eq_limit expresses the trailing coefficient as a limit.

noncomputable def meromorphicTrailingCoeffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (x : 𝕜) : E

If f is meromorphic of finite order at a point x, the trailing coefficient is defined as the (unique!) value g x for a presentation of f in the form (z - x) ^ order • g z with g analytic at x. In all other cases, the trailing coefficient is defined to be zero.

Equations

• meromorphicTrailingCoeffAt f x = if h₁ : MeromorphicAt f x then if h₂ : meromorphicOrderAt f x = ⊤ then 0 else ⋯.choose x else 0

@[simp]

theorem meromorphicTrailingCoeffAt_of_not_MeromorphicAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h : ¬MeromorphicAt f x) : meromorphicTrailingCoeffAt f x = 0

If f is not meromorphic at x, the trailing coefficient is zero by definition.

@[simp]

theorem MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h : meromorphicOrderAt f x = ⊤) : meromorphicTrailingCoeffAt f x = 0

If f is meromorphic of infinite order at x, the trailing coefficient is zero by definition.

Characterization of the Leading Coefficient

theorem AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜} (h₁g : AnalyticAt 𝕜 g x) (h : f =ᶠ[nhdsWithin x {x}ᶜ] fun (z : 𝕜) => (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) : meromorphicTrailingCoeffAt f x = g x

Definition of the trailing coefficient in case where f is meromorphic and a presentation of the form f = (z - x) ^ order • g z is given, with g analytic at x.

theorem AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜} {n : ℤ} (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) (h : f =ᶠ[nhdsWithin x {x}ᶜ] fun (z : 𝕜) => (z - x) ^ n • g z) : meromorphicTrailingCoeffAt f x = g x

Variant of meromorphicTrailingCoeffAt_of_order_eq_finite: Definition of the trailing coefficient in case where f is meromorphic of finite order and a presentation is given.

@[simp]

theorem AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h₁ : AnalyticAt 𝕜 f x) (h₂ : f x ≠ 0) : meromorphicTrailingCoeffAt f x = f x

If f is analytic and does not vanish at x, then the trailing coefficient of f at x is f x.

theorem MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) : Filter.Tendsto ((fun (x_1 : 𝕜) => x_1 - x) ^ (-(meromorphicOrderAt f x).untop₀) • f) (nhdsWithin x {x}ᶜ) (nhds (meromorphicTrailingCoeffAt f x))

If f is meromorphic at x, then the trailing coefficient of f at x is the limit of the function (· - x) ^ (-order) • f.

Elementary Properties

theorem MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} (h₁ : MeromorphicAt f x) (h₂ : meromorphicOrderAt f x ≠ ⊤) : meromorphicTrailingCoeffAt f x ≠ 0

If f is meromorphic of finite order at x, then the trailing coefficient is not zero.

Congruence Lemma

theorem meromorphicTrailingCoeffAt_congr_nhdsNE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E} (h : f₁ =ᶠ[nhdsWithin x {x}ᶜ] f₂) : meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x

If two functions agree in a punctured neighborhood, then their trailing coefficients agree.

Behavior under Arithmetic Operations

theorem MeromorphicAt.meromorphicTrailingCoeffAt_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) : meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x

The trailing coefficient of a scalar product is the scalar product of the trailing coefficients.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f₁ f₂ : 𝕜 → 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) : meromorphicTrailingCoeffAt (f₁ * f₂) x = meromorphicTrailingCoeffAt f₁ x * meromorphicTrailingCoeffAt f₂ x

The trailing coefficient of a product is the product of the trailing coefficients.

theorem meromorphicTrailingCoeffAt_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} : meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹

The trailing coefficient of the inverse function is the inverse of the trailing coefficient.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℤ} {f : 𝕜 → 𝕜} (h₁ : MeromorphicAt f x) : meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

The trailing coefficient of the power of a function is the power of the trailing coefficient.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {f : 𝕜 → 𝕜} (h₁ : MeromorphicAt f x) : meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

The trailing coefficient of the power of a function is the power of the trailing coefficient.