Maximum modulus definition

theorem Hadamard.summable_sigma_inv_norm_pow_of_weighted {ι : Type u_1} {z : ι → ℂ} {m : ι → ℕ} {q : ℕ} (hsum : Summable fun (i : ι) => ↑(m i) / ‖z i‖ ^ q) : Summable fun (j : (i : ι) × Fin (m i)) => 1 / ‖z j.fst‖ ^ q

Convert a multiplicity-weighted inverse-norm sum to a sum over repeated indices.

noncomputable def Hadamard.maxModulus (f : ℂ → ℂ) (r : ℝ) : ℝ

The maximum modulus of f on the circle of radius r. M(f,r) = sup {|f(z)| : |z| = r}

Equations

• Hadamard.maxModulus f r = sSup {y : ℝ | ∃ (z : ℂ), ‖z‖ = r ∧ y = ‖f z‖}

Helper lemmas for subsequence growth and exp/log monotonicity

theorem Hadamard.norm_le_maxModulus_on_circle (f : ℂ → ℂ) (hf : Continuous f) {r : ℝ} {z : ℂ} (hz : ‖z‖ = r) : ‖f z‖ ≤ maxModulus f r

On a circle ‖z‖ = r, the pointwise value is bounded by the maximal modulus M(f,r).

This follows directly from the definition of maxModulus as a supremum over the circle.

theorem Hadamard.maxModulus_le_of_forall_norm_le (f : ℂ → ℂ) (_hf : Continuous f) {r A : ℝ} (hr : 0 ≤ r) (hA : ∀ (z : ℂ), ‖z‖ = r → ‖f z‖ ≤ A) : maxModulus f r ≤ A

If all pointwise values on the circle ‖z‖ = r are bounded by A, then maxModulus f r ≤ A.

theorem Hadamard.norm_le_maxModulus_of_norm_le (f : ℂ → ℂ) (hf : Differentiable ℂ f) {R : ℝ} (_hR : 0 < R) {w : ℂ} (hw : ‖w‖ ≤ R) : ‖f w‖ ≤ maxModulus f R

Maximum modulus principle (specialized): values on the closed disk ‖z‖ ≤ R are bounded by maxModulus f R.

theorem Hadamard.maxModulus_mono_of_differentiable (f : ℂ → ℂ) (hf : Differentiable ℂ f) {r R : ℝ} (hR : 0 < R) (hr : 0 ≤ r) (h : r ≤ R) : maxModulus f r ≤ maxModulus f R

The maximum modulus M(f,r) is monotone in r for entire functions.

theorem Hadamard.re_le_of_norm_exp_le {w : ℂ} {t : ℝ} (h : ‖Complex.exp w‖ ≤ Real.exp t) : w.re ≤ t

If ‖exp w‖ ≤ exp t then Re w ≤ t.

theorem Hadamard.re_lt_of_norm_exp_lt {w : ℂ} {t : ℝ} (h : ‖Complex.exp w‖ < Real.exp t) : w.re < t

If ‖exp w‖ < exp t then Re w < t.

Order of growth

noncomputable def Hadamard.order (f : ℂ → ℂ) : ℝ

Definition 1.1: The order of growth of an entire function

Definition: The infimum of ρ₀ such that |f(z)| < exp(|z|^ρ₀) for |z| ≥ R₀

Lemma 1.2. Let f be an entire function of finite order. ρ(f) = lim sup_{r≥R→∞} (log log M(f,r)) / log(r) where M(f,r) = max_{|z|=r} |f(z)|

Equations

• Hadamard.order f = Filter.limsup (fun (r : ℝ) => if r > 0 ∧ Hadamard.maxModulus f r > 1 then Real.log (Real.log (Hadamard.maxModulus f r)) / Real.log r else 0) Filter.atTop

theorem Hadamard.maxModulus_subseq_bound_of_order (f : ℂ → ℂ) (ρ ε : ℝ) (hε : 0 < ε) (hord : order f = ρ) (hu_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (r : ℝ) => if r > 0 ∧ maxModulus f r > 1 then Real.log (Real.log (maxModulus f r)) / Real.log r else 0) : ∃ (r0 : ℕ → ℝ), Filter.Tendsto r0 Filter.atTop Filter.atTop ∧ (∀ (n : ℕ), 0 < r0 n) ∧ ∀ (n : ℕ), maxModulus f (r0 n) ≤ Real.exp (r0 n ^ (ρ + ε))

