Hayman admissibility

DefinitionHayman auxiliary function \(A\)#✓fully proved

For a function \(G : \mathbb{C} \to \mathbb{C}\) and a real number \(r\), \(A(r)\) is the real part of \(r\,G'(r)/G(r)\), where \(G'\) is the complex derivative of \(G\).

noncomputable def haymanAuxiliaryA (G : ℂ → ℂ) (r : ℝ) : ℝ :=
  Complex.re (((r : ℂ) * deriv G (r : ℂ) / G (r : ℂ)))

Used by 3

Used byHayman auxiliary function \(B\) · Hayman's coefficient asymptotic (finite radius) · Hayman-admissible function (finite radius)

DefinitionHayman auxiliary function \(B\)#✓fully proved

For a function \(G : \mathbb{C} \to \mathbb{C}\) and a real number \(r\), \(B(r) = r\,A'(r)\), where \(A\) is the Hayman auxiliary function of \(G\), viewed as a real function of \(r\), and \(A'\) is its derivative.

noncomputable def haymanAuxiliaryB (G : ℂ → ℂ) (r : ℝ) : ℝ :=
  r * deriv (haymanAuxiliaryA G) r

Uses 1 · Used by 2

Statement usesHayman auxiliary function \(A\)

Used byHayman's coefficient asymptotic (finite radius) · Hayman-admissible function (finite radius)

DefinitionHayman-admissible function (finite radius)#✓fully proved

Let \(G : \mathbb{C} \to \mathbb{C}\), let \(R_0\) and \(\rho\) be real numbers, write \(G'\) for the complex derivative of \(G\) and \(A\), \(B\) for the Hayman auxiliary functions of \(G\), and say that a property holds for \(r\) near \(\rho\) if there is \(\eta > 0\) such that it holds for every \(r \in (R_0, \rho)\) with \(r > \rho - \eta\). Then \(G\) is Hayman admissible on \((R_0, \rho)\) when \(0 < R_0 < \rho\); \(G\) is analytic on the open disk \(|z| < \rho\); for every \(r \in (R_0, \rho)\), \(G(r)\) is a positive real number and \(r\,G'(r)/G(r)\) is real; \(A(r) \to \infty\) and \(B(r) \to \infty\) as \(r\) tends to \(\rho\) within \((R_0, \rho)\); and there is a function \(\delta : \mathbb{R} \to \mathbb{R}\) with \(0 < \delta(r) < \pi\) for \(r\) near \(\rho\) such that for every \(\varepsilon > 0\) and all \(r\) near \(\rho\), every real \(\theta\) with \(|\theta| \le \delta(r)\) satisfies the locality estimate

\[\left|G(re^{i\theta}) - G(r)\,e^{i\theta A(r) - \theta^2 B(r)/2}\right| \le \varepsilon \left|G(r)\,e^{i\theta A(r) - \theta^2 B(r)/2}\right|,\]

and every real \(\theta\) with \(\delta(r) \le |\theta| < \pi\) satisfies the decay estimate \(|G(re^{i\theta})| \le \varepsilon\,|G(r)|/\sqrt{B(r)}\).

The capture, locality and decay conditions follow the Flajolet-Sedgewick formulation rather than the abbreviated maximum-modulus restatement (Jiyou Li, "Asymptotic Estimate for the Multinomial Coefficients", Journal of Integer Sequences 23 (2020), Article 20.1.3, Lemma [Hayman] lem2), whose maximum-modulus condition is insufficient as stated and is not used.

MetaMathlibExt.IsHaymanAdmissible · 30 lines

