Integrating a uniformly controlled analytic power series

This file provides the power-series core of analyticity under a parameter integral. The compactness argument used later supplies a common radius and the summable integral bound on the coefficients.

noncomputable def LeanPool.PoincareThreeBody.integralFormalMultilinearSeries {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (series : α → FormalMultilinearSeries ℝ ℝ ℝ) : FormalMultilinearSeries ℝ ℝ ℝ

Integrate every coefficient of a measurable family of scalar formal power series.

Equations

• LeanPool.PoincareThreeBody.integralFormalMultilinearSeries μ series degree = ∫ (parameter : α), series parameter degree ∂μ

theorem LeanPool.PoincareThreeBody.hasFPowerSeriesOnBall_integral_of_uniform {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {integrand : ℝ → α → ℝ} {center : ℝ} {radius : NNReal} {series : α → FormalMultilinearSeries ℝ ℝ ℝ} (hradius : 0 < radius) (hseries : ∀ᵐ (parameter : α) ∂μ, HasFPowerSeriesOnBall (fun (value : ℝ) => integrand value parameter) (series parameter) center ↑radius) (hcoeffIntegrable : ∀ (degree : ℕ), MeasureTheory.Integrable (fun (parameter : α) => series parameter degree) μ) (hcoeffSummable : Summable fun (degree : ℕ) => (∫ (parameter : α), ‖series parameter degree‖ ∂μ) * ↑radius ^ degree) : HasFPowerSeriesOnBall (fun (value : ℝ) => ∫ (parameter : α), integrand value parameter ∂μ) (integralFormalMultilinearSeries μ series) center ↑radius

A parameter integral has the coefficientwise-integrated power series whenever all fibers share a positive radius and the integrated coefficient norms are summable at that radius.