From order f = ρ, one can choose radii along which the maximal modulus is bounded by exp(r^(ρ+ε)). This is the standard subsequence extraction from the limsup definition.

Definitions

Definition 1.1. An entire function f is finite order if and only if ∃ρ₀, R₀ such that |f(z)| < exp(|z|^ρ₀) whenever |z| ≥ R₀. The infimum of such ρ₀ is called the order of f and is denoted by ρ = ρ(f).

Definition 2.1. Let f be an entire function with zeros {a₁, a₂,...}, repeated according to multiplicity and arranged such that |a₁| ≤ |a₂| ≤ ....

Then f is of finite rank if there is an integer p such that ∑ |aₙ|^{-p-1} < ∞ If p is the smallest integer such that this occurs, then f is said to be of rank p; a function with only a finite number of zeros has rank 0.

The order of an entire function f is defined as: ρ(f) = lim sup_{r→∞} (log log M(f,r))/(log r) where M(f,r) = max_{|z|=r} |f(z)|

def Hadamard.hasFiniteOrder (f : ℂ → ℂ) : Prop

An entire function has finite order if there exist ρ₀, R₀ such that |f(z)| < exp(|z|^ρ₀) whenever |z| ≥ R₀

Equations

• Hadamard.hasFiniteOrder f = (Differentiable ℂ f ∧ ∃ (ρ₀ : ℝ) (R₀ : ℝ), ∀ (z : ℂ), R₀ ≤ ‖z‖ → ‖f z‖ < Real.exp (‖z‖ ^ ρ₀))

theorem Hadamard.hasFiniteOrder_mul (f g : ℂ → ℂ) (hf : hasFiniteOrder f) (hg : hasFiniteOrder g) : hasFiniteOrder (f * g)

Product of entire functions preserves finite order

noncomputable def Hadamard.weierstrassE (p : ℕ) (w : ℂ) : ℂ

Weierstrass elementary factors: E₀(z) = 1 - z Eₚ(z) = (1-z) exp(z + z²/2 + ... + z^p/p) for p ≥ 1

The canonical product is: P(z) = ∏ₙ Eₚₙ(z/aₙ) where {pₙ} is chosen so that ∑ |aₙ|^{-pₙ-1} < ∞

Weierstrass elementary factors where: E_p(w) = (1-w)exp(w + w²/2 + ... + w^p/p) These appear in the canonical product representation.

Equations

• Hadamard.weierstrassE p w = (1 - w) * Complex.exp (∑ k ∈ Finset.range p, w ^ (k + 1) / (↑k + 1))

theorem Hadamard.weierstrass_E_zero (w : ℂ) : weierstrassE 0 w = 1 - w

theorem Hadamard.weierstrass_E_one (w : ℂ) : weierstrassE 1 w = (1 - w) * Complex.exp w

theorem Hadamard.weierstrass_E_at_one (p : ℕ) : weierstrassE p 1 = 0

theorem Hadamard.weierstrass_E_eq_zero_iff_general (p : ℕ) (w : ℂ) : weierstrassE p w = 0 ↔ w = 1

theorem Hadamard.weierstrass_E_ne_zero_general (p : ℕ) {w : ℂ} (hw : w ≠ 1) : weierstrassE p w ≠ 0

theorem Hadamard.weierstrass_E_one_eq_zero_iff (w : ℂ) : weierstrassE 1 w = 0 ↔ w = 1

theorem Hadamard.weierstrass_E_one_ne_zero (w : ℂ) (hw : w ≠ 1) : weierstrassE 1 w ≠ 0

theorem Hadamard.weierstrass_E_zero_arg (p : ℕ) : weierstrassE p 0 = 1

theorem Hadamard.weierstrass_E_continuous (p : ℕ) : Continuous (weierstrassE p)

