Wiman–Valiron theory

DefinitionPower-growth exceptional set#✓fully proved

For a function \(h : \mathbb{R} \to \mathbb{R}\) and real numbers \(p\) and \(x_0\), this is the set of real numbers \(x \ge x_0\) such that \(h(x)^p \le h'(x)\), where \(h(x)^p\) is the real power and \(h'(x)\) is the derivative of \(h\) at \(x\), taken to be \(0\) where \(h\) is not differentiable.

def powerGrowthBadSet (h : ℝ → ℝ) (p x₀ : ℝ) : Set ℝ :=
  {x | x₀ ≤ x ∧ h x ^ p ≤ deriv h x}
Used by 3
Used byThe Wiman exceptional set has finite measure · The power-growth exceptional set has finite measure · Wiman exceptional set

TheoremThe power-growth exceptional set has finite measure#✓fully proved

Let \(p > 1\) and \(x_0\) be real numbers, and let \(h : \mathbb{R} \to \mathbb{R}\) be continuously differentiable, with \(h(x) > 0\) for all \(x \ge x_0\) and \(h\) nondecreasing on \([x_0, \infty)\). Then the power-growth exceptional set of \(h\), the set of \(x \ge x_0\) with \(h(x)^p \le h'(x)\), has finite Lebesgue measure.

theorem volume_powerGrowthBadSet_lt_top
    (h : ℝ → ℝ) {p x₀ : ℝ} (hp : 1 < p)
    (hpos : ∀ x, x₀ ≤ x → 0 < h x)
    (hmono : MonotoneOn h (Ici x₀))
    (hsmooth : ContDiff ℝ 1 h) :
    volume (powerGrowthBadSet h p x₀) < ∞
Uses 1 · Used by 1
Statement usesPower-growth exceptional set
Used byThe Wiman exceptional set has finite measure

DefinitionWiman Taylor coefficient#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\) and \(n \in \mathbb{N}\), the \(n\)th Taylor coefficient of \(f\) at the origin is \(a_n = f^{(n)}(0) / n!\), where \(f^{(n)}\) is the \(n\)th iterated complex derivative of \(f\).

Here the derivative at a point where a function is not complex differentiable is taken to be \(0\). For an entire function these are the coefficients of its Taylor series at \(0\).

def wimanTaylorCoefficient (f : ℂ → ℂ) (n : ℕ) : ℂ :=
  iteratedDeriv n f 0 / (n.factorial : ℂ)
Used by 23
Used byDerivative of the logarithmic majorant as a mean · Eventual regularity of the logarithmic majorant · Taylor expansion of an entire function · Transcendental entire functions have infinitely many Taylor coefficients · Exponential moments of the Wiman coefficient measure are finite · Exponential moments of the Wiman coefficient measure equal the Wiman majorant · The Wiman tilted measure is a probability measure · Second derivative of the logarithmic majorant as a variance · The logarithmic majorant has nonnegative second derivative · Summability of the radial Taylor terms · The maximum term of a transcendental entire function tends to infinity · Wiman coefficient measure · A nonzero Taylor coefficient makes the Wiman coefficient measure nonzero · Point masses of the Wiman coefficient measure · Corrected Rosenbloom estimate · The maximum modulus is at most the radial Taylor majorant · Cauchy's inequality for the maximum term · Wiman term · Wiman term at the absolute value of the radius · Wiman term at a negated radius · Radial Taylor terms are nonnegative · Atoms of the tilted coefficient measure · Hayman's successive coefficient problem for starlike functions

DefinitionWiman term#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\), a real number \(r\) and a natural number \(n\), the Wiman term of \(f\) at radius \(r\) and index \(n\) is the real number \(|a_n| \, |r|^n\), where \(a_n = f^{(n)}(0) / n!\) is the \(n\)th Taylor coefficient of \(f\) at the origin. It is the modulus of the \(n\)th Taylor term of \(f\) on the circle of radius \(|r|\).

Using \(|r|\) makes a negative input denote the same radius as its absolute value, so the Wiman term is always nonnegative.

def wimanTerm (f : ℂ → ℂ) (r : ℝ) (n : ℕ) : ℝ :=
  ‖wimanTaylorCoefficient f n‖ * |r| ^ n
Uses 1 · Used by 24
Statement usesWiman Taylor coefficient
Used byThe Taylor terms are bounded above · Eventual regularity of the logarithmic majorant · The maximum term is attained by a Taylor term · Exponential moments of the Wiman coefficient measure are finite · Exponential moments of the Wiman coefficient measure equal the Wiman majorant · Summability of the radial Taylor terms · The maximum term of a transcendental entire function tends to infinity · Radial majorant · Majorant bound off an exceptional set · Corrected Rosenbloom estimate · The radial majorant is nonnegative · The maximum modulus is at most the radial Taylor majorant · Wiman maximum term · Wiman maximum term at the absolute value of the radius · Bounding the maximum term · Cauchy's inequality for the maximum term · The Wiman maximum term is even in the radius · Wiman term at the absolute value of the radius · Each radial Taylor term is at most the radial majorant · Each Taylor term is at most the maximum term · Wiman term at a negated radius · Radial Taylor terms are nonnegative · Atomic form of the tilted coefficient measure · Atoms of the tilted coefficient measure

DefinitionWiman maximum term#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\) and a real number \(r\), the Wiman maximum term \(\mu(f, r)\) is the supremum over \(n \in \mathbb{N}\) of the Wiman terms \(|a_n| \, |r|^n\), where \(a_n = f^{(n)}(0) / n!\) is the \(n\)th Wiman Taylor coefficient of \(f\).

Here the supremum of a set of real numbers that is not bounded above is taken to be \(0\).

def wimanMaximumTerm (f : ℂ → ℂ) (r : ℝ) : ℝ :=
  sSup (range (wimanTerm f r))
Uses 1 · Used by 14
Statement usesWiman term
Used byThe maximum term eventually exceeds one · The logarithm of the maximum term is eventually positive · Eventual regularity of the logarithmic majorant · Wiman's inequality with exponent \(2/3\) at arbitrarily large radii · The maximum term is attained by a Taylor term · The maximum term of a transcendental entire function tends to infinity · The maximum term tends to infinity along logarithmic radii · Majorant bound off an exceptional set · Corrected Rosenbloom estimate · Wiman maximum term at the absolute value of the radius · Bounding the maximum term · Cauchy's inequality for the maximum term · The Wiman maximum term is even in the radius · Each Taylor term is at most the maximum term

DefinitionWiman maximum modulus#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\) and a real number \(r\), the Wiman maximum modulus \(M(f, r)\) is the supremum of \(|f(z)|\) over all \(z \in \mathbb{C}\) with \(|z| = |r|\).

Here the supremum of a set of real numbers that is not bounded above is taken to be \(0\).

def wimanMaximumModulus (f : ℂ → ℂ) (r : ℝ) : ℝ :=
  sSup ((fun z : ℂ => ‖f z‖) '' Metric.sphere 0 |r|)
Used by 8
Used byRatio of \(\log |f|\) to the logarithm of the maximum modulus · The maximum modulus is attained · Wiman's inequality with exponent \(2/3\) at arbitrarily large radii · Values on a circle are bounded by the maximum modulus · Wiman maximum modulus at the absolute value of the radius · The maximum modulus is at most the radial Taylor majorant · The Wiman maximum modulus is even in the radius · Cauchy's inequality for the maximum term

TheoremWiman term at the absolute value of the radius#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\), every real number \(r\) and every natural number \(n\), the Wiman term of \(f\) at radius \(|r|\) and index \(n\) equals the Wiman term of \(f\) at radius \(r\) and index \(n\).

@[simp]
theorem wimanTerm_abs (f : ℂ → ℂ) (r : ℝ) (n : ℕ) :
    wimanTerm f |r| n = wimanTerm f r n
Uses 2 · Used by 1
Statement usesWiman term
Proof usesWiman Taylor coefficient
Used byWiman maximum term at the absolute value of the radius

TheoremWiman maximum term at the absolute value of the radius#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\) and every real number \(r\), the Wiman maximum term of \(f\) at radius \(|r|\) equals the Wiman maximum term of \(f\) at radius \(r\).

@[simp]
theorem wimanMaximumTerm_abs (f : ℂ → ℂ) (r : ℝ) :
    wimanMaximumTerm f |r| = wimanMaximumTerm f r
Uses 3
Statement usesWiman maximum term
Proof usesWiman term · Wiman term at the absolute value of the radius

TheoremWiman maximum modulus at the absolute value of the radius#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\) and every real number \(r\), the Wiman maximum modulus of \(f\) at radius \(|r|\) equals the Wiman maximum modulus of \(f\) at radius \(r\).

@[simp]
theorem wimanMaximumModulus_abs (f : ℂ → ℂ) (r : ℝ) :
    wimanMaximumModulus f |r| = wimanMaximumModulus f r
Uses 1
Statement usesWiman maximum modulus

TheoremWiman term at a negated radius#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\), every real number \(r\) and every natural number \(n\), the Wiman term of \(f\) at radius \(-r\) and index \(n\) equals the Wiman term of \(f\) at radius \(r\) and index \(n\).

@[simp]
theorem wimanTerm_neg (f : ℂ → ℂ) (r : ℝ) (n : ℕ) :
    wimanTerm f (-r) n = wimanTerm f r n
Uses 2 · Used by 1
Statement usesWiman term
Proof usesWiman Taylor coefficient
Used byThe Wiman maximum term is even in the radius

TheoremThe Wiman maximum term is even in the radius#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\) and every real number \(r\), the Wiman maximum term of \(f\) at radius \(-r\) equals the Wiman maximum term of \(f\) at radius \(r\).

@[simp]
theorem wimanMaximumTerm_neg (f : ℂ → ℂ) (r : ℝ) :
    wimanMaximumTerm f (-r) = wimanMaximumTerm f r
Uses 3
Statement usesWiman maximum term
Proof usesWiman term · Wiman term at a negated radius

TheoremThe Wiman maximum modulus is even in the radius#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\) and every real number \(r\), the Wiman maximum modulus of \(f\) at radius \(-r\) equals the Wiman maximum modulus of \(f\) at radius \(r\).

@[simp]
theorem wimanMaximumModulus_neg (f : ℂ → ℂ) (r : ℝ) :
    wimanMaximumModulus f (-r) = wimanMaximumModulus f r
Uses 1
Statement usesWiman maximum modulus

DefinitionTranscendental functions#✓fully proved

A function \(f : \mathbb{C} \to \mathbb{C}\) is transcendental when there is no complex polynomial \(p\) with \(f(z) = p(z)\) for all \(z \in \mathbb{C}\).

No analyticity is assumed; results about transcendental entire functions assume it separately.

def IsTranscendental (f : ℂ → ℂ) : Prop :=
  ¬ ∃ p : Polynomial ℂ, ∀ z : ℂ, f z = p.eval z
Used by 10
Used byLower bound \(-1\) for the log-modulus ratio along continua · The maximum term eventually exceeds one · The logarithm of the maximum term is eventually positive · Eventual regularity of the logarithmic majorant · The Wiman exceptional set has finite measure · Wiman's inequality with exponent \(2/3\) at arbitrarily large radii · Transcendental entire functions have infinitely many Taylor coefficients · The maximum term of a transcendental entire function tends to infinity · The maximum term tends to infinity along logarithmic radii · Majorant bound off an exceptional set

TheoremValues on a circle are bounded by the maximum modulus#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) be continuous, let \(r\) be a real number and let \(z \in \mathbb{C}\) with \(|z| = r\). Then \(|f(z)| \le M(f, r)\), where \(M(f, r)\) is the Wiman maximum modulus of \(f\) at radius \(r\).

theorem norm_le_wimanMaximumModulus {f : ℂ → ℂ} {r : ℝ} {z : ℂ}
    (hf : Continuous f) (hz : ‖z‖ = r) :
    ‖f z‖ ≤ wimanMaximumModulus f r
Uses 1
Statement usesWiman maximum modulus

TheoremCubing a Wiman 2/3 bound#✓fully proved

Let \(M\) and \(\mu\) be real numbers with \(M \ge 0\), \(\mu \ge 0\) and \(\log \mu \ge 0\), where \(\log\) is the real logarithm with \(\log 0 = 0\). If \(M \le \mu (\log \mu)^{2/3}\), then \(M^3 \le \mu^3 (\log \mu)^2\).

theorem cube_le_cube_mul_log_sq_of_wiman {M μ : ℝ}
    (hM : 0 ≤ M) (_hμ : 0 ≤ μ) (hlog : 0 ≤ Real.log μ)
    (hWiman : M ≤ μ * Real.log μ ^ (2 / 3 : ℝ)) :
    M ^ 3 ≤ μ ^ 3 * Real.log μ ^ 2

TheoremAbsorbing constants into the exponent gap#✓fully proved

For every real \(C > 0\) there is a real \(U > 1\) such that for all reals \(\mu\) and \(A\) with \(U \le \mu \le A\) and \(A \le C \mu \bigl(1 + (\log A)^{81/128}\bigr)\), we have \(A \le \mu (\log \mu)^{2/3}\).

The gap \(2/3 - 81/128 > 0\) between the exponents absorbs the constant \(C\) of the corrected Rosenbloom estimate once the maximum term \(\mu\) is large.

theorem eventually_absorb_corrected_wiman_exponent
    (C : ℝ) (hC : 0 < C) :
    ∃ U : ℝ, 1 < U ∧ ∀ μ A : ℝ,
      U ≤ μ → μ ≤ A →
      A ≤ C * μ * (1 + Real.log A ^ (81 / 128 : ℝ)) →
      A ≤ μ * Real.log μ ^ (2 / 3 : ℝ)
Used by 1
Used byWiman's inequality with exponent \(2/3\) at arbitrarily large radii

TheoremThe maximum modulus is attained#✓fully proved

Let \(f\) be an entire function and let \(r \ge 0\). Then there is a point \(z\) with \(|z| = r\) such that \(|f(w)| \le |f(z)|\) for every \(w\) with \(|w| = r\), and the maximum modulus \(M(r) = \sup_{|w| = r} |f(w)|\) equals \(|f(z)|\).

theorem exists_mem_sphere_eq_wimanMaximumModulus
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    {r : ℝ} (hr : 0 ≤ r) :
    ∃ z ∈ Metric.sphere (0 : ℂ) r,
      wimanMaximumModulus f r = ‖f z‖ ∧
      ∀ w ∈ Metric.sphere (0 : ℂ) r, ‖f w‖ ≤ ‖f z‖
Uses 1 · Used by 2
Statement usesWiman maximum modulus
Used byThe maximum modulus is at most the radial Taylor majorant · Cauchy's inequality for the maximum term

DefinitionRadial majorant#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\) with Taylor coefficients \(a_n = f^{(n)}(0) / n!\) at the origin and a real number \(r\), the radial majorant of \(f\) at \(r\) is \(M_f(r) = \sum_{n \ge 0} |a_n| \, |r|^n\), the sum of the radial Taylor terms at radius \(|r|\). By convention \(M_f(r) = 0\) when this series diverges.

def wimanMajorant (f : ℂ → ℂ) (r : ℝ) : ℝ :=
  ∑' n, wimanTerm f r n
Uses 1 · Used by 14
Statement usesWiman term
Used byThe Taylor terms are bounded above · Eventual regularity of the logarithmic majorant · Wiman's inequality with exponent \(2/3\) at arbitrarily large radii · Exponential moments of the Wiman coefficient measure equal the Wiman majorant · The Wiman growth is the cumulant generating function of the coefficient measure · Wiman growth function · Majorant bound off an exceptional set · Corrected Rosenbloom estimate · The radial majorant is nonnegative · The maximum modulus is at most the radial Taylor majorant · Moment generating function of the coefficient measure · Each radial Taylor term is at most the radial majorant · Atomic form of the tilted coefficient measure · Atoms of the tilted coefficient measure

TheoremRadial Taylor terms are nonnegative#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\) with Taylor coefficients \(a_n = f^{(n)}(0) / n!\) at the origin, every real \(r\) and every \(n \in \mathbb{N}\), we have \(0 \le |a_n| \, |r|^n\).

theorem wimanTerm_nonneg (f : ℂ → ℂ) (r : ℝ) (n : ℕ) :
    0 ≤ wimanTerm f r n
Uses 2 · Used by 5
Statement usesWiman term
Proof usesWiman Taylor coefficient
Used byThe maximum term is attained by a Taylor term · Majorant bound off an exceptional set · Corrected Rosenbloom estimate · The radial majorant is nonnegative · Each radial Taylor term is at most the radial majorant

TheoremSummability of the radial Taylor terms#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0) / n!\) at the origin. For every real \(r\), the series \(\sum_{n \ge 0} |a_n| \, |r|^n\) converges.

theorem summable_wimanTerm
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (r : ℝ) :
    Summable (wimanTerm f r)
Uses 2 · Used by 3
Statement usesWiman term
Proof usesWiman Taylor coefficient
Used byThe maximum term is attained by a Taylor term · Exponential moments of the Wiman coefficient measure are finite · Each radial Taylor term is at most the radial majorant

TheoremThe radial majorant is nonnegative#✓fully proved

For every function \(f : \mathbb{C} \to \mathbb{C}\) with Taylor coefficients \(a_n = f^{(n)}(0) / n!\) at the origin and every real number \(r\), the radial majorant \(M_f(r) = \sum_{n \ge 0} |a_n| \, |r|^n\) (taken to be \(0\) when the series diverges) satisfies \(0 \le M_f(r)\).

theorem wimanMajorant_nonneg (f : ℂ → ℂ) (r : ℝ) :
    0 ≤ wimanMajorant f r
Uses 3 · Used by 1
Statement usesRadial majorant
Proof usesWiman term · Radial Taylor terms are nonnegative
Used byAtoms of the tilted coefficient measure

TheoremEach radial Taylor term is at most the radial majorant#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0) / n!\) at the origin, and let \(M_f(r) = \sum_{k \ge 0} |a_k| \, |r|^k\) be its radial majorant. For every real \(r\) and every \(n \in \mathbb{N}\), \(|a_n| \, |r|^n \le M_f(r)\).

theorem wimanTerm_le_wimanMajorant
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (r : ℝ) (n : ℕ) :
    wimanTerm f r n ≤ wimanMajorant f r
Uses 4 · Used by 3
Statement usesRadial majorant · Wiman term
Proof usesSummability of the radial Taylor terms · Radial Taylor terms are nonnegative
Used byThe Taylor terms are bounded above · Eventual regularity of the logarithmic majorant · Corrected Rosenbloom estimate

DefinitionWiman growth function#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) have Taylor coefficients \(a_n = f^{(n)}(0) / n!\) at the origin, and let \(M_f(r) = \sum_{n \ge 0} |a_n| \, |r|^n\) be its radial majorant, taken to be \(0\) when the series diverges. For a real number \(x\), the Wiman growth of \(f\) at \(x\) is \(\log M_f(e^x)\), the logarithm of the radial majorant at radius \(e^x\), with the convention \(\log 0 = 0\).

def wimanGrowth (f : ℂ → ℂ) (x : ℝ) : ℝ :=
  Real.log (wimanMajorant f (Real.exp x))
Uses 1 · Used by 11
Statement usesRadial majorant
Used byThe logarithmic majorant is \(C^2\) · Derivative of the logarithmic majorant as a mean · Eventual regularity of the logarithmic majorant · The Wiman exceptional set has finite measure · Wiman's inequality with exponent \(2/3\) at arbitrarily large radii · Second derivative of the logarithmic majorant as a variance · The logarithmic majorant has nonnegative second derivative · The Wiman growth is the cumulant generating function of the coefficient measure · Wiman exceptional set · Majorant bound off an exceptional set · Corrected Rosenbloom estimate

DefinitionWiman coefficient measure#✓fully proved

For \(f : \mathbb{C} \to \mathbb{C}\) with Taylor coefficients \(a_n = f^{(n)}(0)/n!\) at \(0\), the Wiman coefficient measure of \(f\) is the measure \(\mu_f = \sum_{n \ge 0} |a_n|\,\delta_n\) on \(\mathbb{N}\), which gives each \(n\) mass \(|a_n|\).

def wimanCoefficientMeasure (f : ℂ → ℂ) : Measure ℕ :=
  Measure.sum fun n : ℕ =>
    ENNReal.ofReal ‖wimanTaylorCoefficient f n‖ • Measure.dirac n
Uses 1 · Used by 15
Statement usesWiman Taylor coefficient
Used byThe logarithmic majorant is \(C^2\) · Derivative of the logarithmic majorant as a mean · Exponential moments of the Wiman coefficient measure are finite · The exponential-integrability set of the Wiman coefficient measure is the whole line · Exponential moments of the Wiman coefficient measure equal the Wiman majorant · The Wiman tilted measure is a probability measure · Second derivative of the logarithmic majorant as a variance · Every real parameter is interior to the exponential-integrability set · The Wiman growth is the cumulant generating function of the coefficient measure · A nonzero Taylor coefficient makes the Wiman coefficient measure nonzero · Point masses of the Wiman coefficient measure · Corrected Rosenbloom estimate · Moment generating function of the coefficient measure · Tilted coefficient measure · Atoms of the tilted coefficient measure

DefinitionTilted coefficient measure#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) have Taylor coefficients \(a_n = f^{(n)}(0)/n!\), and let \(\mu_f\) be its coefficient measure on \(\mathbb{N}\), with mass \(|a_n|\) at \(n\). For a real number \(x\), the tilted coefficient measure \(\mu_{f,x}\) is the exponential tilt of \(\mu_f\) by \(n \mapsto xn\): the measure with density \(e^{xn} / \int e^{xm}\,d\mu_f(m)\) with respect to \(\mu_f\).

def wimanTiltedMeasure (f : ℂ → ℂ) (x : ℝ) : Measure ℕ :=
  (wimanCoefficientMeasure f).tilted fun n : ℕ => x * (n : ℝ)
Uses 1 · Used by 8
Statement usesWiman coefficient measure
Used byDerivative of the logarithmic majorant as a mean · Eventual regularity of the logarithmic majorant · The Wiman tilted measure is a probability measure · Second derivative of the logarithmic majorant as a variance · The logarithmic majorant has nonnegative second derivative · Corrected Rosenbloom estimate · Atomic form of the tilted coefficient measure · Atoms of the tilted coefficient measure

TheoremPoint masses of the Wiman coefficient measure#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) and \(a_n = f^{(n)}(0)/n!\). For every \(n \in \mathbb{N}\), the Wiman coefficient measure \(\mu_f\) of \(f\) gives the singleton \(\{n\}\) mass \(\mu_f(\{n\}) = |a_n|\).

@[simp]
theorem wimanCoefficientMeasure_singleton (f : ℂ → ℂ) (n : ℕ) :
    wimanCoefficientMeasure f {n} = ENNReal.ofReal ‖wimanTaylorCoefficient f n‖
Uses 2 · Used by 2
Statement usesWiman coefficient measure · Wiman Taylor coefficient
Used byA nonzero Taylor coefficient makes the Wiman coefficient measure nonzero · Atoms of the tilted coefficient measure

TheoremExponential moments of the Wiman coefficient measure are finite#✓fully proved

Let \(f\) be an entire function and let \(\mu_f\) be its Wiman coefficient measure on \(\mathbb{N}\), which gives each \(n \in \mathbb{N}\) mass \(|a_n|\), where \(a_n = f^{(n)}(0)/n!\). For every real \(x\), the function \(n \mapsto e^{xn}\) is integrable with respect to \(\mu_f\).

theorem integrable_exp_mul_wimanCoefficientMeasure
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) :
    Integrable (fun n : ℕ => Real.exp (x * (n : ℝ))) (wimanCoefficientMeasure f)
