Differential operators and pointwise Carlson kernels

This file defines Carlson's partial derivatives and Euler--Poisson operators, and proves their action on the pointwise averaging kernels. Compatibility lemmas identify the coordinate and iterated derivatives with the general SCV operators, preserving Carlson's public names. The integral differentiation formulas in Associated and the integration-by-parts proof in Deriv both use this lower-level layer.

References

• [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Sections 5.3--5.4, Academic Press, 1977.

Pointwise differentiation of the averaging kernel

theorem DirichletTransform.carlsonAffineForm_update {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) (i : ι) (w : ℂ) : carlsonAffineForm (Function.update z i w) u = carlsonAffineForm z u + ↑(u i) * (w - z i)

Updating one parameter of Carlson's affine form changes its value by the corresponding simplex coordinate times the change in that parameter.

theorem DirichletTransform.hasDerivAt_carlsonAffineForm_update {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) (i : ι) : HasDerivAt (fun (w : ℂ) => carlsonAffineForm (Function.update z i w) u) (↑(u i)) (z i)

As a function of one variable z i, Carlson's affine form has derivative u i.

theorem DirichletTransform.HasDerivAt.comp_carlsonAffineForm_update {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {f' : ℂ} {z : ι → ℂ} {u : ι → ℝ} (i : ι) (hf : HasDerivAt f f' (carlsonAffineForm z u)) : HasDerivAt (fun (w : ℂ) => f (carlsonAffineForm (Function.update z i w) u)) (↑(u i) * f') (z i)

Differentiating a composed Carlson kernel with respect to z i introduces the factor u i. This is the pointwise identity underlying Carlson's formula (5.3-2).

Differential operators

noncomputable def DirichletTransform.carlsonPartialDeriv {ι : Type u_1} (i : ι) (G : (ι → ℂ) → ℂ) (z : ι → ℂ) : ℂ

The partial derivative in the Carlson variable z i, defined by updating that coordinate while holding all other coordinates fixed.

Equations

• DirichletTransform.carlsonPartialDeriv i G z = deriv (fun (w : ℂ) => G (Function.update z i w)) (z i)

theorem DirichletTransform.carlsonPartialDeriv_eq_partialDeriv {ι : Type u_1} (i : ι) (G : (ι → ℂ) → ℂ) : carlsonPartialDeriv i G = CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i G

Carlson's coordinate derivative is the scalar specialization of the SCV derivative.

theorem DirichletTransform.carlsonPartialDeriv_comp_carlsonAffineForm {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {f' : ℂ} {z : ι → ℂ} {u : ι → ℝ} (i : ι) (hf : HasDerivAt f f' (carlsonAffineForm z u)) : carlsonPartialDeriv i (fun (z : ι → ℂ) => f (carlsonAffineForm z u)) z = ↑(u i) * f'

The partial derivative of a Carlson kernel is the derivative of the univariate function times the corresponding simplex coordinate. This is the pointwise form of Carlson's formula (5.3-2).

theorem DirichletTransform.carlsonPartialDeriv_carlsonPartialDeriv_comp_carlsonAffineForm {ι : Type u_1} [Fintype ι] {f f' : ℂ → ℂ} {f'' : ℂ} {z : ι → ℂ} {u : ι → ℝ} (i j : ι) (hf : ∀ (w : ℂ), HasDerivAt f (f' w) w) (hf' : HasDerivAt f' f'' (carlsonAffineForm z u)) : carlsonPartialDeriv i (carlsonPartialDeriv j fun (z : ι → ℂ) => f (carlsonAffineForm z u)) z = ↑(u i) * ↑(u j) * f''

Mixed partial differentiation of a Carlson kernel introduces the product of the two corresponding simplex coordinates.

def DirichletTransform.carlsonIteratedPartialDeriv {ι : Type u_1} : List ι → ((ι → ℂ) → ℂ) → (ι → ℂ) → ℂ

Successive Carlson partial derivatives, in the order specified by a list of coordinate indices. The head of the list is applied last.

Equations

• DirichletTransform.carlsonIteratedPartialDeriv [] x✝¹ x✝ = x✝¹ x✝
• DirichletTransform.carlsonIteratedPartialDeriv (i :: is) x✝¹ x✝ = DirichletTransform.carlsonPartialDeriv i (fun (w : ι → ℂ) => DirichletTransform.carlsonIteratedPartialDeriv is x✝¹ w) x✝

theorem DirichletTransform.carlsonIteratedPartialDeriv_eq_iteratedPartialDeriv {ι : Type u_1} (is : List ι) (G : (ι → ℂ) → ℂ) : carlsonIteratedPartialDeriv is G = CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson is G

Carlson and SCV use the same order convention for repeated coordinate differentiation.

theorem DirichletTransform.carlsonIteratedPartialDeriv_perm {ι : Type u_1} [Fintype ι] {U : Set (ι → ℂ)} {G : (ι → ℂ) → ℂ} (hG : AnalyticOnNhd ℂ G U) (hU : IsOpen U) {is js : List ι} (h : is.Perm js) : Set.EqOn (carlsonIteratedPartialDeriv is G) (carlsonIteratedPartialDeriv js G) U

Mixed Carlson derivatives of a holomorphic function are independent of their order.

theorem DirichletTransform.carlsonIteratedPartialDeriv_comp_carlsonAffineForm {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} (hf : ∀ (n : ℕ) (w : ℂ), HasDerivAt (iteratedDeriv n f) (iteratedDeriv (n + 1) f w) w) (is : List ι) (z : ι → ℂ) (u : ι → ℝ) : carlsonIteratedPartialDeriv is (fun (z : ι → ℂ) => f (carlsonAffineForm z u)) z = (List.map (fun (i : ι) => ↑(u i)) is).prod * iteratedDeriv is.length f (carlsonAffineForm z u)

Iterated partial differentiation of a Carlson kernel introduces the corresponding product of simplex coordinates. This is the pointwise core of Carlson's formula (5.3-2).

noncomputable def DirichletTransform.carlsonTotalDeriv {ι : Type u_1} [Fintype ι] (G : (ι → ℂ) → ℂ) (z : ι → ℂ) : ℂ

The sum of the coordinate partial derivatives used in Carlson's equation (5.3-3).

Equations

• DirichletTransform.carlsonTotalDeriv G z = ∑ i : ι, DirichletTransform.carlsonPartialDeriv i G z

theorem DirichletTransform.carlsonTotalDeriv_comp_carlsonAffineForm {ι : Type u_1} [Fintype ι] {f : ℂ → ℂ} {f' : ℂ} {z : ι → ℂ} {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) (hf : HasDerivAt f f' (carlsonAffineForm z u)) : carlsonTotalDeriv (fun (z : ι → ℂ) => f (carlsonAffineForm z u)) z = f'

The total Carlson derivative of a pointwise kernel is the ordinary derivative of the averaged function, because simplex coordinates sum to one.

noncomputable def DirichletTransform.carlsonDirectionalDeriv {ι : Type u_1} [Fintype ι] (a : ι → ℂ) (G : (ι → ℂ) → ℂ) (z : ι → ℂ) : ℂ

A constant-coefficient directional differential operator in Carlson's variables.

Equations

• DirichletTransform.carlsonDirectionalDeriv a G z = ∑ i : ι, a i * DirichletTransform.carlsonPartialDeriv i G z

theorem DirichletTransform.carlsonDirectionalDeriv_comp_carlsonAffineForm {ι : Type u_1} [Fintype ι] (a : ι → ℂ) {f : ℂ → ℂ} {f' : ℂ} {z : ι → ℂ} {u : ι → ℝ} (hf : HasDerivAt f f' (carlsonAffineForm z u)) : carlsonDirectionalDeriv a (fun (z : ι → ℂ) => f (carlsonAffineForm z u)) z = (∑ i : ι, a i * ↑(u i)) * f'

Evaluation of a constant-coefficient directional derivative on a Carlson kernel. This is the first-order pointwise identity behind Carlson's more general formula (5.3-4).

noncomputable def DirichletTransform.carlsonEulerPoissonOperator {ι : Type u_1} (i j : ι) (b z : ι → ℂ) (G : (ι → ℂ) → ℂ) : ℂ

Carlson's Euler--Poisson differential expression for a twice differentiable function of the variables z. The equation in Theorem 5.4-1 asserts that this expression vanishes.

Equations

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

theorem DirichletTransform.carlsonEulerPoissonOperator_const_mul {ι : Type u_1} (c : ℂ) (i j : ι) (b z : ι → ℂ) (G : (ι → ℂ) → ℂ) : (carlsonEulerPoissonOperator i j b z fun (w : ι → ℂ) => c * G w) = c * carlsonEulerPoissonOperator i j b z G

The Euler--Poisson operator commutes with multiplication of the dependent function by a constant.

@[simp]

theorem DirichletTransform.carlsonEulerPoissonOperator_self {ι : Type u_1} (i : ι) (b z : ι → ℂ) (G : (ι → ℂ) → ℂ) : carlsonEulerPoissonOperator i i b z G = 0

The diagonal members of the Euler--Poisson system vanish identically.

theorem DirichletTransform.carlsonEulerPoissonOperator_comp_carlsonAffineForm {ι : Type u_1} [Fintype ι] (i j : ι) (b z : ι → ℂ) (u : ι → ℝ) {f f' : ℂ → ℂ} {f'' : ℂ} (hf : ∀ (w : ℂ), HasDerivAt f (f' w) w) (hf' : HasDerivAt f' f'' (carlsonAffineForm z u)) : (carlsonEulerPoissonOperator i j b z fun (z : ι → ℂ) => f (carlsonAffineForm z u)) = (z i - z j) * (↑(u i) * ↑(u j) * f'') + b i * (↑(u j) * f' (carlsonAffineForm z u)) - b j * (↑(u i) * f' (carlsonAffineForm z u))

Evaluation of the Euler--Poisson operator on a Carlson kernel. The integral of this expression is the quantity killed by Carlson's integration-by-parts argument in the proof of Theorem 5.4-1.