theorem Hadamard.weierstrass_E_differentiable (p : ℕ) : Differentiable ℂ (weierstrassE p)

theorem Hadamard.deriv_weierstrass_E_at_one_ne_zero (p : ℕ) : deriv (weierstrassE p) 1 ≠ 0

E_p'(1) ≠ 0 for all p.

Concretely, E_p'(1) = -exp(H_p) where H_p = ∑_{k=1}^p 1/k (the p-th harmonic number), which is nonzero since exp never vanishes.

theorem Hadamard.weierstrass_E_analyticOrderAt_one (p : ℕ) : analyticOrderAt (weierstrassE p) 1 = 1

E_p has a simple zero at 1 for all p.

theorem Hadamard.weierstrass_E_analyticOrderNatAt_one (p : ℕ) : analyticOrderNatAt (weierstrassE p) 1 = 1

E_p has analyticOrderNatAt equal to 1 at w = 1.

Key Lemmas

The proof of Hadamard's theorem proceeds through several key technical lemmas.

Canonical Product

noncomputable def Hadamard.canonicalProductPartial (d : ℕ) (zeros : ℕ → ℂ) (s : Finset ℕ) (z : ℂ) : ℂ

Finite partial product for the canonical product.

Equations

• Hadamard.canonicalProductPartial d zeros s z = ∏ n ∈ s, Hadamard.weierstrassE d (z / zeros n)

noncomputable def Hadamard.canonicalProduct (d : ℕ) (zeros : ℕ → ℂ) (z : ℂ) : ℂ

The Weierstrass canonical product (over all indices).

Equations

• Hadamard.canonicalProduct d zeros z = ∏' (n : ℕ), Hadamard.weierstrassE d (z / zeros n)

@[simp]

theorem Hadamard.canonicalProductPartial_empty (d : ℕ) (zeros : ℕ → ℂ) (z : ℂ) : canonicalProductPartial d zeros ∅ z = 1

@[simp]

theorem Hadamard.canonicalProduct_at_zero (d : ℕ) (zeros : ℕ → ℂ) : canonicalProduct d zeros 0 = 1

theorem Hadamard.order_formula (f : ℂ → ℂ) (_hf : hasFiniteOrder f) : order f = Filter.limsup (fun (r : ℝ) => if r > 0 ∧ maxModulus f r > 1 then Real.log (Real.log (maxModulus f r)) / Real.log r else 0) Filter.atTop

Lemma 1.2: Order formula using log log M(f,r)

Lemma 1.2. Let f be an entire function of finite order. ρ(f) = lim sup_{R→∞,r≥R} (loglogM(f,r))/log(r) where M(f,r) = max_{|z|=r} |f(z)|.

Proof. If f is finite order, M(f,r) ≤ exp(r^ρ₀) ⟹ log M(f,r) ≤ r^ρ₀ ⟹ log log M(f,r) ≤ ρ₀ log(r)

So we have lim_{R→∞} lim_{r≥R} (loglogM(f,r))/log r ≤ ρ₀.

Harmonic Function Theory

The harmonic function theory needed for Borel-Carathéodory has been moved to a separate file: Rh.HarmonicFunctionality

That file contains:

• AnalyticAt.harmonicAt_of_complex: Complex-analytic functions are harmonic
• re_of_holomorphic_is_harmonic: Real part of holomorphic is harmonic
• im_of_holomorphic_is_harmonic: Imaginary part of holomorphic is harmonic
• TODO markers for Mean Value Property, Maximum Principle, Poisson Formula, Harnack's Inequality

We import and open that namespace above, so all lemmas are available here.

Borel-Carathéodory Theorem

theorem Hadamard.borel_caratheodory_point (g : ℂ → ℂ) (R r : ℝ) (h_R : 0 < R) (h_r : r < R) (h_holo : ∀ (z : ℂ), ‖z‖ ≤ R → DifferentiableAt ℂ g z) (h_bdd : BddAbove {x : ℝ | ∃ (ζ : ℂ), ‖ζ‖ = R ∧ x = (g ζ).re}) (z : ℂ) : ‖z‖ ≤ r → ‖g z‖ ≤ 2 * r / (R - r) * (LZCBorelCaratheodory.boundaryRealSup g R - (g 0).re) + ‖g 0‖