Uses 4 · Used by 3
Statement usesWiman coefficient measure
Proof usesSummability of the radial Taylor terms · Wiman Taylor coefficient · Wiman term
Used byThe exponential-integrability set of the Wiman coefficient measure is the whole line · Exponential moments of the Wiman coefficient measure equal the Wiman majorant · The Wiman tilted measure is a probability measure

TheoremThe exponential-integrability set of the Wiman coefficient measure is the whole line#✓fully proved

Let \(f\) be an entire function and let \(\mu_f\) be its Wiman coefficient measure on \(\mathbb{N}\). The set of real \(t\) for which \(n \mapsto e^{tn}\) is integrable with respect to \(\mu_f\) is all of \(\mathbb{R}\).

theorem integrableExpSet_wimanCoefficientMeasure_eq_univ
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) :
    integrableExpSet (fun n : ℕ => (n : ℝ)) (wimanCoefficientMeasure f) = Set.univ
Uses 2 · Used by 2
Statement usesWiman coefficient measure
Proof usesExponential moments of the Wiman coefficient measure are finite
Used byThe logarithmic majorant is \(C^2\) · Every real parameter is interior to the exponential-integrability set

TheoremEvery real parameter is interior to the exponential-integrability set#✓fully proved

Let \(f\) be an entire function and let \(\mu_f\) be its Wiman coefficient measure on \(\mathbb{N}\). Every real \(x\) lies in the interior of the set of real \(t\) for which \(n \mapsto e^{tn}\) is integrable with respect to \(\mu_f\).

