Differentiation of associated Dirichlet averages

theorem DirichletTransform.hasDerivAt_regCarlsonDirichletAverage_update_of_bound {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) {f f' : ℂ → ℂ} {s : Set ℂ} (hs : s ∈ nhds (z i)) (hf : ∀ w ∈ s, ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, HasDerivAt f (f' (carlsonAffineForm (Function.update z i w) u)) (carlsonAffineForm (Function.update z i w) u)) (hf'_continuous : ∀ w ∈ s, ContinuousOn f' (carlsonAffineForm (Function.update z i w) '' Convexity.StdSimplex.coordinateSet ℝ ι)) {C : ℝ} (hf'_bound : ∀ w ∈ s, ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, ‖f' (carlsonAffineForm (Function.update z i w) u)‖ ≤ C) : HasDerivAt (fun (w : ℂ) => regCarlsonDirichletAverage b (Function.update z i w) f) (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ↑(u i) * f' (carlsonAffineForm z u)) (z i)

Differentiation under a regularized Carlson average under a local uniform bound for the derivative on the affine combinations met by the simplex.

theorem DirichletTransform.hasDerivAt_regCarlsonDirichletAverage_update {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) {f f' : ℂ → ℂ} (hf : ∀ (w : ℂ), HasDerivAt f (f' w) w) (hf'_continuous : Continuous f') {C : ℝ} (hf'_bound : ∀ (w : ℂ), ‖f' w‖ ≤ C) : HasDerivAt (fun (w : ℂ) => regCarlsonDirichletAverage b (Function.update z i w) f) (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ↑(u i) * f' (carlsonAffineForm z u)) (z i)

Differentiation under a regularized Carlson average when the derivative of the univariate function is globally bounded.

theorem DirichletTransform.hasDerivAt_regCarlsonDirichletAverage_update_of_analyticOnNhd {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : Set.range z ⊆ Ω) (i : ι) : HasDerivAt (fun (w : ℂ) => regCarlsonDirichletAverage b (Function.update z i w) f) (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ↑(u i) * deriv f (carlsonAffineForm z u)) (z i)

Differentiation under a regularized Carlson average when the averaged function is holomorphic on a convex neighborhood of all the nodes.

theorem DirichletTransform.carlsonPartialDeriv_regCarlsonDirichletAverage_of_analyticOnNhd {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : Set.range z ⊆ Ω) (i : ι) : carlsonPartialDeriv i (fun (w : ι → ℂ) => regCarlsonDirichletAverage b w f) z = b i * regCarlsonDirichletAverage (addDirichletUnit b i) z (deriv f)

Carlson 5.3-2, first-order form. For a function holomorphic on a convex node domain, differentiation with respect to node i raises the corresponding Dirichlet parameter.

theorem DirichletTransform.carlsonPartialDeriv_regCarlsonDirichletAverage {ι : Type u_1} [Fintype ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) {f f' : ℂ → ℂ} (hf : ∀ (w : ℂ), HasDerivAt f (f' w) w) (hf'_continuous : Continuous f') {C : ℝ} (hf'_bound : ∀ (w : ℂ), ‖f' w‖ ≤ C) : carlsonPartialDeriv i (fun (z : ι → ℂ) => regCarlsonDirichletAverage b z f) z = b i * regCarlsonDirichletAverage (addDirichletUnit b i) z f'

Regularized form of Carlson's relation 5.6-1(5): differentiating with respect to z i produces the associated average with parameter b i increased by one.

theorem DirichletTransform.carlsonIteratedPartialDeriv_regCarlsonDirichletAverage {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : Set.range z ⊆ Ω) (is : List ι) : carlsonIteratedPartialDeriv is (fun (w : ι → ℂ) => regCarlsonDirichletAverage b w f) z = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => (List.map (fun (i : ι) => ↑(u i)) is).prod * iteratedDeriv is.length f (carlsonAffineForm z u)

Carlson 5.3-2, regularized complex form. Successive partial differentiation may be taken under a Carlson average when the nodes lie in a convex domain of holomorphy.

theorem DirichletTransform.carlsonPartialDeriv_carlsonDirichletAverage_of_analyticOnNhd {ι : Type u_1} [Fintype ι] {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconv : Convex ℝ Ω) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (hz : Set.range z ⊆ Ω) (i : ι) : carlsonPartialDeriv i (fun (z : ι → ℂ) => carlsonDirichletAverage b z f) z = (b i / ∑ j : ι, b j) * carlsonDirichletAverage (addDirichletUnit b i) z (deriv f)

The unregularized coordinate derivative on a convex domain of holomorphy. Unlike the globally bounded derivative specialization, this applies to general holomorphic kernels, including exponentials and powers on their branch domains.

theorem DirichletTransform.carlsonPartialDeriv_carlsonDirichletAverage {ι : Type u_1} [Fintype ι] [Nonempty ι] {b z : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) {f f' : ℂ → ℂ} (hf : ∀ (w : ℂ), HasDerivAt f (f' w) w) (hf'_continuous : Continuous f') {C : ℝ} (hf'_bound : ∀ (w : ℂ), ‖f' w‖ ≤ C) : carlsonPartialDeriv i (fun (z : ι → ℂ) => carlsonDirichletAverage b z f) z = (b i / ∑ j : ι, b j) * carlsonDirichletAverage (addDirichletUnit b i) z f'

Carlson's relation 5.6-1(5) in its original normalization. The coefficient is the weight b i / ∑ j, b j.