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 MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt 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 Trailing 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.

@[simp]

theorem meromorphicTrailingCoeffAt_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x e : 𝕜} : meromorphicTrailingCoeffAt (fun (x : 𝕜) => e) x = e

The trailing coefficient of a constant function is the constant.

theorem meromorphicTrailingCoeffAt_id_sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] {x y : 𝕜} : meromorphicTrailingCoeffAt (fun (x : 𝕜) => x - y) x = if x = y then 1 else x - y

The trailing coefficient of fun z ↦ z - constant at z₀ equals one if z₀ = constant, or else z₀ - constant.

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 meromorphicTrailingCoeffAt_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} : meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x

Taking the negative commutes with taking meromorphicTrailingCoeffAt.

theorem meromorphicTrailingCoeffAt_fun_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} : meromorphicTrailingCoeffAt (fun (z : 𝕜) => -f z) x = -meromorphicTrailingCoeffAt f x

Taking the negative commutes with taking meromorphicTrailingCoeffAt.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_left_of_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E} (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) : meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x

If f₁ and f₂ have unequal order at x, then the trailing coefficient of f₁ + f₂ at x is the trailing coefficient of the function with the lowest order.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E} (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) : meromorphicTrailingCoeffAt (fun (z : 𝕜) => f₁ z + f₂ z) x = meromorphicTrailingCoeffAt f₁ x

If f₁ and f₂ have unequal order at x, then the trailing coefficient of f₁ + f₂ at x is the trailing coefficient of the function with the lowest order.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_left_of_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E} (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) : meromorphicTrailingCoeffAt (f₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x

If f₁ and f₂ have unequal order at x, then the trailing coefficient of f₁ - f₂ at x is the trailing coefficient of the function with the lowest order.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E} (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) : meromorphicTrailingCoeffAt (fun (z : 𝕜) => f₁ z - f₂ z) x = meromorphicTrailingCoeffAt f₁ x

If f₁ and f₂ have unequal order at x, then the trailing coefficient of f₁ - f₂ at x is the trailing coefficient of the function with the lowest order.

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

If f₁ and f₂ have equal order at x and if their trailing coefficients do not cancel, then the trailing coefficient of f₁ + f₂ at x is the sum of the trailing coefficients.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_add_eq_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) (h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x) (h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0) : meromorphicTrailingCoeffAt (fun (z : 𝕜) => f₁ z + f₂ z) x = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x

If f₁ and f₂ have equal order at x and if their trailing coefficients do not cancel, then the trailing coefficient of f₁ + f₂ at x is the sum of the trailing coefficients.

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

If f₁ and f₂ have equal order at x and if their trailing coefficients do not cancel, then the trailing coefficient of f₁ - f₂ at x is the sum of the trailing coefficients.

theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) (h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x) (h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0) : meromorphicTrailingCoeffAt (fun (z : 𝕜) => f₁ z - f₂ z) x = meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

If f₁ and f₂ have equal order at x and if their trailing coefficients do not cancel, then the trailing coefficient of f₁ - f₂ at x is the sum of the trailing coefficients.

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_fun_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 (fun (z : 𝕜) => f₁ z • f₂ z) 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 MeromorphicAt.meromorphicTrailingCoeffAt_fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f₁ f₂ : 𝕜 → 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) : meromorphicTrailingCoeffAt (fun (z : 𝕜) => f₁ z * f₂ z) x = meromorphicTrailingCoeffAt f₁ x * meromorphicTrailingCoeffAt f₂ x

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

theorem meromorphicTrailingCoeffAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜} (h : ∀ σ ∈ s, MeromorphicAt (f σ) x) : meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x

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

theorem meromorphicTrailingCoeffAt_fun_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜} (h : ∀ σ ∈ s, MeromorphicAt (f σ) x) : meromorphicTrailingCoeffAt (fun (z : 𝕜) => ∏ n ∈ s, f n z) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) 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 meromorphicTrailingCoeffAt_fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜} : meromorphicTrailingCoeffAt (fun (z : 𝕜) => (f z)⁻¹) 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_fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℤ} {f : 𝕜 → 𝕜} (h₁ : MeromorphicAt f x) : meromorphicTrailingCoeffAt (fun (z : 𝕜) => f z ^ 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.

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

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