Averages of Cauchy's integral formula

This file develops the foundational part of [Carl77, Section 5.11]. We use Mathlib's circle integral formulation of Cauchy's theorem. Carlson works more generally with positively oriented rectifiable Jordan curves.

The integer resolvent kernel and its regularized integral are analytic away from the convex hull of the Carlson variables. A compact-domain differentiation lemma handles the possibly singular Dirichlet density. A separate product-integrability estimate justifies the interchange of circle and simplex integrals, giving the circle version of Carlson's Representation 5.11-2 for every derivative order. Joint continuation on a general convex holomorphy domain is proved separately in Dirichlet.Average.JointContinuation by integration by parts. The general Jordan-curve representation, including its continued-parameter version, remains to be proved.

References

• [Carl77] B. C. Carlson, Special Functions of Applied Mathematics, Section 5.11, Academic Press, 1977.

noncomputable def DirichletTransform.carlsonCauchyKernel {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) (u : ι → ℝ) (s : ℂ) : ℂ

The integer Cauchy kernel occurring in Carlson's Theorem 5.11-1 and Representation 5.11-2.

Equations

• DirichletTransform.carlsonCauchyKernel n z u s = (s - DirichletTransform.carlsonAffineForm z u) ^ (-(↑n + 1))

noncomputable def DirichletTransform.regCarlsonResolvent {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) (s : ℂ) : ℂ

The native regularized average of Carlson's integer Cauchy kernel.

Equations

• DirichletTransform.regCarlsonResolvent n b z s = DirichletTransform.regCarlsonDirichletAverage b z fun (w : ℂ) => (s - w) ^ (-(↑n + 1))

theorem DirichletTransform.regCarlsonResolvent_eq_regDirichletIntegral {ι : Type u_1} [Fintype ι] (n : ℕ) (b z : ι → ℂ) (s : ℂ) : regCarlsonResolvent n b z s = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => carlsonCauchyKernel n z u s

The regularized resolvent is the Dirichlet integral of the corresponding pointwise Cauchy kernel.

theorem DirichletTransform.sub_carlsonAffineForm_ne_zero_of_mem_compl_convexHull {ι : Type u_1} [Fintype ι] (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) {s : ℂ} (hs : s ∈ ((convexHull ℝ) (Set.range z))ᶜ) : s - carlsonAffineForm z u ≠ 0

The denominator of Carlson's Cauchy kernel does not vanish when s lies outside the convex hull of the Carlson variables.

theorem DirichletTransform.analyticOnNhd_carlsonCauchyKernel {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : AnalyticOnNhd ℂ (carlsonCauchyKernel n z u) ((convexHull ℝ) (Set.range z))ᶜ

For a fixed simplex point, Carlson's integer Cauchy kernel is analytic in s outside the convex hull of the variables. Integer powers make this statement branch-independent.

theorem DirichletTransform.continuousOn_carlsonCauchyKernel {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) : ContinuousOn (fun (p : ℂ × (ι → ℝ)) => carlsonCauchyKernel n z p.2 p.1) (((convexHull ℝ) (Set.range z))ᶜ ×ˢ Convexity.StdSimplex.coordinateSet ℝ ι)

Joint continuity of the Cauchy kernel outside the node convex hull and on the simplex.

theorem DirichletTransform.hasDerivAt_carlsonCauchyKernel {ι : Type u_1} [Fintype ι] (n : ℕ) (z : ι → ℂ) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) {s : ℂ} (hs : s ∈ ((convexHull ℝ) (Set.range z))ᶜ) : HasDerivAt (carlsonCauchyKernel n z u) (-(↑n + 1) * carlsonCauchyKernel (n + 1) z u s) s

Differentiation raises the order of the integer resolvent kernel.