Pointwise Borel–Carathéodory inequality, used as an ingredient in the logarithmic-derivative estimates of Titchmarsh §3.9.

theorem Hadamard.cauchy_estimate_iteratedDeriv_at_zero (g : ℂ → ℂ) {R M : ℝ} (hR : 0 < R) (hg : DiffContOnCl ℂ g (Metric.ball 0 R)) (hM : ∀ z ∈ Metric.sphere 0 R, ‖g z‖ ≤ M) (n : ℕ) : ‖iteratedDeriv n g 0‖ ≤ ↑n.factorial * M / R ^ n

Cauchy estimates at the origin for higher derivatives.

If g is complex-differentiable on the open disk of radius R > 0 and continuous on its closure, and ‖g z‖ ≤ M for every z on the circle ‖z‖ = R, then for all n ≥ 0 we have ‖iteratedDeriv n g 0‖ ≤ n! * M / R^n.

We combine the Cauchy integral representation for the power series coefficients (DiffContOnCl.hasFPowerSeriesOnBall) with the norm bound on the circle (norm_cauchyPowerSeries_le) and relate the coefficient to the iterated derivative via HasFPowerSeriesOnBall.factorial_smul.

theorem Hadamard.polynomial_from_growth (g : ℂ → ℂ) (ρ : ℝ) (hρ : 0 ≤ ρ) (h_entire : Differentiable ℂ g) (h_growth : ∀ ε > 0, ∃ (r_seq : ℕ → ℝ), Filter.Tendsto r_seq Filter.atTop Filter.atTop ∧ ∀ (n : ℕ) (z : ℂ), ‖z‖ = r_seq n → (g z).re < ‖z‖ ^ (ρ + ε)) : ∃ (p : Polynomial ℂ), (∀ (z : ℂ), g z = Polynomial.eval z p) ∧ ↑p.natDegree ≤ ρ

Theorem 2.3: If Re g(z) = O(r^ρ), then g is a polynomial of degree ≤ ρ

Theorem 2.3. Let g: ℂ → ℂ be entire. If for all ε > 0 there exists a sequence {rₙ} with rₙ → ∞ such that Re g(z) < r^{ρ+ε} whenever |z| = rₙ, then g(z) is a polynomial of degree ≤ ρ.

Theorem 2.3 is equivalent to saying: if for all ε > 0 there exists some rₙ → ∞ such that Re g(z) < rₙ^{ρ+ε} whenever |z| = rₙ, then g(z) is a polynomial of degree at most ρ. The sequence rₙ is necessary to avoid weird behavior at particular radii in applications.

Proof. By the Borel-Carathéodory inequality, for 0 < r < R, max_{|z|≤r} |g(z)| ≤ (2r)/(R-r) · max_{|z|=R} Re g(z) + |g(0)|

By Liouville's Theorem (the souped-up version) g(z) must be a polynomial of degree less than or equal to ρ.

theorem Hadamard.circleAverage_of_analytic (g : ℂ → ℂ) (R : ℝ) (hR : 0 < R) (hg : DiffContOnCl ℂ g (Metric.ball 0 R)) : Real.circleAverage g 0 R = g 0

Circle average of an analytic function equals its center value.

If g is complex differentiable on the open ball ball 0 R and continuous on its closure (DiffContOnCl), then its circle average on |z| = R equals g 0.

theorem Hadamard.circleAverage_log_norm_of_hasLog (f g : ℂ → ℂ) (R : ℝ) (hR : 0 < R) (hg : DiffContOnCl ℂ g (Metric.ball 0 R)) (hexp : ∀ (z : ℂ), ‖z‖ ≤ R → f z = Complex.exp (g z)) : Real.circleAverage (fun (z : ℂ) => Real.log ‖f z‖) 0 R = Real.log ‖f 0‖

If a branch g of the logarithm exists on the closed disk, the circle average of log ‖f‖ equals log ‖f(0)‖.

