Documentation

LeanPool.CarlsonFunctions.Carlson.TwoVariable.QuadraticSeries

The double series in Carlson's second quadratic transformation #

The coefficient convolution is Carlson's calculation in Section 6.10, pp. 165–166. Absolute convergence justifies grouping the double series by total degree. A coarse geometric majorant suffices for the local identity, which is subsequently extended by analyticity.

source
noncomputable def DirichletTransform.TwoVariable.quadraticSeriesCoeff (a c : ℂ) (m k : ℕ) :
ℂ

Coefficient of the double series before grouping terms of equal total degree.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem DirichletTransform.TwoVariable.sum_antidiagonal_quadraticSeriesCoeff (a c : ℂ) (hc : 0 < c.re) (n : ℕ) :
    ∑ mk ∈ Finset.antidiagonal n, quadraticSeriesCoeff a c mk.1 mk.2 = Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval (a + 1 - c) (ascPochhammer ℂ n) / (Polynomial.eval c (ascPochhammer ℂ n) * ↑n.factorial)

    The finite convolution that collapses Carlson's double series.

    source
    theorem DirichletTransform.TwoVariable.norm_quadraticSeriesCoeff_le (a c : ℂ) (hc : 1 / 2 ≤ c.re) (m k : ℕ) :
    ‖quadraticSeriesCoeff a c m k‖ ≤ (4 * (‖a‖ + 1)) ^ (2 * m + k)

    A coarse geometric majorant is sufficient, since the transformation is first proved in an arbitrarily small neighborhood of equal nodes.

    source
    theorem DirichletTransform.TwoVariable.summable_norm_quadraticSeries (a c w : ℂ) (hc : 1 / 2 ≤ c.re) (hw : 4 * (‖a‖ + 1) * ‖w‖ < 1 / 2) :
    Summable fun (mk : ℕ × ℕ) => ‖quadraticSeriesCoeff a c mk.1 mk.2 * w ^ (2 * (mk.1 + mk.2))‖

    Absolute convergence on a small disk, sufficient for analytic continuation.

    source
    theorem DirichletTransform.TwoVariable.tsum_quadraticSeries_eq (a c w : ℂ) (hc : 1 / 2 ≤ c.re) (hw : 4 * (‖a‖ + 1) * ‖w‖ < 1 / 2) :
    ∑' (m : ℕ) (k : ℕ), quadraticSeriesCoeff a c m k * w ^ (2 * (m + k)) = ∑' (n : ℕ), Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval (a + 1 - c) (ascPochhammer ℂ n) / (Polynomial.eval c (ascPochhammer ℂ n) * ↑n.factorial) * w ^ (2 * n)

    Regroup the absolutely convergent double series by its total degree.

    source
    theorem DirichletTransform.TwoVariable.hasSum_quadraticSeries_row (a c w : ℂ) (m : ℕ) (hw : ‖w‖ < 1) :
    HasSum (fun (k : ℕ) => quadraticSeriesCoeff a c m k * w ^ (2 * (m + k))) (Polynomial.eval a (ascPochhammer ℂ (2 * m)) / (Polynomial.eval c (ascPochhammer ℂ m) * ↑m.factorial) * w ^ (2 * m) / (1 + w ^ 2) ^ (a + ↑(2 * m)))

    Summing a row is the ordinary binomial series used on p. 165.