theorem mem_interior_integrableExpSet_wimanCoefficientMeasure
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) :
    x ∈ interior (integrableExpSet (fun n : ℕ => (n : ℝ))
      (wimanCoefficientMeasure f))
Uses 2 · Used by 3
Statement usesWiman coefficient measure
Proof usesThe exponential-integrability set of the Wiman coefficient measure is the whole line
Used byDerivative of the logarithmic majorant as a mean · Second derivative of the logarithmic majorant as a variance · Corrected Rosenbloom estimate

TheoremExponential moments of the Wiman coefficient measure equal the Wiman majorant#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0)/n!\) at \(0\), and let \(\mu_f\) be its Wiman coefficient measure on \(\mathbb{N}\). For every real \(x\),

\[\int e^{xn}\,d\mu_f(n) = M_f(e^x),\]

where \(M_f(r) = \sum_{n \ge 0} |a_n|\,|r|^n\) is the Wiman majorant of \(f\).

theorem integral_exp_mul_wimanCoefficientMeasure
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) :
    ∫ n : ℕ, Real.exp (x * (n : ℝ)) ∂(wimanCoefficientMeasure f) =
      wimanMajorant f (Real.exp x)
Uses 5 · Used by 1
Statement usesWiman coefficient measure · Radial majorant
Proof usesExponential moments of the Wiman coefficient measure are finite · Wiman Taylor coefficient · Wiman term
Used byMoment generating function of the coefficient measure

