Analytic dependence of integrals on several complex parameters

This file combines Mathlib's dominated differentiation-under-the-integral API with finite-dimensional complex analyticity from SeveralComplexVariables.Basic. A compact-domain criterion derives the required domination from joint continuity of the pointwise derivative.

The parameter space in the analyticity criterion is an arbitrary finite-dimensional complex normed space: the statement uses Fréchet derivatives and requires no coordinates. The compact integral criteria below concern a single complex parameter and arbitrary compact integration sets, not a particular integration geometry. This material is ultimately intended near Mathlib.Analysis.Calculus.ParametricIntegral.

Main results

analyticOnNhd_integral_of_dominated_of_fderiv_le packages the existing local dominated Fréchet-derivative criterion at every point of an open finite-dimensional parameter domain.

hasDerivAt_integral_of_continuousOn_compact identifies the derivative of a compact set integral with the integral of its pointwise complex derivative. hasDerivAt_integral_mul_of_continuousOn_compact allows a fixed integrable weight, including a weight singular on the boundary. The general dominated Fréchet derivative identification is already Mathlib's hasFDerivAt_integral_of_dominated_of_fderiv_le. The integral theorem names remain in the root namespace, consistently with that API.

theorem AnalyticOnNhd.exists_cthickening_deriv_boundCarlson {Ω K : Set ℂ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f Ω) (hΩopen : IsOpen Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω) : ∃ (δ : ℝ), 0 < δ ∧ Metric.cthickening δ K ⊆ Ω ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ Metric.cthickening δ K, ‖deriv f w‖ ≤ C

The derivative of a holomorphic function is uniformly bounded on a sufficiently small closed thickening of any compact subset of its open domain.

theorem analyticOnNhd_integral_of_dominated_of_fderiv_leCarlson {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℂ P] [FiniteDimensional ℂ P] {μ : MeasureTheory.Measure α} {U : Set P} {F : P → α → E} (hU : IsOpen U) (hdom : ∀ x ∈ U, ∃ (s : Set P) (bound : α → ℝ) (F' : P → α → P →L[ℂ] E), s ∈ nhds x ∧ (∀ᶠ (y : P) in nhds x, MeasureTheory.AEStronglyMeasurable (F y) μ) ∧ MeasureTheory.Integrable (F x) μ ∧ MeasureTheory.AEStronglyMeasurable (F' x) μ ∧ (∀ᵐ (a : α) ∂μ, ∀ y ∈ s, ‖F' y a‖ ≤ bound a) ∧ MeasureTheory.Integrable bound μ ∧ ∀ᵐ (a : α) ∂μ, ∀ y ∈ s, HasFDerivAt (fun (x : P) => F x a) (F' y a) y) : AnalyticOnNhd ℂ (fun (x : P) => ∫ (a : α), F x a ∂μ) U

An integral on a finite-dimensional complex parameter space is analytic if, locally at every parameter, its pointwise Fréchet derivatives have an integrable uniform bound. The hypotheses are grouped pointwise so that the dominating function and neighborhood may depend on the base parameter.

theorem hasDerivAt_integral_of_continuousOn_compactCarlson {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace α] [BorelSpace α] [T2Space α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {K : Set α} (hK : IsCompact K) {U : Set ℂ} (hU : IsOpen U) {x : ℂ} (hx : x ∈ U) {F F' : ℂ → α → E} (hF : ContinuousOn (fun (p : ℂ × α) => F p.1 p.2) (U ×ˢ K)) (hF' : ContinuousOn (fun (p : ℂ × α) => F' p.1 p.2) (U ×ˢ K)) (hd : ∀ z ∈ U, ∀ a ∈ K, HasDerivAt (fun (w : ℂ) => F w a) (F' z a) z) : HasDerivAt (fun (z : ℂ) => ∫ (a : α) in K, F z a ∂μ) (∫ (a : α) in K, F' x a ∂μ) x

Differentiation under an integral over a compact set when the integrand and its pointwise complex derivative are jointly continuous. Compactness supplies domination.

theorem hasDerivAt_integral_mul_of_continuousOn_compactCarlson {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] [T2Space α] {μ : MeasureTheory.Measure α} {K : Set α} (hK : IsCompact K) {g : α → ℂ} (hg : MeasureTheory.IntegrableOn g K μ) {U : Set ℂ} (hU : IsOpen U) {x : ℂ} (hx : x ∈ U) {F F' : ℂ → α → ℂ} (hF : ContinuousOn (fun (p : ℂ × α) => F p.1 p.2) (U ×ˢ K)) (hF' : ContinuousOn (fun (p : ℂ × α) => F' p.1 p.2) (U ×ˢ K)) (hd : ∀ z ∈ U, ∀ a ∈ K, HasDerivAt (fun (w : ℂ) => F w a) (F' z a) z) : HasDerivAt (fun (z : ℂ) => ∫ (a : α) in K, g a * F z a ∂μ) (∫ (a : α) in K, g a * F' x a ∂μ) x

A fixed integrable scalar weight can be included in compact-domain differentiation. Only the kernel and its derivative must be jointly continuous; the weight may be singular on the boundary of the integration domain.