Dividing an analytic function by prescribed zeros

If an analytic function f vanishes to order at least k x at each point x of a finite set s, then f factors globally as f z = (∏ x ∈ s, (z - x) ^ k x) • g z, where g is analytic wherever f is. The quotient g is obtained by repeatedly taking divided differences dslope · x, each of which lowers the order of vanishing at x by one (AnalyticAt.analyticOrderAt_dslope_add_one).

Over ℂ this is the factorization of an entire function with zeros of prescribed multiplicities used in transcendence proofs, where g is then estimated by the maximum modulus principle. The order hypotheses may be given as vanishing of derivatives through Mathlib's natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero.

Main results

• HasFPowerSeriesAt.iterate_dslope_apply_eq_coeff: the iterated divided differences of f at a take the Taylor coefficients of f at a as their values at a.
• TauCeti.iterate_dslope_apply_eq_zero_of_lt: if f vanishes to order at least n at a, then the first n iterated divided differences of f at a vanish at a.
• AnalyticOnNhd.exists_eq_prod_pow_smul: an analytic function with zeros of orders at least k x at the points x ∈ s is ∏ x ∈ s, (z - x) ^ k x times an analytic function.
• TauCeti.differentiableAt_of_eventuallyEq_div: the removable singularity of a quotient A / B of two functions analytic and vanishing at a, with deriv B a = b ≠ 0 and deriv A a = c * b, is differentiable once filled by the value c.

References

• J.-H. Evertse, Diophantine approximation, lecture notes (2019), ch. 4, §4.4, Lemma 4.24.

theorem AnalyticAt.iterate_dslope {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a z : 𝕜} (hf : AnalyticAt 𝕜 f z) (n : ℕ) : AnalyticAt 𝕜 ((Function.swap dslope a)^[n] f) z

Iterated divided differences at a preserve analyticity at every point where f is analytic.

theorem HasFPowerSeriesAt.iterate_dslope_apply_eq_coeff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {p : FormalMultilinearSeries 𝕜 𝕜 E} {z₀ : 𝕜} (hp : HasFPowerSeriesAt f p z₀) (n : ℕ) : (Function.swap dslope z₀)^[n] f z₀ = p.coeff n

The n-th iterated divided difference at z₀ of a function with power series p at z₀ takes the value p.coeff n at z₀: these values are the Taylor coefficients.

theorem TauCeti.differentiableAt_of_eventuallyEq_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {A B H : 𝕜 → 𝕜} {c b : 𝕜} (hA : AnalyticAt 𝕜 A a) (hB : AnalyticAt 𝕜 B a) (hA₀ : A a = 0) (hB₀ : B a = 0) (hdA : HasDerivAt A (c * b) a) (hdB : HasDerivAt B b a) (hb : b ≠ 0) (hHa : H a = c) (hH : ∀ᶠ (x : 𝕜) in nhdsWithin a {a}ᶜ, H x = A x / B x) : DifferentiableAt 𝕜 H a

Removable singularity of a quotient of analytic functions with a simple zero. If A and B are analytic and vanish at a, with deriv A a = c * b and deriv B a = b ≠ 0, then every function H with H a = c that equals A / B on a punctured neighbourhood of a is differentiable at a.

theorem TauCeti.iterate_dslope_apply_eq_zero_of_lt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {n k : ℕ} (hn : ↑n ≤ analyticOrderAt f a) (hk : k < n) : (Function.swap dslope a)^[k] f a = 0

If f vanishes to order at least n at a, then each of the first n iterated divided differences (swap dslope a)^[k] f, k < n, vanishes at a.

theorem AnalyticOnNhd.exists_eq_prod_pow_smul {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (s : Finset 𝕜) (k : 𝕜 → ℕ) (hk : ∀ x ∈ s, ↑(k x) ≤ analyticOrderAt f x) : ∃ (g : 𝕜 → E), AnalyticOnNhd 𝕜 g U ∧ ∀ (z : 𝕜), f z = (∏ x ∈ s, (z - x) ^ k x) • g z

Division by prescribed zeros. If f is analytic on a neighbourhood of U and vanishes to order at least k x at each point x of a finite set s, then f z = (∏ x ∈ s, (z - x) ^ k x) • g z for all z and some g analytic on a neighbourhood of U.