TheoremMoment generating function of the coefficient measure#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0)/n!\), and let \(\mu_f\) be its coefficient measure on \(\mathbb{N}\), which has mass \(|a_n|\) at \(n\). For every real \(x\), the moment generating function of \(n \mapsto n\) under \(\mu_f\) at \(x\), namely \(\int e^{xn}\,d\mu_f(n)\), equals the radial majorant \(M_f(e^x)\), where \(M_f(r) = \sum_n |a_n|\,|r|^n\).

theorem wiman_mgf_eq_majorant
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) :
    mgf (fun n : ℕ => (n : ℝ)) (wimanCoefficientMeasure f) x =
      wimanMajorant f (Real.exp x)
Uses 3 · Used by 2
Statement usesWiman coefficient measure · Radial majorant
Proof usesExponential moments of the Wiman coefficient measure equal the Wiman majorant
Used byThe Wiman growth is the cumulant generating function of the coefficient measure · Atoms of the tilted coefficient measure

TheoremThe Wiman growth is the cumulant generating function of the coefficient measure#✓fully proved

Let \(f\) be an entire function and let \(\mu_f\) be its Wiman coefficient measure on \(\mathbb{N}\). For every real \(x\), the cumulant generating function of \(n \mapsto n\) under \(\mu_f\) at \(x\), namely \(\log \int e^{xn}\,d\mu_f(n)\), equals the Wiman growth \(G_f(x) = \log M_f(e^x)\), where \(M_f\) is the Wiman majorant of \(f\).

