Estimates for Carlson's R-polynomials

Home for the Section 6.2 bounds used in normally convergent series.

theorem DirichletTransform.norm_eval_carlsonPowerPolynomial_le {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : ‖(MvPolynomial.eval fun (i : ι) => ↑(u i)) (carlsonPowerPolynomial n z)‖ ≤ (∑ i : ι, ‖z i‖) ^ n

The power kernel represented by carlsonPowerPolynomial is uniformly bounded on the standard simplex by the corresponding power of the sum of the variable norms.

theorem DirichletTransform.norm_carlsonRPolynomialNumerator_le {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) {B : ℝ} (hB : 0 ≤ B) (hb : ∀ (i : ι), ‖b i‖ ≤ B) : ‖carlsonRPolynomialNumerator n b z‖ ≤ (B + ↑n) ^ n * (∑ i : ι, ‖z i‖) ^ n

theorem DirichletTransform.exists_summable_norm_regCarlsonR_div_factorial_bounded_variables {ι : Type u_1} [Fintype ι] {K : Set (ι → ℂ)} (hK : IsCompact K) {Z : ℝ} (hZ : 0 ≤ Z) : ∃ (M : ℕ → ℝ), Summable M ∧ ∀ (n : ℕ), ∀ b ∈ K, ∀ (z : ι → ℂ), ∑ i : ι, ‖z i‖ ≤ Z → ‖(↑n.factorial)⁻¹ * regCarlsonR n z b‖ ≤ M n

A summable majorant uniform in compact parameter sets and bounded node vectors.

theorem DirichletTransform.exists_summable_norm_regCarlsonR_div_factorial_on_compact_parameters {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {K : Set (ι → ℂ)} (hK : IsCompact K) : ∃ (M : ℕ → ℝ), Summable M ∧ ∀ (n : ℕ), ∀ b ∈ K, ‖(↑n.factorial)⁻¹ * regCarlsonR n z b‖ ≤ M n

On compact parameter sets the exponential generating terms have a summable majorant.