Meromorphic API for the Logarithmic Derivative

Arithmetic on Codiscrete Sets

The pointwise lemma logDeriv_mul requires differentiability and nonvanishing of the factors at the point in question. For meromorphic functions whose order is nowhere ⊤, both conditions hold away from a codiscrete set, turning the pointwise arithmetic into arithmetic of codiscrete equivalence classes.

theorem MeromorphicOn.logDeriv_mul_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} {U : Set 𝕜} (hf : MeromorphicOn f U) (hg : MeromorphicOn g U) (h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤) (h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤) : logDeriv (f * g) =ᶠ[Filter.codiscreteWithin U] logDeriv f + logDeriv g

The logarithmic derivative converts products into sums: away from a codiscrete subset of U, the logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic derivatives.

theorem MeromorphicOn.logDeriv_fun_mul_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} {U : Set 𝕜} (hf : MeromorphicOn f U) (hg : MeromorphicOn g U) (h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤) (h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤) : (logDeriv fun (i : 𝕜) => f i * g i) =ᶠ[Filter.codiscreteWithin U] fun (i : 𝕜) => logDeriv f i + logDeriv g i

Eta-expanded form of MeromorphicOn.logDeriv_mul_eventuallyEq

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of U, the logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic derivatives.

theorem Meromorphic.logDeriv_mul_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} (hf : Meromorphic f) (hg : Meromorphic g) (h'f : ∀ (x : 𝕜), meromorphicOrderAt f x ≠ ⊤) (h'g : ∀ (x : 𝕜), meromorphicOrderAt g x ≠ ⊤) : logDeriv (f * g) =ᶠ[Filter.codiscrete 𝕜] logDeriv f + logDeriv g

The logarithmic derivative converts products into sums: away from a codiscrete subset of 𝕜, the logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic derivatives.

theorem Meromorphic.logDeriv_fun_mul_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} (hf : Meromorphic f) (hg : Meromorphic g) (h'f : ∀ (x : 𝕜), meromorphicOrderAt f x ≠ ⊤) (h'g : ∀ (x : 𝕜), meromorphicOrderAt g x ≠ ⊤) : (logDeriv fun (i : 𝕜) => f i * g i) =ᶠ[Filter.codiscrete 𝕜] fun (i : 𝕜) => logDeriv f i + logDeriv g i

Eta-expanded form of Meromorphic.logDeriv_mul_eventuallyEq

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of 𝕜, the logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic derivatives.

theorem MeromorphicOn.logDeriv_prod_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'} (h : ∀ i ∈ s, MeromorphicOn (F i) U) (h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) : logDeriv (∏ i ∈ s, F i) =ᶠ[Filter.codiscreteWithin U] ∑ i ∈ s, logDeriv (F i)

The logarithmic derivative converts products into sums: away from a codiscrete subset of U, the logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic derivatives.

theorem MeromorphicOn.logDeriv_fun_prod_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'} (h : ∀ i ∈ s, MeromorphicOn (F i) U) (h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) : (logDeriv fun (a : 𝕜) => ∏ c ∈ s, F c a) =ᶠ[Filter.codiscreteWithin U] fun (a : 𝕜) => ∑ c ∈ s, logDeriv (F c) a

Eta-expanded form of MeromorphicOn.logDeriv_prod_eventuallyEq

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of U, the logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic derivatives.

theorem Meromorphic.logDeriv_prod_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'} (h : ∀ i ∈ s, Meromorphic (F i)) (h' : ∀ i ∈ s, ∀ (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) : logDeriv (∏ i ∈ s, F i) =ᶠ[Filter.codiscrete 𝕜] ∑ i ∈ s, logDeriv (F i)

The logarithmic derivative converts products into sums: away from a codiscrete subset of 𝕜, the logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic derivatives.

