Analyticity of integrals over compact parameter sets, obtained by lifting local power series and passing through a bounded integral linear map.
theorem
KamProject.Arnold1963.analyticAt_integral_compact
{X : Type u_1}
{E : Type u_2}
{F : Type u_3}
[TopologicalSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsFiniteMeasure μ]
{f : E × F → ℂ}
{g : X → F}
{p : E}
(hg : Continuous g)
{K : Set X}
(hK : IsCompact K)
(hKm : MeasurableSet K)
(hf : ∀ t ∈ K, AnalyticAt ℂ f (p, g t))
: