Schwarz's lemma with prescribed zeros

Let f be analytic on a neighbourhood of the closed disc closedBall c T, bounded by M on the circle sphere c T, and vanishing to order at least k x at each point x of a finite set s inside the open disc. Dividing out the zeros, f = (∏ x ∈ s, (· - x) ^ k x) • g with g analytic, and the maximum modulus principle applied to g gives ‖f z‖ ≤ M * ∏ x ∈ s, (‖z - x‖ / (T - ‖x - c‖)) ^ k x on the closed disc.

When the zeros and the point z lie in the smaller disc closedBall c R with 3 * R ≤ T, every factor is at most 3 * R / T, so ‖f z‖ ≤ M * (3 * R / T) ^ ∑ x ∈ s, k x. This is the analytic estimate of transcendence proofs: an auxiliary function with many zeros in a small disc is very small there.

At a zero a ∈ s itself the same quotient controls the derivative of order k a: since f = (z - a) ^ k a • h with h = (∏ x ∈ s \ {a}, (· - x) ^ k x) • g, Leibniz's rule gives f⁽ᵏ⁽ᵃ⁾⁾(a) = (k a)! • h a. This bounds the first nonvanishing derivative of an auxiliary function at one of its zeros, as in Gelfond's proof of the Gelfond–Schneider theorem.

Main results

• TauCeti.norm_le_mul_prod_div_pow: the bound by the product over the zeros.
• TauCeti.norm_le_mul_three_mul_div_pow: the bound M * (3 * R / T) ^ ∑ x ∈ s, k x.
• TauCeti.norm_iteratedDeriv_le_mul_prod_div_pow: the bound for the derivative of order k a at a zero a ∈ s.

References

• J.-H. Evertse, Diophantine approximation, lecture notes (2019), ch. 4, §4.4, Lemma 4.26.
• M. Waldschmidt, Diophantine approximation on linear algebraic groups, Springer (2000), §2.2, Lemma 2.4.

theorem TauCeti.norm_le_mul_prod_div_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {T M : ℝ} {s : Finset ℂ} {k : ℂ → ℕ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c T)) (hk : ∀ x ∈ s, ↑(k x) ≤ analyticOrderAt f x) (hs : ↑s ⊆ Metric.ball c T) (hM : ∀ w ∈ Metric.sphere c T, ‖f w‖ ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall c T) : ‖f z‖ ≤ M * ∏ x ∈ s, (‖z - x‖ / (T - ‖x - c‖)) ^ k x

Schwarz's lemma with prescribed zeros. If f is analytic on a neighbourhood of closedBall c T, bounded by M on sphere c T, and vanishes to order at least k x at each point x of a finite set s ⊆ ball c T, then on closedBall c T ‖f z‖ ≤ M * ∏ x ∈ s, (‖z - x‖ / (T - ‖x - c‖)) ^ k x.

theorem TauCeti.norm_iteratedDeriv_le_mul_prod_div_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {T M : ℝ} {s : Finset ℂ} {k : ℂ → ℕ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c T)) (hk : ∀ x ∈ s, ↑(k x) ≤ analyticOrderAt f x) (hs : ↑s ⊆ Metric.ball c T) (hM : ∀ w ∈ Metric.sphere c T, ‖f w‖ ≤ M) {a : ℂ} (ha : a ∈ s) : ‖iteratedDeriv (k a) f a‖ ≤ ↑(k a).factorial * M / (T - ‖a - c‖) ^ k a * ∏ x ∈ s.erase a, (‖a - x‖ / (T - ‖x - c‖)) ^ k x

Schwarz's lemma for the first nonvanishing derivative. If f is analytic on a neighbourhood of closedBall c T, bounded by M on sphere c T, and vanishes to order at least k x at each point x of a finite set s ⊆ ball c T, then at every a ∈ s ‖f⁽ᵏ⁽ᵃ⁾⁾(a)‖ ≤ k(a)! M / (T - ‖a - c‖) ^ k(a) * ∏ x ∈ s \ {a}, (‖a - x‖ / (T - ‖x - c‖)) ^ k x.

theorem TauCeti.norm_le_mul_three_mul_div_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {T M : ℝ} {s : Finset ℂ} {k : ℂ → ℕ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c T)) (hk : ∀ x ∈ s, ↑(k x) ≤ analyticOrderAt f x) (hs : ↑s ⊆ Metric.closedBall c R) (hRT : 3 * R ≤ T) (hM : ∀ w ∈ Metric.sphere c T, ‖f w‖ ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall c R) : ‖f z‖ ≤ M * (3 * R / T) ^ ∑ x ∈ s, k x

Schwarz's lemma with prescribed zeros, in the form M * (3 * R / T) ^ ∑ x ∈ s, k x. If f is analytic on a neighbourhood of closedBall c T, bounded by M on sphere c T, and vanishes to order at least k x at each point x of a finite set s ⊆ closedBall c R, where 3 * R ≤ T, then ‖f z‖ ≤ M * (3 * R / T) ^ ∑ x ∈ s, k x on closedBall c R.