Parameterized analytic division

This file develops the several-variable Hadamard-division input needed by Poincaré's normalization. The homotopy (mass, phase) ↦ (t * mass, phase) reduces division by the mass coordinate to integration of the mass partial derivative along 0 ≤ t ≤ 1.

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.ParameterPhase : Type

Product of the perturbing mass parameter and the phase space.

Equations

• LeanPool.PoincareThreeBody.ParameterPhase = (ℝ × LeanPool.PoincareThreeBody.PhaseSpace)

def LeanPool.PoincareThreeBody.massScale (t : ℝ) : ParameterPhase →L[ℝ] ParameterPhase

Scale the mass coordinate while leaving every phase coordinate fixed.

Equations

• LeanPool.PoincareThreeBody.massScale t = (t • ContinuousLinearMap.fst ℝ ℝ LeanPool.PoincareThreeBody.PhaseSpace).prod (ContinuousLinearMap.snd ℝ ℝ LeanPool.PoincareThreeBody.PhaseSpace)

@[simp]

theorem LeanPool.PoincareThreeBody.massScale_apply (t : ℝ) (z : ℝ × PhaseSpace) : (massScale t) z = (t * z.1, z.2)

theorem LeanPool.PoincareThreeBody.continuous_massScale : Continuous massScale

def LeanPool.PoincareThreeBody.massDirection : ParameterPhase

The distinguished unit direction in the mass coordinate.

Equations

• LeanPool.PoincareThreeBody.massDirection = (1, 0)

@[simp]

theorem LeanPool.PoincareThreeBody.massDirection_fst : massDirection.1 = 1

@[simp]

theorem LeanPool.PoincareThreeBody.massDirection_snd : massDirection.2 = 0

@[simp]

theorem LeanPool.PoincareThreeBody.norm_massDirection : ‖massDirection‖ = 1

