Analyticity under integration over a compact time set

A finite subcover of the compact time set reduces the result to the one-slab theorem. We use inclusion-exclusion for the finite cover, so no explicit partition or ordering of its members is needed.

theorem LeanPool.PoincareThreeBody.analyticAt_setIntegral_of_joint_analytic {function : ℝ × ℝ → ℝ} {centerParameter : ℝ} {timeSet : Set ℝ} (hcompact : IsCompact timeSet) (hjoint : ∀ time ∈ timeSet, AnalyticAt ℝ function (centerParameter, time)) (hintegrable : ∀ᶠ (parameter : ℝ) in nhds centerParameter, MeasureTheory.IntegrableOn (fun (time : ℝ) => function (parameter, time)) timeSet MeasureTheory.volume) : AnalyticAt ℝ (fun (parameter : ℝ) => ∫ (time : ℝ) in timeSet, function (parameter, time)) centerParameter

A jointly analytic scalar function remains analytic in its first variable after integration of the second variable over a compact set. The eventual integrability assumption is exactly what is needed to identify the inclusion-exclusion sum near the center parameter.