theorem wiman_cgf_eq_growth
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) :
    ProbabilityTheory.cgf (fun n : ℕ => (n : ℝ))
        (wimanCoefficientMeasure f) x = wimanGrowth f x
Uses 4 · Used by 3
Statement usesWiman coefficient measure · Wiman growth function
Proof usesRadial majorant · Moment generating function of the coefficient measure
Used byThe logarithmic majorant is \(C^2\) · Derivative of the logarithmic majorant as a mean · Second derivative of the logarithmic majorant as a variance

TheoremA nonzero Taylor coefficient makes the Wiman coefficient measure nonzero#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) and \(a_n = f^{(n)}(0)/n!\). If \(a_n \ne 0\) for some \(n\), then the Wiman coefficient measure \(\mu_f\) of \(f\) is not the zero measure.

theorem wimanCoefficientMeasure_ne_zero
    (f : ℂ → ℂ) (hne : ∃ n, wimanTaylorCoefficient f n ≠ 0) :
    wimanCoefficientMeasure f ≠ 0
Uses 3 · Used by 1
Statement usesWiman coefficient measure · Wiman Taylor coefficient
Proof usesPoint masses of the Wiman coefficient measure
Used byThe Wiman tilted measure is a probability measure

TheoremThe Wiman tilted measure is a probability measure#✓fully proved

Let \(f\) be an entire function such that \(f^{(n)}(0)/n! \ne 0\) for some \(n\), and let \(\mu_f\) be its Wiman coefficient measure on \(\mathbb{N}\). For every real \(x\), the Wiman tilted measure of \(f\) at \(x\), which has density \(n \mapsto e^{xn} / \int e^{xm}\,d\mu_f(m)\) with respect to \(\mu_f\), is a probability measure.

theorem isProbabilityMeasure_wimanTiltedMeasure
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (hne : ∃ n, wimanTaylorCoefficient f n ≠ 0) (x : ℝ) :
    IsProbabilityMeasure (wimanTiltedMeasure f x)
Uses 5 · Used by 1
Statement usesWiman Taylor coefficient · Tilted coefficient measure
Proof usesExponential moments of the Wiman coefficient measure are finite · Wiman coefficient measure · A nonzero Taylor coefficient makes the Wiman coefficient measure nonzero
Used byCorrected Rosenbloom estimate

TheoremAtoms of the tilted coefficient measure#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0)/n!\), radial majorant \(M_f(r) = \sum_n |a_n|\,|r|^n\) and Taylor terms \(T_n(r) = |a_n|\,|r|^n\). For every real \(x\) and every \(n \in \mathbb{N}\), the tilted coefficient measure \(\mu_{f,x}\) gives the singleton \(\{n\}\) mass \(T_n(e^x) / M_f(e^x)\) (with the convention \(t/0 = 0\)).

@[simp]
theorem wimanTiltedMeasure_singleton
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) (n : ℕ) :
    wimanTiltedMeasure f x {n} =
      ENNReal.ofReal
        (wimanTerm f (Real.exp x) n / wimanMajorant f (Real.exp x))
Uses 8 · Used by 2
Statement usesRadial majorant · Wiman term · Tilted coefficient measure
Proof usesWiman coefficient measure · Point masses of the Wiman coefficient measure · The radial majorant is nonnegative · Wiman Taylor coefficient · Moment generating function of the coefficient measure
Used byCorrected Rosenbloom estimate · Atomic form of the tilted coefficient measure

TheoremAtomic form of the tilted coefficient measure#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0)/n!\), radial majorant \(M_f(r) = \sum_n |a_n|\,|r|^n\) and Taylor terms \(T_n(r) = |a_n|\,|r|^n\). For every real \(x\), the tilted coefficient measure \(\mu_{f,x}\) equals \(\sum_{n \in \mathbb{N}} \frac{T_n(e^x)}{M_f(e^x)}\,\delta_n\), the measure on \(\mathbb{N}\) with mass \(T_n(e^x) / M_f(e^x)\) at each \(n\) (with the convention \(t/0 = 0\)).

theorem wimanTiltedMeasure_eq_sum
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) :
    wimanTiltedMeasure f x =
      Measure.sum fun n : ℕ =>
        ENNReal.ofReal
          (wimanTerm f (Real.exp x) n / wimanMajorant f (Real.exp x)) •
            Measure.dirac n
Uses 4
Statement usesRadial majorant · Wiman term · Tilted coefficient measure
Proof usesAtoms of the tilted coefficient measure

TheoremThe logarithmic majorant is \(C^2\)#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n\) at the origin, and let \(\Phi(x) = \log \sum_{n \ge 0} |a_n| e^{nx}\) be the logarithm of its radial Taylor majorant at radius \(e^x\) (with \(\log 0 = 0\)). Then \(\Phi\) is twice continuously differentiable on \(\mathbb{R}\).

theorem contDiff_two_wimanGrowth
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) :
    ContDiff ℝ 2 (wimanGrowth f)
Uses 4 · Used by 1
Statement usesWiman growth function
Proof usesThe exponential-integrability set of the Wiman coefficient measure is the whole line · Wiman coefficient measure · The Wiman growth is the cumulant generating function of the coefficient measure
Used byEventual regularity of the logarithmic majorant

TheoremDerivative of the logarithmic majorant as a mean#✓fully proved