theorem Hadamard.blaschke_on_sphere_norm_one (a z : ℂ) (R : ℝ) (hz : ‖z‖ = R) (ha : ‖a‖ < R) : ‖(↑R ^ 2 - (starRingEnd ℂ) a * z) / (↑R * (z - a))‖ = 1

On the circle |z|=R, the elementary factor B_a(z) = (R^2 - conj a * z)/(R (z - a)) has unit modulus.

theorem Hadamard.jensen_formula (f : ℂ → ℂ) (R : ℝ) (hR : 0 < R) (_h_holo : ∀ (z : ℂ), ‖z‖ ≤ R → DifferentiableAt ℂ f z) (_h_nozeros_boundary : ∀ (z : ℂ), ‖z‖ = R → f z ≠ 0) (h_nonzero_0 : f 0 ≠ 0) (zeros : Finset ℂ) (h_zeros : ∀ a ∈ zeros, f a = 0 ∧ ‖a‖ < R) (h_logF : ∃ (g : ℂ → ℂ), DiffContOnCl ℂ g (Metric.ball 0 R) ∧ ∀ (z : ℂ), ‖z‖ ≤ R → f z * ∏ a ∈ zeros, (↑R ^ 2 - (starRingEnd ℂ) a * z) / (↑R * (z - a)) = Complex.exp (g z)) : Real.log ‖f 0‖ = -∑ a ∈ zeros, Real.log (R / ‖a‖) + Real.circleAverage (fun (z : ℂ) => Real.log ‖f z‖) 0 R

theorem Hadamard.finite_sum_pow_bound (z : ℂ) (h : ℕ) (hz : ‖z‖ ≤ 1) : ‖∑ k ∈ Finset.range h, z ^ (k + 1) / (↑k + 1)‖ ≤ ↑h * ‖z‖

Helper: Finite sum bound for |z| ≤ 1

theorem Hadamard.logTaylor_neg_eq_neg_sum (h : ℕ) (z : ℂ) : Complex.logTaylor (h + 1) (-z) = -∑ k ∈ Finset.range h, z ^ (k + 1) / (↑k + 1)

theorem Hadamard.weierstrass_E_small_disk_lower_bound (h : ℕ) : ∃ (C : ℝ), ∀ (z : ℂ), ‖z‖ ≤ 1 / 2 → Real.log ‖weierstrassE h z‖ ≥ -C * ‖z‖ ^ (h + 1)

theorem Hadamard.weierstrass_E_small_disk_norm_sub_one_le (h : ℕ) (z : ℂ) : ‖z‖ ≤ 1 / 2 → ‖weierstrassE h z - 1‖ ≤ 4 * ‖z‖ ^ (h + 1)

theorem Hadamard.weierstrass_E_small_disk_log_norm_le (h : ℕ) (z : ℂ) (hz : ‖z‖ ≤ 1 / 2) : Real.log ‖weierstrassE h z‖ ≤ 4 * ‖z‖ ^ (h + 1)

Weierstrass products (Conway Ch. 7 §5)

Conway’s Theorem 5.9 / 5.12 show that if ∑ ‖fₙ(z) - 1‖ converges absolutely and uniformly on compacts, then ∏ fₙ converges uniformly on compacts to an analytic function.

In Mathlib, we use Summable.hasProdLocallyUniformlyOn_nat_one_add (from Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn) to package the convergence of products of the form ∏ (1 + gₙ z). Our elementary-factor estimate weierstrass_E_small_disk_norm_sub_one_le is a (slightly weaker) analogue of Conway’s Lemma 5.11.

