Sharp bounds for Carlson polynomials

Carlson's inequality 6.2-7(24) uses the maximum node norm, not the sum of node norms. This distinction preserves the full Taylor disk in Section 6.3.

theorem DirichletTransform.norm_carlsonRPolynomialNumerator_le_pochhammer {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) {B : ι → ℝ} (hb : ∀ (i : ι), ‖b i‖ ≤ B i) {r : ℝ} (hr : 0 ≤ r) (hz : ∀ (i : ι), ‖z i‖ ≤ r) : ‖carlsonRPolynomialNumerator n b z‖ ≤ Polynomial.eval (∑ i : ι, B i) (ascPochhammer ℝ n) * r ^ n

Carlson 6.2-7(24), with independent nonnegative bounds for the parameter norms.

theorem DirichletTransform.norm_carlsonRPolynomialNumerator_le_sum_norm {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) {r : ℝ} (hr : 0 ≤ r) (hz : ∀ (i : ι), ‖z i‖ ≤ r) : ‖carlsonRPolynomialNumerator n b z‖ ≤ Polynomial.eval (∑ i : ι, ‖b i‖) (ascPochhammer ℝ n) * r ^ n

The parameter majorant in 6.2-7 can be chosen to be the parameter norms themselves.

theorem DirichletTransform.exists_uniform_norm_invGamma_sum_add_nat {ι : Type u_1} [Fintype ι] {K : Set (ι → ℂ)} (hK : IsCompact K) : ∃ (m : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ b ∈ K, ∀ (n : ℕ), ‖(Complex.Gamma (∑ i : ι, b i + (↑n + ↑m)))⁻¹‖ ≤ C / ↑n.factorial

Uniform factorial decay for reciprocal Gamma after sufficiently many shifts of the total parameter on a compact set.

theorem DirichletTransform.exists_summable_norm_carlsonTaylor_bounded_variables {ι : Type u_1} [Fintype ι] {K : Set (ι → ℂ)} (hK : IsCompact K) {a : ℕ → ℂ} {C q r : ℝ} (hC : 0 ≤ C) (hq : 0 ≤ q) (hr : 0 ≤ r) (hqr : q * r < 1) (ha : ∀ (n : ℕ), ‖a n‖ ≤ C * q ^ n) : ∃ (M : ℕ → ℝ), Summable M ∧ ∀ (n : ℕ), ∀ b ∈ K, ∀ (z : ι → ℂ), (∀ (i : ι), ‖z i‖ ≤ r) → ‖a n * regCarlsonR n z b‖ ≤ M n

A normally convergent majorant for the Taylor construction on compact parameter sets and bounded node vectors. The only radius restriction is q * r < 1.