Uniform fiber series from one joint analytic ball

A joint power series on a ball in (parameter, time) yields parameter power series with a common radius on any smaller time slab. These are the local pieces used in the compact-interval parameter-integral theorem.

def LeanPool.PoincareThreeBody.parameterInclusion : ℝ →L[ℝ] ℝ × ℝ

The isometric inclusion of the analytic parameter as the first product coordinate.

Equations

• LeanPool.PoincareThreeBody.parameterInclusion = ContinuousLinearMap.inl ℝ ℝ ℝ

@[simp]

theorem LeanPool.PoincareThreeBody.parameterInclusion_apply (value : ℝ) : parameterInclusion value = (value, 0)

@[simp]

theorem LeanPool.PoincareThreeBody.norm_parameterInclusion : ‖parameterInclusion‖ = 1

noncomputable def LeanPool.PoincareThreeBody.jointBallFiberSeries (jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ) (centerTime time : ℝ) : FormalMultilinearSeries ℝ ℝ ℝ

Restrict a changed-origin joint series to displacement in the first coordinate.

Equations

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

theorem LeanPool.PoincareThreeBody.hasFPowerSeriesOnBall_fiber_of_joint_ball {function : ℝ × ℝ → ℝ} {jointSeries : FormalMultilinearSeries ℝ (ℝ × ℝ) ℝ} {centerParameter centerTime time : ℝ} {jointRadius timeBound fiberRadius : NNReal} (hjoint : HasFPowerSeriesOnBall function jointSeries (centerParameter, centerTime) ↑jointRadius) (htime : |time - centerTime| ≤ ↑timeBound) (hfiberRadius : 0 < fiberRadius) (hradii : timeBound + fiberRadius < jointRadius) : HasFPowerSeriesOnBall (fun (parameter : ℝ) => function (parameter, time)) (jointBallFiberSeries jointSeries centerTime time) centerParameter ↑fiberRadius

A joint analytic ball gives all nearby time fibers a common parameter radius.