Coefficient algebra for Carlson's homogeneity recurrence

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

The nth elementary symmetric polynomial evaluated at the Carlson variables.

Equations

• DirichletTransform.carlsonElementarySymmetric n z = (MvPolynomial.eval z) (MvPolynomial.esymm ι ℂ n)

theorem DirichletTransform.carlsonElementarySymmetric_generating_polynomial {ι : Type u_1} [Fintype ι] (w : ℂ) : ∏ i : ι, (1 + MvPolynomial.C w * MvPolynomial.X i) = ∑ n ∈ Finset.range (Fintype.card ι + 1), MvPolynomial.C (w ^ n) * MvPolynomial.esymm ι ℂ n

The finite generating polynomial for the elementary symmetric coefficients.

theorem DirichletTransform.carlsonElementarySymmetric_euler {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) : ∑ i : ι, z i * (MvPolynomial.eval z) ((MvPolynomial.pderiv i) (MvPolynomial.esymm ι ℂ n)) = ↑n * carlsonElementarySymmetric n z

Euler's identity for an elementary symmetric polynomial.

theorem DirichletTransform.carlsonElementarySymmetric_generating_pderiv {ι : Type u_1} [Fintype ι] (w : ℂ) (z : ι → ℂ) (i : ι) : w * ∏ j ∈ Finset.univ.erase i, (1 + w * z j) = ∑ n ∈ Finset.range (Fintype.card ι + 1), w ^ n * (MvPolynomial.eval z) ((MvPolynomial.pderiv i) (MvPolynomial.esymm ι ℂ n))

Differentiating the generating polynomial with respect to one Carlson variable.

theorem DirichletTransform.carlsonAssociatedRecurrenceKernel_polynomial {ι : Type u_1} [Fintype ι] (a w : ℂ) (b z : ι → ℂ) : a * ∏ i : ι, (1 + w * z i) + w * ∑ i : ι, (1 - b i) * z i * ∏ j ∈ Finset.univ.erase i, (1 + w * z j) = ∑ n ∈ Finset.range (Fintype.card ι + 1), w ^ n * ((a + ↑n) * carlsonElementarySymmetric n z - ∑ i : ι, b i * z i * (MvPolynomial.eval z) ((MvPolynomial.pderiv i) (MvPolynomial.esymm ι ℂ n)))

The polynomial factor in the differentiated ray kernel, expanded as in (8.4-6).

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

Carlson's coefficient Aₙ from Relation 8.4-1 in its displayed quotient form. eval_carlsonAssociatedRecurrencePolynomial identifies its polynomial form away from the two displayed denominators.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.carlsonElementarySymmetric_card {ι : Type u_1} [Fintype ι] (z : ι → ℂ) : carlsonElementarySymmetric (Fintype.card ι) z = ∏ i : ι, z i

The top elementary symmetric polynomial is the product of all variables.

theorem DirichletTransform.carlsonAssociatedRecurrenceCoeff_card {ι : Type u_1} [Fintype ι] [Nonempty ι] {a a' : ℂ} {b z : ι → ℂ} (hsum : a + a' = ∑ i : ι, b i) (ha : a ≠ 0) (ha' : a' ≠ ↑(Fintype.card ι)) : carlsonAssociatedRecurrenceCoeff (Fintype.card ι) a a' b z = -Polynomial.eval (a + 1) (ascPochhammer ℂ (Fintype.card ι - 1)) * ∏ i : ι, z i

Carlson's last coefficient has a removable singularity at a' = card ι.

theorem DirichletTransform.carlsonAssociatedRecurrenceCoeff_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] {a a' : ℂ} (b z : ι → ℂ) (ha : a ≠ 0) (ha' : a' ≠ ↑(Fintype.card ι)) : carlsonAssociatedRecurrenceCoeff 0 a a' b z = Polynomial.eval (a' - ↑(Fintype.card ι) + 1) (ascPochhammer ℂ (Fintype.card ι - 1))

Carlson's first coefficient has a removable singularity at a = 0.

noncomputable def DirichletTransform.carlsonAssociatedRecurrencePolynomial {ι : Type u_1} [Fintype ι] (n : ℕ) (a a' : ℂ) (b : ι → ℂ) : MvPolynomial ι ℂ

The division-free polynomial coefficient in Carlson's recurrence for a nonempty index type, including its removable-singularity values. The endpoint formulas are used separately because the corresponding factors cancel against the expression involving the symmetric polynomial.

Equations

• One or more equations did not get rendered due to their size.

theorem DirichletTransform.eval_carlsonAssociatedRecurrencePolynomial {ι : Type u_1} [Fintype ι] [Nonempty ι] {n : ℕ} (hn : n ≤ Fintype.card ι) {a a' : ℂ} {b z : ι → ℂ} (hsum : a + a' = ∑ i : ι, b i) (ha : a ≠ 0) (ha' : a' ≠ ↑(Fintype.card ι)) : (MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial n a a' b) = carlsonAssociatedRecurrenceCoeff n a a' b z

Away from the two displayed denominators, the polynomial coefficients agree with Carlson's quotient formula. No parameter-dependent denominator remains in the polynomial.

theorem DirichletTransform.analyticAt_carlsonAssociatedRecurrencePolynomial_eval {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {x : E} {a a' : E → ℂ} {b : E → ι → ℂ} (ha : AnalyticAt ℂ a x) (ha' : AnalyticAt ℂ a' x) (hb : ∀ (i : ι), AnalyticAt ℂ (fun (y : E) => b y i) x) (n : ℕ) (z : ι → ℂ) : AnalyticAt ℂ (fun (y : E) => (MvPolynomial.eval z) (carlsonAssociatedRecurrencePolynomial n (a y) (a' y) (b y))) x

Polynomial recurrence coefficients depend analytically on analytic parameters.