Integrating a joint analytic power series over a time slab

This file turns the uniform fiber series supplied by a joint analytic ball into a power series for its parameter integral over any closed time interval contained in a smaller slab.

theorem LeanPool.PoincareThreeBody.continuousOn_jointBallFiberSeries_degree (jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ) (centerTime : ℝ) (degree : ℕ) {timeBound : NNReal} (hradius : ↑timeBound < jointSeries.radius) : ContinuousOn (fun (time : ℝ) => jointBallFiberSeries jointSeries centerTime time degree) {time : ℝ | |time - centerTime| ≤ ↑timeBound}

For a fixed degree, the restricted parameter coefficient varies continuously with time as long as the time displacement remains inside the joint convergence ball.

noncomputable def LeanPool.PoincareThreeBody.jointBallFiberCoefficientBound (jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ) (timeBound : NNReal) (degree : ℕ) : NNReal

A time-independent majorant for one coefficient of the parameter fiber series.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.nnnorm_jointBallFiberSeries_le_coefficientBound (jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ) (centerTime time : ℝ) (degree : ℕ) {timeBound : NNReal} (hradius : ↑timeBound < jointSeries.radius) (htime : |time - centerTime| ≤ ↑timeBound) : ‖jointBallFiberSeries jointSeries centerTime time degree‖₊ ≤ jointBallFiberCoefficientBound jointSeries timeBound degree

Every fiber coefficient on the slab is bounded by the coefficient majorant above.

theorem LeanPool.PoincareThreeBody.summable_coefficientBound_mul_pow (jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ) {timeBound fiberRadius : NNReal} (hradii : ↑(timeBound + fiberRadius) < jointSeries.radius) : Summable fun (degree : ℕ) => ↑(jointBallFiberCoefficientBound jointSeries timeBound degree) * ↑fiberRadius ^ degree

The coefficient majorants are summable at every parameter radius whose sum with the slab half-width remains inside the original joint convergence radius.

theorem LeanPool.PoincareThreeBody.hasFPowerSeriesOnBall_setIntegral_of_joint_ball_of_measurableSet {function : ℝ × ℝ → ℝ} {jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ} {centerParameter centerTime : ℝ} {timeSet : Set ℝ} {jointRadius timeBound fiberRadius : NNReal} (hjoint : HasFPowerSeriesOnBall function jointSeries (centerParameter, centerTime) ↑jointRadius) (hfiberRadius : 0 < fiberRadius) (hradii : timeBound + fiberRadius < jointRadius) (htimeSet : MeasurableSet timeSet) (htimeFinite : MeasureTheory.volume timeSet < ⊤) (hinterval : ∀ time ∈ timeSet, |time - centerTime| ≤ ↑timeBound) : HasFPowerSeriesOnBall (fun (parameter : ℝ) => ∫ (time : ℝ) in timeSet, function (parameter, time)) (integralFormalMultilinearSeries (MeasureTheory.volume.restrict timeSet) (jointBallFiberSeries jointSeries centerTime)) centerParameter ↑fiberRadius

Integrating over a finite measurable time set contained in a joint analytic slab preserves a uniform parameter power series.

theorem LeanPool.PoincareThreeBody.hasFPowerSeriesOnBall_setIntegral_of_joint_ball {function : ℝ × ℝ → ℝ} {jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ} {centerParameter centerTime start finish : ℝ} {jointRadius timeBound fiberRadius : NNReal} (hjoint : HasFPowerSeriesOnBall function jointSeries (centerParameter, centerTime) ↑jointRadius) (hfiberRadius : 0 < fiberRadius) (hradii : timeBound + fiberRadius < jointRadius) (hinterval : ∀ time ∈ Set.Icc start finish, |time - centerTime| ≤ ↑timeBound) : HasFPowerSeriesOnBall (fun (parameter : ℝ) => ∫ (time : ℝ) in Set.Icc start finish, function (parameter, time)) (integralFormalMultilinearSeries (MeasureTheory.volume.restrict (Set.Icc start finish)) (jointBallFiberSeries jointSeries centerTime)) centerParameter ↑fiberRadius

Closed intervals are the principal special case of measurable time sets.