theorem Hadamard.weierstrass_product_hasProdLocallyUniformlyOn (a : ℕ → ℂ) (p : ℕ → ℕ) (u : ℕ → ℝ) (hu : Summable u) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (z : ℂ), ‖weierstrassE (p n) (z / a n) - 1‖ ≤ u n) : HasProdLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) => weierstrassE (p n) (z / a n)) (fun (z : ℂ) => ∏' (n : ℕ), weierstrassE (p n) (z / a n)) Set.univ

theorem Hadamard.differentiableOn_weierstrass_product (a : ℕ → ℂ) (p : ℕ → ℕ) (u : ℕ → ℝ) (hu : Summable u) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (z : ℂ), ‖weierstrassE (p n) (z / a n) - 1‖ ≤ u n) : DifferentiableOn ℂ (fun (z : ℂ) => ∏' (n : ℕ), weierstrassE (p n) (z / a n)) Set.univ

A Conway-style convergence criterion (Theorem 5.12)

The previous lemmas assume a global summable bound on ‖Eₚ(z/aₙ) - 1‖. In applications one only has such bounds on compact sets, using that ‖aₙ‖ → ∞. The next lemma packages this common case: on each compact K we use the bound ‖z‖ ≤ R and the elementary estimate weierstrass_E_small_disk_norm_sub_one_le.

theorem Hadamard.weierstrass_product_hasProdLocallyUniformlyOn_of_tendsto_norm_atTop (a : ℕ → ℂ) (p : ℕ → ℕ) (ha : Filter.Tendsto (fun (n : ℕ) => ‖a n‖) Filter.atTop Filter.atTop) (hsum : ∀ (R : ℝ), 0 < R → Summable fun (n : ℕ) => (R / ‖a n‖) ^ (p n + 1)) : HasProdLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) => weierstrassE (p n) (z / a n)) (fun (z : ℂ) => ∏' (n : ℕ), weierstrassE (p n) (z / a n)) Set.univ

theorem Hadamard.differentiableOn_weierstrass_product_of_tendsto_norm_atTop (a : ℕ → ℂ) (p : ℕ → ℕ) (ha : Filter.Tendsto (fun (n : ℕ) => ‖a n‖) Filter.atTop Filter.atTop) (hsum : ∀ (R : ℝ), 0 < R → Summable fun (n : ℕ) => (R / ‖a n‖) ^ (p n + 1)) : DifferentiableOn ℂ (fun (z : ℂ) => ∏' (n : ℕ), weierstrassE (p n) (z / a n)) Set.univ

Away from the zero at 1: on {‖z‖ ≥ 1 / 2, ‖z-1‖ ≥ δ}, log ‖E_h(z)‖ ≥ -C(δ)‖z‖^h.

theorem Hadamard.weierstrass_E_away_from_one_lower_bound_explicit (h : ℕ) (δ : ℝ) (hδ : 0 < δ) (z : ℂ) : 1 / 2 ≤ ‖z‖ → δ ≤ ‖z - 1‖ → Real.log ‖weierstrassE h z‖ ≥ -(2 ^ h * (↑h + |Real.log δ|) * ‖z‖ ^ h)

Explicit version of Hadamard.weierstrass_E_away_from_one_lower_bound, with the concrete witness 2^h * (h + |log δ|).

theorem Hadamard.weierstrass_E_away_from_one_lower_bound (h : ℕ) (δ : ℝ) (hδ : 0 < δ) : ∃ (C : ℝ), ∀ (z : ℂ), 1 / 2 ≤ ‖z‖ → δ ≤ ‖z - 1‖ → Real.log ‖weierstrassE h z‖ ≥ -C * ‖z‖ ^ h

Main Theorems

theorem Hadamard.entire_no_zeros_is_exp_polynomial (f : ℂ → ℂ) (ρ : ℝ) (h_finite_order : hasFiniteOrder f) (h_order : order f = ρ) (h_no_zeros : ∀ (z : ℂ), f z ≠ 0) : ∃ (g : Polynomial ℂ), (∀ (z : ℂ), f z = Complex.exp (Polynomial.eval z g)) ∧ ↑g.natDegree ≤ ρ

Step 1: Entire functions without zeros are exponentials of polynomials

Prove this for entire function f(z) without zeros: by existence of logarithms we know f(z) = e^{g(z)}.

We show g(z) is a polynomial (This involves the so-called Borel-Carathéodory inequality).

Proof sketch:

1. Since f has no zeros and is entire, we can write f = e^g for some entire g
2. We have |f(z)| < exp(|z|^ρ) by finite order assumption
3. So e^{Re g(z)} < exp(|z|^ρ), thus Re g(z) < |z|^ρ
4. By polynomial_from_growth, g is a polynomial of degree ≤ ρ