theorem Meromorphic.logDeriv_fun_prod_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {s : Finset ι} {F : ι → 𝕜 → 𝕜'} (h : ∀ i ∈ s, Meromorphic (F i)) (h' : ∀ i ∈ s, ∀ (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) : (logDeriv fun (a : 𝕜) => ∏ c ∈ s, F c a) =ᶠ[Filter.codiscrete 𝕜] fun (a : 𝕜) => ∑ c ∈ s, logDeriv (F c) a

Eta-expanded form of Meromorphic.logDeriv_prod_eventuallyEq

---

The logarithmic derivative converts products into sums: away from a codiscrete subset of 𝕜, the logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic derivatives.

theorem MeromorphicOn.logDeriv_finprod_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {F : ι → 𝕜 → 𝕜'} (hF : (Function.mulSupport F).Finite) (h : ∀ (i : ι), MeromorphicOn (F i) U) (h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) : logDeriv (∏ᶠ (i : ι), F i) =ᶠ[Filter.codiscreteWithin U] ∑ᶠ (i : ι), logDeriv (F i)

The logarithmic derivative converts products into sums: away from a codiscrete subset of U, the logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic derivatives.

theorem Meromorphic.logDeriv_finprod_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {F : ι → 𝕜 → 𝕜'} (hF : (Function.mulSupport F).Finite) (h : ∀ (i : ι), Meromorphic (F i)) (h' : ∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) : logDeriv (∏ᶠ (i : ι), F i) =ᶠ[Filter.codiscrete 𝕜] ∑ᶠ (i : ι), logDeriv (F i)

The logarithmic derivative converts products into sums: away from a codiscrete subset of 𝕜, the logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic derivatives.

theorem MeromorphicOn.logDeriv_zpow_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {U : Set 𝕜} (hf : MeromorphicOn f U) (n : ℤ) : logDeriv (f ^ n) =ᶠ[Filter.codiscreteWithin U] n • logDeriv f

Away from a codiscrete subset of U, the logarithmic derivative of the n-th power of a meromorphic function is n times the logarithmic derivative.

theorem MeromorphicOn.logDeriv_fun_zpow_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {U : Set 𝕜} (hf : MeromorphicOn f U) (n : ℤ) : (logDeriv fun (i : 𝕜) => f i ^ n) =ᶠ[Filter.codiscreteWithin U] fun (i : 𝕜) => n • logDeriv f i

Eta-expanded form of MeromorphicOn.logDeriv_zpow_eventuallyEq

---

Away from a codiscrete subset of U, the logarithmic derivative of the n-th power of a meromorphic function is n times the logarithmic derivative.

theorem Meromorphic.logDeriv_zpow_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} (hf : Meromorphic f) (n : ℤ) : logDeriv (f ^ n) =ᶠ[Filter.codiscrete 𝕜] n • logDeriv f

Away from a codiscrete subset of 𝕜, the logarithmic derivative of the n-th power of a meromorphic function is n times the logarithmic derivative.

theorem Meromorphic.logDeriv_fun_zpow_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} (hf : Meromorphic f) (n : ℤ) : (logDeriv fun (i : 𝕜) => f i ^ n) =ᶠ[Filter.codiscrete 𝕜] fun (i : 𝕜) => n • logDeriv f i

Eta-expanded form of Meromorphic.logDeriv_zpow_eventuallyEq

---

Away from a codiscrete subset of 𝕜, the logarithmic derivative of the n-th power of a meromorphic function is n times the logarithmic derivative.

theorem MeromorphicOn.logDeriv_finprod_zpow_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {F : ι → 𝕜 → 𝕜'} {d : ι → ℤ} (hd : (Function.support d).Finite) (h : ∀ (i : ι), MeromorphicOn (F i) U) (h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) : logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[Filter.codiscreteWithin U] fun (z : 𝕜) => ∑ᶠ (i : ι), d i • logDeriv (F i) z

The logarithmic derivative converts products into sums: away from a codiscrete subset of U, the logarithmic derivative of a finite product of integer powers of meromorphic functions is the corresponding weighted sum of logarithmic derivatives. This is the shape of statement used in the differentiated Poisson–Jensen formula, where the exponents are given by a divisor.

theorem Meromorphic.logDeriv_finprod_zpow_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {F : ι → 𝕜 → 𝕜'} {d : ι → ℤ} (hd : (Function.support d).Finite) (h : ∀ (i : ι), Meromorphic (F i)) (h' : ∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤) : logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[Filter.codiscrete 𝕜] fun (z : 𝕜) => ∑ᶠ (i : ι), d i • logDeriv (F i) z

The logarithmic derivative converts products into sums: away from a codiscrete subset of 𝕜, the logarithmic derivative of a finite product of integer powers of meromorphic functions is the corresponding weighted sum of logarithmic derivatives. This is the shape of statement used in the differentiated Poisson–Jensen formula, where the exponents are given by a divisor.