Let \(f\) be an entire function whose Taylor coefficients \(a_n\) at the origin are not all zero, and let \(\Phi(x) = \log \sum_{n \ge 0} |a_n| e^{nx}\). For real \(x\), let \(\nu_x\) be the coefficient measure tilted at \(x\), the probability measure on \(\mathbb{N}\) with \(\nu_x(\{n\}) = |a_n| e^{nx} / \sum_{m \ge 0} |a_m| e^{mx}\). Then \(\Phi'(x) = \int n \, d\nu_x(n)\), the mean of \(n\) under \(\nu_x\).

theorem deriv_wimanGrowth_eq_expectation
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (_hne : ∃ n, wimanTaylorCoefficient f n ≠ 0) (x : ℝ) :
    deriv (wimanGrowth f) x =
      ∫ n : ℕ, (n : ℝ) ∂(wimanTiltedMeasure f x)
Uses 6 · Used by 1
Statement usesWiman growth function · Wiman Taylor coefficient · Tilted coefficient measure
Proof usesEvery real parameter is interior to the exponential-integrability set · Wiman coefficient measure · The Wiman growth is the cumulant generating function of the coefficient measure
Used byEventual regularity of the logarithmic majorant

TheoremSecond derivative of the logarithmic majorant as a variance#✓fully proved

Let \(f\) be an entire function whose Taylor coefficients \(a_n\) at the origin are not all zero, and let \(\Phi(x) = \log \sum_{n \ge 0} |a_n| e^{nx}\). For real \(x\), let \(\nu_x\) be the coefficient measure tilted at \(x\), the probability measure on \(\mathbb{N}\) with \(\nu_x(\{n\}) = |a_n| e^{nx} / \sum_{m \ge 0} |a_m| e^{mx}\). Then \(\Phi''(x)\) is the variance of \(n\) under \(\nu_x\).

theorem iteratedDeriv_two_wimanGrowth_eq_variance
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (_hne : ∃ n, wimanTaylorCoefficient f n ≠ 0) (x : ℝ) :
    iteratedDeriv 2 (wimanGrowth f) x =
      ProbabilityTheory.variance
        (fun n : ℕ => (n : ℝ)) (wimanTiltedMeasure f x)
Uses 6 · Used by 2
Statement usesWiman growth function · Wiman Taylor coefficient · Tilted coefficient measure
Proof usesEvery real parameter is interior to the exponential-integrability set · Wiman coefficient measure · The Wiman growth is the cumulant generating function of the coefficient measure
Used byThe logarithmic majorant has nonnegative second derivative · Corrected Rosenbloom estimate

TheoremThe logarithmic majorant has nonnegative second derivative#✓fully proved

Let \(f\) be an entire function whose Taylor coefficients \(a_n\) at the origin are not all zero, and let \(\Phi(x) = \log \sum_{n \ge 0} |a_n| e^{nx}\). Then \(\Phi''(x) \ge 0\) for every real \(x\).

theorem iteratedDeriv_two_wimanGrowth_nonneg
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (hne : ∃ n, wimanTaylorCoefficient f n ≠ 0) (x : ℝ) :
    0 ≤ iteratedDeriv 2 (wimanGrowth f) x
Uses 4 · Used by 1
Statement usesWiman growth function · Wiman Taylor coefficient
Proof usesSecond derivative of the logarithmic majorant as a variance · Tilted coefficient measure
Used byEventual regularity of the logarithmic majorant

TheoremThe Taylor terms are bounded above#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n\) at the origin, and let \(r\) be real. Then the set of Taylor terms \(\{|a_n|\,|r|^n : n \in \mathbb{N}\}\) is bounded above.

theorem bddAbove_range_wimanTerm
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (r : ℝ) :
    BddAbove (range (wimanTerm f r))
Uses 3 · Used by 1
Statement usesWiman term
Proof usesRadial majorant · Each radial Taylor term is at most the radial majorant
Used byEach Taylor term is at most the maximum term

TheoremEach Taylor term is at most the maximum term#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n\) at the origin and maximum term \(\mu(r) = \sup_k |a_k|\,|r|^k\). For every real \(r\) and every \(n \in \mathbb{N}\), \(|a_n|\,|r|^n \le \mu(r)\).

theorem wimanTerm_le_wimanMaximumTerm
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (r : ℝ) (n : ℕ) :
    wimanTerm f r n ≤ wimanMaximumTerm f r
Uses 3 · Used by 5
Statement usesWiman maximum term · Wiman term
Proof usesThe Taylor terms are bounded above
Used byThe maximum term is attained by a Taylor term · The maximum term of a transcendental entire function tends to infinity · Majorant bound off an exceptional set · Corrected Rosenbloom estimate · Bounding the maximum term

TheoremBounding the maximum term#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n\) at the origin and maximum term \(\mu(r) = \sup_n |a_n|\,|r|^n\). For all real \(r\) and \(c\), \(\mu(r) \le c\) if and only if \(|a_n|\,|r|^n \le c\) for every \(n \in \mathbb{N}\).

theorem wimanMaximumTerm_le_iff
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (r a : ℝ) :
    wimanMaximumTerm f r ≤ a ↔ ∀ n : ℕ, wimanTerm f r n ≤ a
Uses 3 · Used by 3
Statement usesWiman maximum term · Wiman term
Proof usesEach Taylor term is at most the maximum term
Used byEventual regularity of the logarithmic majorant · The maximum term is attained by a Taylor term · Cauchy's inequality for the maximum term

TheoremThe maximum term is attained by a Taylor term#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n\) at the origin and maximum term \(\mu(r) = \sup_n |a_n|\,|r|^n\). For every real \(r\) there is an \(n \in \mathbb{N}\) with \(|a_n|\,|r|^n = \mu(r)\).

theorem exists_wimanTerm_eq_wimanMaximumTerm
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (r : ℝ) :
    ∃ n : ℕ, wimanTerm f r n = wimanMaximumTerm f r
Uses 6
Statement usesWiman maximum term · Wiman term
Proof usesSummability of the radial Taylor terms · Bounding the maximum term · Each Taylor term is at most the maximum term · Radial Taylor terms are nonnegative

TheoremCorrected Rosenbloom estimate#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0)/n!\), radial majorant \(M_f(r) = \sum_n |a_n|\,|r|^n\), maximum term \(\mu_f(r) = \sup_n |a_n|\,|r|^n\) and logarithmic majorant \(g_f(x) = \log M_f(e^x)\). For every real \(x\), \(M_f(e^x) \le 8\,\mu_f(e^x)\,\bigl(1 + \sqrt{g_f''(x)}\bigr)\).

The additive \(1\) keeps the estimate valid when \(g_f''(x) = 0\).

theorem wimanMajorant_le_eight_mul_maximumTerm
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (x : ℝ) :
    wimanMajorant f (Real.exp x) ≤
      8 * wimanMaximumTerm f (Real.exp x) *
        (1 + Real.sqrt (iteratedDeriv 2 (wimanGrowth f) x))
Uses 14 · Used by 1
Statement usesWiman growth function · Radial majorant · Wiman maximum term
Proof usesThe Wiman tilted measure is a probability measure · Second derivative of the logarithmic majorant as a variance · Every real parameter is interior to the exponential-integrability set · Wiman coefficient measure · Wiman Taylor coefficient · Wiman term · Each radial Taylor term is at most the radial majorant · Each Taylor term is at most the maximum term · Radial Taylor terms are nonnegative · Tilted coefficient measure · Atoms of the tilted coefficient measure
Used byMajorant bound off an exceptional set

TheoremCauchy's inequality for the maximum term#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n\) at the origin, maximum term \(\mu(r) = \sup_n |a_n|\,|r|^n\) and maximum modulus \(M(r) = \sup_{|z| = |r|} |f(z)|\). Then \(\mu(r) \le M(r)\) for every real \(r > 0\).

theorem wimanMaximumTerm_le_wimanMaximumModulus
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    {r : ℝ} (hr : 0 < r) :
    wimanMaximumTerm f r ≤ wimanMaximumModulus f r
Uses 6 · Used by 1
Statement usesWiman maximum modulus · Wiman maximum term
Proof usesThe maximum modulus is attained · Bounding the maximum term · Wiman Taylor coefficient · Wiman term
Used byWiman's inequality with exponent \(2/3\) at arbitrarily large radii

TheoremTaylor expansion of an entire function#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n = f^{(n)}(0) / n!\) at the origin. For every \(z \in \mathbb{C}\), the series \(\sum_{n \ge 0} a_n z^n\) converges unconditionally to \(f(z)\).

theorem hasSum_wimanTaylorCoefficient_mul_pow
    (f : ℂ → ℂ) (hf : Differentiable ℂ f) (z : ℂ) :
    HasSum (fun n : ℕ => wimanTaylorCoefficient f n * z ^ n) (f z)
Uses 1 · Used by 2
Statement usesWiman Taylor coefficient
Used byTranscendental entire functions have infinitely many Taylor coefficients · The maximum modulus is at most the radial Taylor majorant

TheoremTranscendental entire functions have infinitely many Taylor coefficients#✓fully proved

A transcendental entire function has infinitely many nonzero Taylor coefficients.

theorem infinite_support_wimanTaylorCoefficient
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    (Function.support (wimanTaylorCoefficient f)).Infinite
Uses 3 · Used by 2
Statement usesTranscendental functions · Wiman Taylor coefficient
Proof usesTaylor expansion of an entire function
Used byEventual regularity of the logarithmic majorant · The maximum term of a transcendental entire function tends to infinity

TheoremThe maximum modulus is at most the radial Taylor majorant#✓fully proved

Let \(f\) be an entire function with Taylor coefficients \(a_n\) at the origin and let \(r \ge 0\). Then the maximum modulus \(M(r) = \sup_{|z| = r} |f(z)|\) satisfies \(M(r) \le \sum_{n \ge 0} |a_n| r^n\).

theorem wimanMaximumModulus_le_wimanMajorant
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    {r : ℝ} (hr : 0 ≤ r) :
    wimanMaximumModulus f r ≤ wimanMajorant f r
Uses 6 · Used by 1
Statement usesRadial majorant · Wiman maximum modulus
Proof usesThe maximum modulus is attained · Taylor expansion of an entire function · Wiman Taylor coefficient · Wiman term
Used byWiman's inequality with exponent \(2/3\) at arbitrarily large radii

TheoremThe maximum term of a transcendental entire function tends to infinity#✓fully proved

Let \(f\) be an entire function that is not a polynomial function, with Taylor coefficients \(a_n\) at the origin and maximum term \(\mu(r) = \sup_n |a_n|\,|r|^n\). Then \(\mu(r) \to \infty\) as \(r \to \infty\).

theorem tendsto_wimanMaximumTerm_atTop
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    Tendsto (wimanMaximumTerm f) atTop atTop
Uses 6 · Used by 3
Statement usesTranscendental functions · Wiman maximum term
Proof usesTranscendental entire functions have infinitely many Taylor coefficients · Wiman Taylor coefficient · Wiman term · Each Taylor term is at most the maximum term
Used byThe maximum term eventually exceeds one · Eventual regularity of the logarithmic majorant · The maximum term tends to infinity along logarithmic radii

TheoremThe maximum term eventually exceeds one#✓fully proved

Let \(f\) be an entire function that is not a polynomial function, with Taylor coefficients \(a_n\) at the origin and maximum term \(\mu(r) = \sup_n |a_n|\,|r|^n\). Then there is \(R\) such that \(\mu(r) > 1\) for all real \(r \ge R\).

theorem eventually_one_lt_wimanMaximumTerm
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    ∀ᶠ r : ℝ in atTop, 1 < wimanMaximumTerm f r
Uses 3 · Used by 1
Statement usesTranscendental functions · Wiman maximum term
Proof usesThe maximum term of a transcendental entire function tends to infinity
Used byThe logarithm of the maximum term is eventually positive

TheoremThe logarithm of the maximum term is eventually positive#✓fully proved

Let \(f\) be an entire function that is not a polynomial function, with Taylor coefficients \(a_n\) at the origin and maximum term \(\mu(r) = \sup_n |a_n|\,|r|^n\). Then there is \(R\) such that \(\log \mu(r) > 0\) for all real \(r \ge R\).

theorem eventually_pos_log_wimanMaximumTerm
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    ∀ᶠ r : ℝ in atTop, 0 < Real.log (wimanMaximumTerm f r)
Uses 3
Statement usesTranscendental functions · Wiman maximum term
Proof usesThe maximum term eventually exceeds one

TheoremEventual regularity of the logarithmic majorant#✓fully proved

Let \(f\) be a transcendental entire function with Taylor coefficients \(a_n\) at the origin, and let \(\Phi(x) = \log \sum_{n \ge 0} |a_n| e^{nx}\). Then \(\Phi\) is twice continuously differentiable on \(\mathbb{R}\), \(\Phi'(x) \to \infty\) as \(x \to \infty\), and there is a real \(x_0\) such that \(\Phi(x) > 0\) for every \(x \ge x_0\) and both \(\Phi\) and \(\Phi'\) are nondecreasing on \([x_0, \infty)\).

theorem eventually_wimanGrowth_regular
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    ∃ x₀ : ℝ,
      (∀ x, x₀ ≤ x → 0 < wimanGrowth f x) ∧
      MonotoneOn (wimanGrowth f) (Set.Ici x₀) ∧
      MonotoneOn (deriv (wimanGrowth f)) (Set.Ici x₀) ∧
      ContDiff ℝ 2 (wimanGrowth f) ∧
      Tendsto (deriv (wimanGrowth f)) atTop atTop
Uses 14 · Used by 2
Statement usesTranscendental functions · Wiman growth function
Proof usesThe logarithmic majorant is \(C^2\) · Derivative of the logarithmic majorant as a mean · Transcendental entire functions have infinitely many Taylor coefficients · The logarithmic majorant has nonnegative second derivative · The maximum term of a transcendental entire function tends to infinity · Radial majorant · Wiman maximum term · Bounding the maximum term · Wiman Taylor coefficient · Wiman term · Each radial Taylor term is at most the radial majorant · Tilted coefficient measure
Used byThe Wiman exceptional set has finite measure · Majorant bound off an exceptional set

DefinitionWiman exceptional set#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\) with radial majorant \(M_f\), let \(g(x) = \log M_f(e^x)\). For \(x_0 \in \mathbb{R}\), the Wiman exceptional set \(E_f(x_0)\) is the union of the power-growth bad sets of \(g\) and of \(g'\) with exponent \(9/8\) above \(x_0\), that is, the set of \(x \ge x_0\) with \(g(x)^{9/8} \le g'(x)\) or \(g'(x)^{9/8} \le g''(x)\).

def wimanExceptionalSet (f : ℂ → ℂ) (x₀ : ℝ) : Set ℝ :=
  Real.powerGrowthBadSet (wimanGrowth f) (9 / 8 : ℝ) x₀ ∪
    Real.powerGrowthBadSet (deriv (wimanGrowth f)) (9 / 8 : ℝ) x₀
Uses 2 · Used by 3
Statement usesWiman growth function · Power-growth exceptional set
Used byThe Wiman exceptional set has finite measure · Wiman's inequality with exponent \(2/3\) at arbitrarily large radii · Majorant bound off an exceptional set

TheoremThe Wiman exceptional set has finite measure#✓fully proved

Let \(f\) be a transcendental entire function, let \(M_f\) be its radial majorant and let \(g(x) = \log M_f(e^x)\). For \(x_0 \in \mathbb{R}\) let \(E_f(x_0)\) be the Wiman exceptional set, the set of \(x \ge x_0\) with \(g(x)^{9/8} \le g'(x)\) or \(g'(x)^{9/8} \le g''(x)\). There is \(x_0 \in \mathbb{R}\) such that \(E_f(x_0)\) has finite Lebesgue measure and \(g''(x) \le g(x)^{81/64}\) for every \(x \ge x_0\) outside \(E_f(x_0)\).

The exponent \(81/64 = (9/8)^2\) comes from composing the two growth bounds.

theorem exists_finite_wimanExceptionalSet
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    ∃ x₀ : ℝ,
      volume (wimanExceptionalSet f x₀) < ∞ ∧
      ∀ x, x₀ ≤ x → x ∉ wimanExceptionalSet f x₀ →
        iteratedDeriv 2 (wimanGrowth f) x ≤
          wimanGrowth f x ^ (81 / 64 : ℝ)
Uses 6 · Used by 1
Statement usesTranscendental functions · Wiman exceptional set · Wiman growth function
Proof usesEventual regularity of the logarithmic majorant · Power-growth exceptional set · The power-growth exceptional set has finite measure
Used byMajorant bound off an exceptional set

TheoremMajorant bound off an exceptional set#✓fully proved

Let \(f\) be a transcendental entire function with Taylor coefficients \(a_n = f^{(n)}(0)/n!\), radial majorant \(M_f(r) = \sum_n |a_n|\,|r|^n\), maximum term \(\mu_f(r) = \sup_n |a_n|\,|r|^n\) and logarithmic majorant \(g_f(x) = \log M_f(e^x)\). There are reals \(C > 0\) and \(x_0\) such that the Wiman exceptional set \(E_f(x_0)\) has finite Lebesgue measure and, for every real \(x \ge x_0\) with \(x \notin E_f(x_0)\), \(M_f(e^x) \le C\,\mu_f(e^x)\,\bigl(1 + g_f(x)^{81/128}\bigr)\).

theorem wimanMajorant_bound_off_exceptionalSet
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    ∃ C x₀ : ℝ, 0 < C ∧
      volume (wimanExceptionalSet f x₀) < ∞ ∧
      ∀ x, x₀ ≤ x → x ∉ wimanExceptionalSet f x₀ →
        wimanMajorant f (Real.exp x) ≤
          C * wimanMaximumTerm f (Real.exp x) *
            (1 + wimanGrowth f x ^ (81 / 128 : ℝ))
Uses 11 · Used by 1
Statement usesTranscendental functions · Wiman exceptional set · Wiman growth function · Radial majorant · Wiman maximum term
Proof usesEventual regularity of the logarithmic majorant · The Wiman exceptional set has finite measure · Corrected Rosenbloom estimate · Wiman term · Each Taylor term is at most the maximum term · Radial Taylor terms are nonnegative
Used byWiman's inequality with exponent \(2/3\) at arbitrarily large radii

TheoremThe maximum term tends to infinity along logarithmic radii#✓fully proved

Let \(f\) be a transcendental entire function with Taylor coefficients \(a_n\) at the origin and maximum term \(\mu(r) = \sup_{n \ge 0} |a_n| |r|^n\). Then \(\mu(e^x) \to \infty\) as \(x \to \infty\).

theorem tendsto_wimanMaximumTerm_exp_atTop
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) :
    Tendsto (fun x : ℝ => wimanMaximumTerm f (Real.exp x)) atTop atTop
