Deleting zero Dirichlet parameters

In the polynomial formula, a zero parameter kills every term involving its node. Combining this with equal-node aggregation deletes that coordinate altogether. The exponential series and the continued Taylor series inherit the same property. This proves Corollary 6.3-2 for holomorphic averages on disks; the general R-function specialization is in Carlson.R.ZeroParameter. The deletion statements use a nonempty remaining index type, the usual special-function setting.

theorem DirichletTransform.carlsonRPolynomialNumerator_update_of_param_zero {ι : Type u_1} [Fintype ι] (n : ℕ) {b : ι → ℂ} (z : ι → ℂ) (i : ι) (hbi : b i = 0) (w : ℂ) : carlsonRPolynomialNumerator n b (Function.update z i w) = carlsonRPolynomialNumerator n b z

A zero parameter makes the polynomial numerator independent of its node.

theorem DirichletTransform.regCarlsonR_update_of_param_zero {ι : Type u_1} [Fintype ι] (n : ℕ) {b : ι → ℂ} (z : ι → ℂ) (i : ι) (hbi : b i = 0) (w : ℂ) : regCarlsonR n (Function.update z i w) b = regCarlsonR n z b

Regularized R polynomials do not depend on nodes with zero parameter.

theorem DirichletTransform.regCarlsonSSeries_update_of_param_zero {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (z : ι → ℂ) (i : ι) (hbi : b i = 0) (w : ℂ) : regCarlsonSSeries (Function.update z i w) b = regCarlsonSSeries z b

The entire regularized S function does not depend on a zero-parameter node.

theorem DirichletTransform.regCarlsonR_option_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] (n : ℕ) {b : Option ι → ℂ} (hb : b none = 0) (z : Option ι → ℂ) : regCarlsonR n z b = regCarlsonR n (z ∘ some) (b ∘ some)

Deleting a zero parameter from a regularized R polynomial. Option ι distinguishes the deleted coordinate from the nonempty set of remaining coordinates.

theorem DirichletTransform.regCarlsonSSeries_option_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : Option ι → ℂ} (hb : b none = 0) (z : Option ι → ℂ) : regCarlsonSSeries z b = regCarlsonSSeries (z ∘ some) (b ∘ some)

Deleting a zero parameter from the entire regularized S function.

theorem DirichletTransform.IsRegCarlsonContinuation.option_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] {A : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f (Metric.ball A R)) {z : Option ι → ℂ} (hz : ‖fun (i : Option ι) => z i - A‖ < R) {G : (Option ι → ℂ) → ℂ} {H : (ι → ℂ) → ℂ} (hG : IsRegCarlsonContinuation f z G) (hH : IsRegCarlsonContinuation f (z ∘ some) H) {b : Option ι → ℂ} (hb : b none = 0) : G b = H (b ∘ some)

Zero parameters may be deleted from any continued holomorphic average on a disk (Carlson, Corollary 6.3-2), including exceptional values of the total parameter in the regularized normalization.