theorem LeanPool.PoincareThreeBody.norm_massScale_le_one {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ‖massScale t‖ ≤ 1

On the unit interval, the mass-scaling homotopy is norm nonexpanding.

noncomputable def LeanPool.PoincareThreeBody.massPartialSeries (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (t : ℝ) : FormalMultilinearSeries ℝ ParameterPhase ℝ

The power series of the mass partial derivative after applying the mass-scaling homotopy to its input variables.

Equations

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

theorem LeanPool.PoincareThreeBody.massPartialSeries_apply (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (t : ℝ) (n : ℕ) (v : Fin n → ParameterPhase) : (massPartialSeries p t n) v = ((p.derivSeries n) fun (i : Fin n) => (massScale t) (v i)) massDirection

theorem LeanPool.PoincareThreeBody.continuous_massPartialSeries_coeff (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (n : ℕ) : Continuous fun (t : ℝ) => massPartialSeries p t n

noncomputable def LeanPool.PoincareThreeBody.massPartialTerm (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (x : ParameterPhase) (n : ℕ) : C(ℝ, ℝ)

One evaluated coefficient, bundled as a continuous function of the homotopy parameter.

Equations

• LeanPool.PoincareThreeBody.massPartialTerm p x n = { toFun := fun (t : ℝ) => (LeanPool.PoincareThreeBody.massPartialSeries p t n) fun (x_1 : Fin n) => x, continuous_toFun := ⋯ }

@[simp]

theorem LeanPool.PoincareThreeBody.massPartialTerm_apply (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (x : ParameterPhase) (n : ℕ) (t : ℝ) : (massPartialTerm p x n) t = (massPartialSeries p t n) fun (x_1 : Fin n) => x

def LeanPool.PoincareThreeBody.unitIntervalCompact : TopologicalSpace.Compacts ℝ

The unoriented unit interval, bundled as a compact set.

Equations

• LeanPool.PoincareThreeBody.unitIntervalCompact = { carrier := Set.uIcc 0 1, isCompact' := LeanPool.PoincareThreeBody.unitIntervalCompact._proof_1 }

noncomputable def LeanPool.PoincareThreeBody.massPartialTermUnit (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (x : ParameterPhase) (n : ℕ) : C(↥unitIntervalCompact, ℝ)

A mass-partial power-series coefficient restricted to the compact unit interval.

Equations

• LeanPool.PoincareThreeBody.massPartialTermUnit p x n = ContinuousMap.restrict (↑LeanPool.PoincareThreeBody.unitIntervalCompact) (LeanPool.PoincareThreeBody.massPartialTerm p x n)

theorem LeanPool.PoincareThreeBody.norm_massPartialSeries_le (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (n : ℕ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ‖massPartialSeries p t n‖ ≤ ‖p.derivSeries n‖

Uniform coefficient bound along the unit homotopy interval.

theorem LeanPool.PoincareThreeBody.norm_massPartialTerm_restrict_le (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (x : ParameterPhase) (n : ℕ) : ‖massPartialTermUnit p x n‖ ≤ ‖p.derivSeries n‖ * ‖x‖ ^ n

theorem LeanPool.PoincareThreeBody.summable_norm_massPartialTerm_restrict (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) {x : ParameterPhase} (hx : x ∈ Metric.eball 0 p.derivSeries.radius) : Summable fun (n : ℕ) => ‖massPartialTermUnit p x n‖

noncomputable def LeanPool.PoincareThreeBody.integratedMassPartialSeries (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) : FormalMultilinearSeries ℝ ParameterPhase ℝ

Integrating the mass-partial series along the scaling homotopy gives the formal series for the removable mass quotient.

Equations

• LeanPool.PoincareThreeBody.integratedMassPartialSeries p n = ∫ (t : ℝ) in 0..1, LeanPool.PoincareThreeBody.massPartialSeries p t n

theorem LeanPool.PoincareThreeBody.integratedMassPartialSeries_apply (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (n : ℕ) (v : Fin n → ParameterPhase) : (integratedMassPartialSeries p n) v = ∫ (t : ℝ) in 0..1, (massPartialSeries p t n) v

theorem LeanPool.PoincareThreeBody.hasSum_integratedMassPartialSeries (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) {x : ParameterPhase} (hx : x ∈ Metric.eball 0 p.derivSeries.radius) : HasSum (fun (n : ℕ) => (integratedMassPartialSeries p n) fun (x_1 : Fin n) => x) (∫ (t : ℝ) in 0..1, ∑' (n : ℕ), (massPartialTerm p x n) t)

noncomputable def LeanPool.PoincareThreeBody.parameterizedMassIntegral (f : ParameterPhase → ℝ) (base z : ParameterPhase) : ℝ

Homotopy formula for the removable quotient: integrate the mass partial derivative from the zero-mass slice to the requested mass while keeping the phase coordinates fixed.

Equations

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

theorem LeanPool.PoincareThreeBody.HasFPowerSeriesOnBall.tsum_massPartialTerm_eq_massDerivative {f : ParameterPhase → ℝ} {p : FormalMultilinearSeries ℝ ParameterPhase ℝ} {base : ParameterPhase} {r : ENNReal} (hp : HasFPowerSeriesOnBall f p base r) {x : ParameterPhase} (hx : x ∈ Metric.eball 0 r) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∑' (n : ℕ), (massPartialTerm p x n) t = (fderiv ℝ f (base + (massScale t) x)) massDirection

theorem LeanPool.PoincareThreeBody.HasFPowerSeriesOnBall.hasSum_parameterizedMassIntegral {f : ParameterPhase → ℝ} {p : FormalMultilinearSeries ℝ ParameterPhase ℝ} {base : ParameterPhase} {r : ENNReal} (hp : HasFPowerSeriesOnBall f p base r) {x : ParameterPhase} (hx : x ∈ Metric.eball 0 r) : HasSum (fun (n : ℕ) => (integratedMassPartialSeries p n) fun (x_1 : Fin n) => x) (PoincareThreeBody.parameterizedMassIntegral f base (base + x))

theorem LeanPool.PoincareThreeBody.norm_integratedMassPartialSeries_le (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) (n : ℕ) : ‖integratedMassPartialSeries p n‖ ≤ ‖p.derivSeries n‖

Integration over the unit interval does not reduce the convergence radius supplied by the derivative series.

theorem LeanPool.PoincareThreeBody.derivSeries_radius_le_integratedMassPartialSeries_radius (p : FormalMultilinearSeries ℝ ParameterPhase ℝ) : p.derivSeries.radius ≤ (integratedMassPartialSeries p).radius

theorem LeanPool.PoincareThreeBody.HasFPowerSeriesOnBall.parameterizedMassIntegral {f : ParameterPhase → ℝ} {p : FormalMultilinearSeries ℝ ParameterPhase ℝ} {base : ParameterPhase} {r : ENNReal} (hp : HasFPowerSeriesOnBall f p base r) : HasFPowerSeriesOnBall (PoincareThreeBody.parameterizedMassIntegral f base) (integratedMassPartialSeries p) base r

The homotopy integral has the integrated derivative series as a genuine power series on the same ball as the original analytic function.

theorem LeanPool.PoincareThreeBody.AnalyticAt.analyticAt_parameterizedMassIntegral {f : ParameterPhase → ℝ} {base : ParameterPhase} (hf : AnalyticAt ℝ f base) : AnalyticAt ℝ (parameterizedMassIntegral f base) base

Parameterized analytic Hadamard lemma in integral form.

theorem LeanPool.PoincareThreeBody.deriv_curry_left_at {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] {G : ℝ × B → ℝ} {mass : ℝ} {b : B} (hG : DifferentiableAt ℝ G (mass, b)) : deriv (fun (m : ℝ) => G (m, b)) mass = (fderiv ℝ G (mass, b)) (1, 0)

The derivative of a mass slice is the joint derivative in the pure mass direction.

theorem LeanPool.PoincareThreeBody.HasFPowerSeriesOnBall.mass_mul_parameterizedMassIntegral {f : ParameterPhase → ℝ} {p : FormalMultilinearSeries ℝ ParameterPhase ℝ} {baseState : PhaseSpace} {r : ENNReal} (hp : HasFPowerSeriesOnBall f p (0, baseState) r) {x : ParameterPhase} (hx : x ∈ Metric.eball 0 r) : x.1 * PoincareThreeBody.parameterizedMassIntegral f (0, baseState) ((0, baseState) + x) = f ((0, baseState) + x) - f ((0, baseState) + (0, x.2))

Fundamental-theorem identity behind parameterized division.

theorem LeanPool.PoincareThreeBody.analyticAt_uncurry_domainMassNormalizedCandidate_mass_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (henergy : ∀ (energy : ℝ), AnalyticAt ℝ energyFunction energy) (hcancel : ∀ (state : PhaseSpace), (0, state) ∈ collisionFree → F 0 state = energyFunction (hamiltonian 0 state)) {state : PhaseSpace} (hcollision : (0, state) ∈ collisionFree) : AnalyticAt ℝ (Function.uncurry (domainMassNormalizedCandidate F energyFunction)) (0, state)

The parameterized integral supplies the removable analytic extension of the normalized residual at every collision-free point of the mass-zero slice.

theorem LeanPool.PoincareThreeBody.jointAnalyticMassDivisionPrinciple : JointAnalyticMassDivisionPrinciple

Analytic Hadamard division by the mass parameter, with cancellation required only on the actual collision-free mass-zero domain.