Documentation

LeanPool.CarlsonFunctions.Carlson.RPolynomial.Coefficients

Coefficients of Carlson's R-polynomials #

Home for Carlson's Section 6.2: multi-index coefficients, zero specializations, and termination.

source
theorem DirichletTransform.coeff_carlsonPowerPolynomial {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) (m : ι →₀ ℕ) :
(carlsonPowerPolynomial n z).coeff m = if (m.sum fun (x : ι) (e : ℕ) => e) = n then ↑m.multinomial * m.prod fun (i : ι) (e : ℕ) => z i ^ e else 0

The coefficient form of the multinomial theorem for Carlson's homogeneous power polynomial. This is the algebraic core of Carlson's representation 6.2-1.

source
theorem DirichletTransform.coeff_carlsonPowerPolynomial_eq_zero_of_sum_ne {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) (m : ι →₀ ℕ) (hm : (m.sum fun (x : ι) (e : ℕ) => e) ≠ n) :
(carlsonPowerPolynomial n z).coeff m = 0

Only multi-indices of total degree n can occur in Carlson's degree-n power polynomial.

source
theorem DirichletTransform.regCarlsonRPolynomial_eq_sum_support {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) :
regCarlsonRPolynomial n b z = ∑ m ∈ (carlsonPowerPolynomial n z).support, (↑m.multinomial * m.prod fun (i : ι) (e : ℕ) => z i ^ e) * regDirichletMonomialTransform (⇑m) b

Carlson's regularized polynomial written as the finite sum of its total-degree n multi-index terms.

source
theorem DirichletTransform.regCarlsonRPolynomial_eq_pochhammer_sum {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) :
regCarlsonRPolynomial n b z = ∑ m ∈ (carlsonPowerPolynomial n z).support, (↑m.multinomial * m.prod fun (i : ι) (e : ℕ) => z i ^ e) * ((∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℂ (m i))) * (Complex.Gamma (∑ i : ι, (b i + ↑(m i))))⁻¹)

Carlson's regularized polynomial written explicitly in Pochhammer--Gamma form.

source
noncomputable def DirichletTransform.carlsonRPolynomialNumerator {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) :
ℂ

The Pochhammer numerator of Carlson's degree-n R-polynomial.

Carlson's usual polynomial is obtained by dividing this expression by (∑ i, b i)ₙ. Keeping the numerator separate makes transformation identities valid without exclusions at zeros of that Pochhammer symbol.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem DirichletTransform.carlsonRPolynomialNumerator_zero {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) :
    carlsonRPolynomialNumerator 0 b z = 1

    The Pochhammer numerator of the degree-zero R-polynomial is one.

    source
    theorem DirichletTransform.carlsonRPolynomialNumerator_one {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) :
    carlsonRPolynomialNumerator 1 b z = ∑ i : ι, b i * z i

    The Pochhammer numerator in degree one is the weighted linear form ∑ i, b i * z i, as in Carlson's formula 5.7(2).

    source
    theorem DirichletTransform.regCarlsonRPolynomial_eq_numerator_mul_one_div_Gamma {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) :
    regCarlsonRPolynomial n b z = carlsonRPolynomialNumerator n b z * (Complex.Gamma (∑ i : ι, b i + ↑n))⁻¹

    The regularized Carlson polynomial is its Pochhammer numerator times the reciprocal Gamma factor at the translated total parameter.

    source
    @[simp]
    theorem DirichletTransform.carlsonPowerPolynomial_zero {ι : Type u_1} [Fintype ι] (z : ι → ℂ) :
    carlsonPowerPolynomial 0 z = 1

    Carlson's degree-zero power polynomial is the constant polynomial one.

    source
    @[simp]
    theorem DirichletTransform.carlsonPowerPolynomial_one {ι : Type u_1} [Fintype ι] (z : ι → ℂ) :
    carlsonPowerPolynomial 1 z = carlsonAffinePolynomial z

    Carlson's degree-one power polynomial is its defining affine polynomial.

    source
    @[simp]
    theorem DirichletTransform.regCarlsonRPolynomial_zero {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) :
    regCarlsonRPolynomial 0 b z = (Complex.Gamma (∑ i : ι, b i))⁻¹

    The regularized Carlson polynomial of degree zero is the reciprocal Gamma factor.

    source
    @[simp]
    theorem DirichletTransform.regCarlsonRPolynomial_zero_variables {ι : Type u_1} [Fintype ι] (b : ι → ℂ) {n : ℕ} (hn : n ≠ 0) :
    (regCarlsonRPolynomial n b fun (x : ι) => 0) = 0

    If all Carlson variables vanish, every positive-degree Carlson polynomial vanishes.

    source
    theorem DirichletTransform.map_equivFunOnFinite_piAntidiag_univ {ι : Type u_1} [Fintype ι] (n : ℕ) :
    Finset.map { toFun := ⇑Finsupp.equivFunOnFinite.symm, inj' := ⋯ } (Finset.univ.piAntidiag n) = Finset.univ.finsuppAntidiag n

    Reindexing the degree-n Finsupp antidiagonal along Finsupp.equivFunOnFinite.

    source
    theorem DirichletTransform.carlsonRPolynomialNumerator_eq_multinomial_sum {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) :
    carlsonRPolynomialNumerator n b z = ∑ m ∈ Finset.univ.piAntidiag n, (↑(Nat.multinomial Finset.univ m) * ∏ i : ι, z i ^ m i) * ∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℂ (m i))

    The Pochhammer numerator is the complete degree-n multinomial expansion.

    source
    theorem DirichletTransform.analyticAt_regCarlsonR_comp {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {x : E} {b z : E → ι → ℂ} (hb : ∀ (i : ι), AnalyticAt ℂ (fun (y : E) => b y i) x) (hz : ∀ (i : ι), AnalyticAt ℂ (fun (y : E) => z y i) x) (n : ℕ) :
    AnalyticAt ℂ (fun (y : E) => regCarlsonR n (z y) (b y)) x

    Regularized Carlson polynomials preserve analytic dependence jointly in their nodes and Dirichlet parameters.