noncomputable def IsHaymanAdmissible (G : ℂ → ℂ) (R0 ρ : ℝ) : Prop :=
  0 < R0 ∧ R0 < ρ ∧
  AnalyticOn ℂ G (Metric.ball (0 : ℂ) ρ) ∧
  (∀ r ∈ Set.Ioo R0 ρ,
    0 < Complex.re (G (r : ℂ)) ∧ Complex.im (G (r : ℂ)) = 0 ∧
    Complex.im (((r : ℂ) * deriv G (r : ℂ) / G (r : ℂ))) = 0) ∧
  Filter.Tendsto (fun r => haymanAuxiliaryA G r)
    (nhdsWithin ρ (Set.Ioo R0 ρ)) Filter.atTop ∧
  Filter.Tendsto (fun r => haymanAuxiliaryB G r)
    (nhdsWithin ρ (Set.Ioo R0 ρ)) Filter.atTop ∧
  ∃ δ : ℝ → ℝ,
    Filter.Eventually (fun r => 0 < δ r ∧ δ r < Real.pi)
      (nhdsWithin ρ (Set.Ioo R0 ρ)) ∧
    (∀ ε : ℝ, 0 < ε →
      Filter.Eventually
        (fun r => ∀ θ : ℝ, |θ| ≤ δ r →
          ‖G ((r : ℂ) * Complex.exp (Complex.I * (θ : ℂ))) -
            G (r : ℂ) * Complex.exp (Complex.I * (θ : ℂ) *
              (haymanAuxiliaryA G r : ℂ) -
              ((θ ^ 2 * haymanAuxiliaryB G r / 2 : ℝ) : ℂ))‖ ≤
          ε * ‖G (r : ℂ) * Complex.exp (Complex.I * (θ : ℂ) *
            (haymanAuxiliaryA G r : ℂ) -
            ((θ ^ 2 * haymanAuxiliaryB G r / 2 : ℝ) : ℂ))‖)
        (nhdsWithin ρ (Set.Ioo R0 ρ))) ∧
    (∀ ε : ℝ, 0 < ε →
      Filter.Eventually
        (fun r => ∀ θ : ℝ, δ r ≤ |θ| → |θ| < Real.pi →
          ‖G ((r : ℂ) * Complex.exp (Complex.I * (θ : ℂ)))‖ ≤
          ε * (‖G (r : ℂ)‖ / Real.sqrt (haymanAuxiliaryB G r)))
        (nhdsWithin ρ (Set.Ioo R0 ρ)))

Uses 2 · Used by 1

Statement usesHayman auxiliary function \(A\) · Hayman auxiliary function \(B\)

Used byHayman's coefficient asymptotic (finite radius)

TheoremHayman's coefficient asymptotic (finite radius)#✓fully proved

Let \(G : \mathbb{C} \to \mathbb{C}\) be Hayman admissible on \((R_0, \rho)\), with Hayman auxiliary functions \(A\) and \(B\). Let \((c_n)_{n \ge 0}\) be complex numbers such that \(\sum_{n \ge 0} c_n z^n\) converges absolutely to \(G(z)\) for every complex \(z\) with \(|z| < \rho\), and let \((r_n)_{n \ge 0}\) be real numbers such that for all sufficiently large \(n\), \(r_n \in (R_0, \rho)\), \(A(r_n) = n\), and \(r_n\) is the only \(r \in (R_0, \rho)\) with \(A(r) = n\). Then, as \(n \to \infty\),

\[c_n \sim \frac{G(r_n)}{r_n^n \sqrt{2\pi B(r_n)}}.\]

Proof: The saddle converges to the finite radius, Cauchy's coefficient integral is split at the admissibility cutoff, and the central Gaussian term and decaying tails are normalized separately.

theorem hayman_coefficient_asymptotic
    (G : ℂ → ℂ) (coeff : ℕ → ℂ) (R0 ρ : ℝ) (saddle : ℕ → ℝ) :
    IsHaymanAdmissible G R0 ρ →
    (∀ z : ℂ, ‖z‖ < ρ → HasSum (fun n => coeff n * z ^ n) (G z)) →
    (∀ᶠ n : ℕ in Filter.atTop, saddle n ∈ Set.Ioo R0 ρ ∧
      haymanAuxiliaryA G (saddle n) = (n : ℝ) ∧
      (∀ r ∈ Set.Ioo R0 ρ, haymanAuxiliaryA G r = (n : ℝ) → r = saddle n)) →
    Asymptotics.IsEquivalent Filter.atTop coeff
      (fun n => G (saddle n : ℂ) /
        ((saddle n : ℂ) ^ n *
          (Real.sqrt (2 * Real.pi * haymanAuxiliaryB G (saddle n)) : ℂ)))

Sources

• arXiv:1906.07169v2, tex lines 495-506.

Uses 3

Statement usesHayman-admissible function (finite radius) · Hayman auxiliary function \(A\) · Hayman auxiliary function \(B\)

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.