Uses 3 · Used by 1
Statement usesTranscendental functions · Wiman maximum term
Proof usesThe maximum term of a transcendental entire function tends to infinity
Used byWiman's inequality with exponent \(2/3\) at arbitrarily large radii

TheoremWiman's inequality with exponent \(2/3\) at arbitrarily large radii#✓fully proved

Let \(f\) be a transcendental entire function with Taylor coefficients \(a_n\) at the origin, maximum modulus \(M(r) = \sup_{|z| = |r|} |f(z)|\) and maximum term \(\mu(r) = \sup_{n \ge 0} |a_n| |r|^n\). Then for every real \(R\) there is a real \(r > R\) with \(M(r) \le \mu(r) (\log \mu(r))^{2/3}\).

theorem exists_wiman_radius_two_thirds
    (f : ℂ → ℂ) (hf : Differentiable ℂ f)
    (htrans : IsTranscendental f) (R : ℝ) :
    ∃ r : ℝ, R < r ∧ wimanMaximumModulus f r ≤
        wimanMaximumTerm f r *
          Real.log (wimanMaximumTerm f r) ^ (2 / 3 : ℝ)
Sources
  • Filevych (2003), Matematychni Studii 20(2), 215–221. This is a strict corollary of, not the full theorem stated in, that paper.
Uses 12
Statement usesTranscendental functions · Wiman maximum modulus · Wiman maximum term
Proof usesAbsorbing constants into the exponent gap · The maximum term tends to infinity along logarithmic radii · Wiman exceptional set · Wiman growth function · Radial majorant · Majorant bound off an exceptional set · The maximum modulus is at most the radial Taylor majorant · Cauchy's inequality for the maximum term · Sets of finite Lebesgue measure contain no right half-line
58 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.