Locally dominated holomorphic integrals

A locally uniform integrable bound on a holomorphic integrand also bounds its derivatives on smaller balls, by the Schwarz estimate. This avoids explicit logarithmic estimates when the parameters occur in complex powers. Measurability of the derivative is kept as a separate hypothesis so that the integration space needs no topology.

theorem analyticOnNhd_integral_of_locally_dominatedCarlson {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {U : Set (ι → ℂ)} {F : (ι → ℂ) → α → ℂ} (hU : IsOpen U) (hmeas : ∀ x ∈ U, MeasureTheory.AEStronglyMeasurable (F x) μ) (hderivmeas : ∀ x ∈ U, MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℂ (fun (x : ι → ℂ) => F x a) x) μ) (hhol : ∀ᵐ (a : α) ∂μ, AnalyticOnNhd ℂ (fun (x : ι → ℂ) => F x a) U) (hdom : ∀ x ∈ U, ∃ (s : Set (ι → ℂ)) (bound : α → ℝ), s ∈ nhds x ∧ MeasureTheory.Integrable bound μ ∧ ∀ᵐ (a : α) ∂μ, ∀ y ∈ s, ‖F y a‖ ≤ bound a) : AnalyticOnNhd ℂ (fun (x : ι → ℂ) => ∫ (a : α), F x a ∂μ) U

A locally dominated holomorphic integrand has a holomorphic integral. The derivative measurability assumption is often obtained from continuity on the integration domain.