Rényi–Vincze characterization of the exponential

DefinitionHayman Problem 2.32: a non-exponential solution of the Rényi–Vincze conditions#✓fully proved

There exist a function \(f : \mathbb{C} \to \mathbb{C}\) and real numbers \(a_0, a_1, a_2, \dots\) such that \(f\) is not the function \(z \mapsto c\,e^z\) for any real \(c > 0\); \(a_n \ge 0\) for every \(n\); \(a_n \ne 0\) for infinitely many \(n\); for every \(z \in \mathbb{C}\) the series \(\sum_{n \ge 0} a_n z^n\) has sum \(f(z)\); \(f\) is entire; and either \(\int_0^\infty a_n x^n / f(x)\,dx = 1\) for every \(n \ge 0\) (condition (2.6)), or \(\int_0^\infty f(\rho x) / f(x)\,dx = 1/(1-\rho)\) for every real \(\rho\) with \(0 < \rho < 1\) (condition (2.6)').

def conjecture : Prop :=
  ∃ (f : Complex → Complex) (a : Nat → Real),
    (∀ c : ℝ, 0 < c → f ≠ fun z => (↑c : ℂ) * Complex.exp z) ∧
    (∀ n : Nat, 0 ≤ a n) ∧
    (∀ N : Nat, ∃ n : Nat, N ≤ n ∧ a n ≠ 0) ∧
    (∀ z : Complex, HasSum (fun n => (↑(a n) : Complex) * z ^ n) (f z)) ∧
    DifferentiableOn Complex f (Set.univ : Set Complex) ∧
    ((∀ n : Nat,
        ∫ x in Set.Ici (0 : Real), (↑(a n * x ^ n) : Complex) / f (↑x : Complex) ∂MeasureTheory.volume = (1 : Complex)) ∨
      (∀ ρ : Real, 0 < ρ → ρ < 1 →
        ∫ x in Set.Ici (0 : Real), f (↑(ρ * x) : Complex) / f (↑x : Complex) ∂MeasureTheory.volume = (1 : Complex) / (1 - (↑ρ : Complex))))

Sources

• AMR-022-2032, Hayman - Research Problems in Function Theory (2018), Problem 2.32 (https://arxiv.org/abs/1809.07200, source labels 2.6 and 2.6', A. Renyi, St. Vincze).

Used by 1

Used byNo non-exponential solution of the Rényi–Vincze conditions

TheoremNo non-exponential solution of the Rényi–Vincze conditions#●ready to prove

There are no function \(f : \mathbb{C} \to \mathbb{C}\) and real numbers \(a_0, a_1, a_2, \dots\) such that \(f\) is not the function \(z \mapsto c\,e^z\) for any real \(c > 0\); \(a_n \ge 0\) for every \(n\); \(a_n \ne 0\) for infinitely many \(n\); for every \(z \in \mathbb{C}\) the series \(\sum_{n \ge 0} a_n z^n\) has sum \(f(z)\); \(f\) is entire; and either \(\int_0^\infty a_n x^n / f(x)\,dx = 1\) for every \(n \ge 0\), or \(\int_0^\infty f(\rho x) / f(x)\,dx = 1/(1-\rho)\) for every real \(\rho\) with \(0 < \rho < 1\).

Miles and Williamson (J. London Math. Soc. (2) 33 (1986) 110-116) proved that a transcendental entire \(f\) with positive coefficients and \(\int_0^\infty a_n x^n / f(x)\,dx = 1\) for all \(n\) is \(c\,e^z\). The first integral condition forces every \(a_n > 0\), and the second reduces to the first.

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Antonio Greco and Andrea Loi, Radial balanced metrics on the unit disk, arXiv:0803.3711 (2008), https://arxiv.org/abs/0803.3711.

Uses 1

Statement usesHayman Problem 2.32: a non-exponential solution of the Rényi–Vincze conditions

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.