theorem DirichletTransform.hasDerivAt_regCarlsonResolvent {ι : Type u_1} [Fintype ι] (n : ℕ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (z : ι → ℂ) {s : ℂ} (hs : s ∈ ((convexHull ℝ) (Set.range z))ᶜ) : HasDerivAt (regCarlsonResolvent n b z) (-(↑n + 1) * regCarlsonResolvent (n + 1) b z s) s

Carlson 5.11-1 on the native Dirichlet domain, with the derivative identified: the integrated integer resolvent is holomorphic outside the convex hull of its nodes.

theorem DirichletTransform.analyticOnNhd_regCarlsonResolvent {ι : Type u_1} [Fintype ι] (n : ℕ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (z : ι → ℂ) : AnalyticOnNhd ℂ (regCarlsonResolvent n b z) ((convexHull ℝ) (Set.range z))ᶜ

The regularized resolvent is analytic on the entire complement of the node convex hull, not merely a half-plane. Integer powers require no choice of logarithmic branch.

@[simp]

theorem DirichletTransform.carlsonCauchyKernel_zero {ι : Type u_1} [Fintype ι] (z : ι → ℂ) (u : ι → ℝ) (s : ℂ) : carlsonCauchyKernel 0 z u s = (s - carlsonAffineForm z u)⁻¹

The first Cauchy kernel is the usual reciprocal kernel.

theorem DirichletTransform.two_pi_I_inv_mul_circleIntegral_carlsonCauchyKernel_zero {ι : Type u_1} [Fintype ι] {c : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (z : ι → ℂ) {u : ι → ℝ} (hu : carlsonAffineForm z u ∈ Metric.ball c R) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (s : ℂ) in C(c, R), carlsonCauchyKernel 0 z u s * f s = f (carlsonAffineForm z u)

Cauchy's integral formula at a Carlson affine combination contained in a circle.

theorem DirichletTransform.regCarlsonDirichletAverage_eq_average_circleIntegral {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (z : ι → ℂ) {c : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hz : ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, carlsonAffineForm z u ∈ Metric.ball c R) : regCarlsonDirichletAverage b z f = (2 * ↑Real.pi * Complex.I)⁻¹ * ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ∮ (s : ℂ) in C(c, R), carlsonCauchyKernel 0 z u s * f s

Circle form of the first step in Carlson's Representation 5.11-2: average Cauchy's formula over the simplex, before applying Fubini to interchange the two integrals.

noncomputable def DirichletTransform.regCarlsonCauchyRepresentation {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (c : ℂ) (R : ℝ) (f : ℂ → ℂ) : ℂ

The circle-contour expression on the right side of Carlson's Representation 5.11-2, specialized to the zeroth derivative.

Equations

• DirichletTransform.regCarlsonCauchyRepresentation b z c R f = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (s : ℂ) in C(c, R), DirichletTransform.regCarlsonResolvent 0 b z s * f s

theorem DirichletTransform.circleIntegral_regDirichletIntegral {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (c : ℂ) {R : ℝ} (hR : 0 ≤ R) {F : ℂ → (ι → ℝ) → ℂ} (hF : ContinuousOn (fun (p : ℂ × (ι → ℝ)) => F p.1 p.2) (Metric.sphere c R ×ˢ Convexity.StdSimplex.coordinateSet ℝ ι)) : ∮ (s : ℂ) in C(c, R), ProbabilityTheory.regDirichletIntegral b (F s) = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ∮ (s : ℂ) in C(c, R), F s u

A continuous kernel on the circle times the simplex may be integrated in either order against a native regularized Dirichlet density. Compactness bounds the kernel; the density itself need not be continuous at the boundary.

theorem DirichletTransform.circleIntegral_regCarlsonResolvent_mul {ι : Type u_1} [Fintype ι] (n : ℕ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (z : ι → ℂ) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) {f : ℂ → ℂ} (hf : ContinuousOn f (Metric.sphere c R)) (hz : Set.range z ⊆ Metric.ball c R) : ∮ (s : ℂ) in C(c, R), regCarlsonResolvent n b z s * f s = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ∮ (s : ℂ) in C(c, R), carlsonCauchyKernel n z u s * f s

Moving the integrated resolvent through a circle integral.

theorem DirichletTransform.regCarlsonDirichletAverage_iteratedDeriv_eq_circleIntegral {ι : Type u_1} [Fintype ι] (n : ℕ) {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (z : ι → ℂ) {c : ℂ} {R : ℝ} (hR : 0 < R) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hz : Set.range z ⊆ Metric.ball c R) : regCarlsonDirichletAverage b z (iteratedDeriv n f) = ↑n.factorial * (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (s : ℂ) in C(c, R), regCarlsonResolvent n b z s * f s

Carlson's Representation 5.11-2 on a circle, for every derivative order. The native integral requires positive real parts of the Dirichlet parameters; no derivatives of f on the boundary circle are assumed.

theorem DirichletTransform.regCarlsonDirichletAverage_eq_cauchyRepresentation {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (z : ι → ℂ) {c : ℂ} {R : ℝ} (hR : 0 < R) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hz : Set.range z ⊆ Metric.ball c R) : regCarlsonDirichletAverage b z f = regCarlsonCauchyRepresentation b z c R f

Carlson's averaged Cauchy representation on a circle, for the zeroth derivative. The native integral requires positive real parts of the Dirichlet parameters.