Holomorphic parameters in compact contour integrals

A jointly holomorphic kernel can be integrated over a fixed compact parameter set, after a continuous parametrization and multiplication by a fixed integrable weight. The weight need not be holomorphic. In the circle specialization it includes the contour derivative and a continuous boundary function.

This is simplex-independent infrastructure for continued Cauchy representations. It does not assert a Jordan-curve theorem or homotopy invariance of contours.

theorem analyticOnNhd_integral_mul_compact_kernelCarlson {E : Type u_1} {α : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] [T2Space α] {μ : MeasureTheory.Measure α} {K : Set α} (hK : IsCompact K) {g : α → ℂ} (hg : MeasureTheory.IntegrableOn g K μ) {γ : α → ℂ} (hγ : ContinuousOn γ K) {U : Set E} (hU : IsOpen U) {W : Set (E × ℂ)} {H : E × ℂ → ℂ} (hH : AnalyticOnNhd ℂ H W) (hW : ∀ x ∈ U, ∀ t ∈ K, (x, γ t) ∈ W) : AnalyticOnNhd ℂ (fun (x : E) => ∫ (t : α) in K, g t * H (x, γ t) ∂μ) U

Holomorphic dependence of a compact weighted integral of a jointly holomorphic kernel. Only the parametrization, not the weight, must be continuous.

theorem analyticOnNhd_circleIntegral_kernel_mulCarlson {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (hU : IsOpen U) {W : Set (E × ℂ)} {H : E × ℂ → ℂ} (hH : AnalyticOnNhd ℂ H W) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) {f : ℂ → ℂ} (hf : ContinuousOn f (Metric.sphere c R)) (hW : ∀ x ∈ U, ∀ s ∈ Metric.sphere c R, (x, s) ∈ W) : AnalyticOnNhd ℂ (fun (x : E) => ∮ (s : ℂ) in C(c, R), H (x, s) * f s) U

Integrating a holomorphic parameter-dependent kernel against a continuous boundary function on a fixed circle preserves holomorphy in all parameters.