Analytic coefficient normalization in the mass parameter

Poincaré's induction subtracts a function of the Hamiltonian from a candidate integral and then divides by the mass parameter. The differentiable slope dslope supplies the removable value at mass zero. This file establishes the analytic one-variable division theorem and applies it to each phase-space slice of the normalized residual.

theorem LeanPool.PoincareThreeBody.AnalyticAt.analyticAt_dslope {f : ℝ → ℝ} {base : ℝ} (hf : AnalyticAt ℝ f base) : AnalyticAt ℝ (dslope f base) base

The differentiable slope of an analytic one-variable function is analytic at its base point. This is the analytic form of division by a linear factor.

theorem LeanPool.PoincareThreeBody.sub_mul_dslope_eq_of_eq_zero {f : ℝ → ℝ} {base : ℝ} (hzero : f base = 0) (argument : ℝ) : (argument - base) * dslope f base argument = f argument

If an analytic function vanishes at the base point, its differentiable slope reconstructs it after multiplication by the corresponding linear factor.

noncomputable def LeanPool.PoincareThreeBody.normalizationResidual (F : ℝ → PhaseSpace → ℝ) (energyFunction : ℝ → ℝ) (mass : ℝ) (state : PhaseSpace) : ℝ

The residual obtained after subtracting a one-variable function of the Hamiltonian.

Equations

• LeanPool.PoincareThreeBody.normalizationResidual F energyFunction mass state = F mass state - energyFunction (LeanPool.PoincareThreeBody.hamiltonian mass state)

noncomputable def LeanPool.PoincareThreeBody.massNormalizedCandidate (F : ℝ → PhaseSpace → ℝ) (energyFunction : ℝ → ℝ) (mass : ℝ) (state : PhaseSpace) : ℝ

The mass-normalized residual, with the removable value at zero supplied by dslope.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.domainMassNormalizedCandidate (F : ℝ → PhaseSpace → ℝ) (energyFunction : ℝ → ℝ) (mass : ℝ) (state : PhaseSpace) : ℝ

Domain-correct normalization. Away from zero it is the literal residual quotient, so its value does not depend on the unconstrained values of F 0 at the two states excluded from the mass-zero domain. At zero it uses the removable dslope value.

Equations

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

@[simp]

theorem LeanPool.PoincareThreeBody.domainMassNormalizedCandidate_zero (F : ℝ → PhaseSpace → ℝ) (energyFunction : ℝ → ℝ) (state : PhaseSpace) : domainMassNormalizedCandidate F energyFunction 0 state = massNormalizedCandidate F energyFunction 0 state

theorem LeanPool.PoincareThreeBody.domainMassNormalizedCandidate_eq_div {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} {mass : ℝ} (hmass : mass ≠ 0) (state : PhaseSpace) : domainMassNormalizedCandidate F energyFunction mass state = normalizationResidual F energyFunction mass state / mass

theorem LeanPool.PoincareThreeBody.mass_mul_massNormalizedCandidate {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} {state : PhaseSpace} (hzero : F 0 state = energyFunction (hamiltonian 0 state)) (mass : ℝ) : mass * massNormalizedCandidate F energyFunction mass state = normalizationResidual F energyFunction mass state

Exact reconstruction of a residual whose zeroth mass coefficient has been cancelled.

theorem LeanPool.PoincareThreeBody.massNormalizedCandidate_eq_div {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} {mass : ℝ} (hmass : mass ≠ 0) {state : PhaseSpace} (hzero : F 0 state = energyFunction (hamiltonian 0 state)) : massNormalizedCandidate F energyFunction mass state = normalizationResidual F energyFunction mass state / mass

At nonzero mass the normalized candidate is the ordinary quotient of the residual by mass.

theorem LeanPool.PoincareThreeBody.domainMassNormalizedCandidate_eq_massNormalizedCandidate {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} {mass : ℝ} {state : PhaseSpace} (hzero : F 0 state = energyFunction (hamiltonian 0 state)) : domainMassNormalizedCandidate F energyFunction mass state = massNormalizedCandidate F energyFunction mass state

On a phase point where the zeroth coefficient cancels, the domain-correct and dslope normalizations coincide.

theorem LeanPool.PoincareThreeBody.analyticAt_uncurry_domainMassNormalizedCandidate_of_mass_ne {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} {z : ℝ × PhaseSpace} (hmass : z.1 ≠ 0) (hcandidate : AnalyticAt ℝ (Function.uncurry F) z) (hhamiltonian : AnalyticAt ℝ (Function.uncurry hamiltonian) z) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian z.1 z.2)) : AnalyticAt ℝ (Function.uncurry (domainMassNormalizedCandidate F energyFunction)) z

Away from the removable hypersurface mass = 0, the domain-correct normalized candidate is jointly analytic by ordinary analytic division. Thus the genuinely parameterized content of the Hadamard division step is confined to points whose mass coordinate is zero.

theorem LeanPool.PoincareThreeBody.isJointlyAnalytic_domainMassNormalizedCandidate_of_mass_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) (henergyFunction : ∀ (energy : ℝ), AnalyticAt ℝ energyFunction energy) (hmassZero : ∀ (state : PhaseSpace), (0, state) ∈ collisionFree → AnalyticAt ℝ (Function.uncurry (domainMassNormalizedCandidate F energyFunction)) (0, state)) : IsJointlyAnalytic δ (domainMassNormalizedCandidate F energyFunction)

To prove joint analyticity of the normalized family on the full parameter domain, it is enough to prove the removable extension at the mass-zero slice. All nonzero-mass points follow from ordinary analytic division.

theorem LeanPool.PoincareThreeBody.mass_mul_domainMassNormalizedCandidate {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} {state : PhaseSpace} (hzero : F 0 state = energyFunction (hamiltonian 0 state)) (mass : ℝ) : mass * domainMassNormalizedCandidate F energyFunction mass state = normalizationResidual F energyFunction mass state

Exact reconstruction for the domain-correct normalization.

theorem LeanPool.PoincareThreeBody.analyticAt_normalizationResidual_massSlice {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} (hdomain : (0, state) ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian 0 state)) : AnalyticAt ℝ (fun (mass : ℝ) => normalizationResidual F energyFunction mass state) 0

Joint analyticity of the candidate and analyticity of the energy function make every fixed phase slice of the residual analytic in mass.

theorem LeanPool.PoincareThreeBody.analyticAt_massNormalizedCandidate_massSlice {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} (hdomain : (0, state) ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian 0 state)) : AnalyticAt ℝ (fun (mass : ℝ) => massNormalizedCandidate F energyFunction mass state) 0

The removable mass quotient is analytic at zero on every fixed collision-free phase slice.

theorem LeanPool.PoincareThreeBody.massNormalizedCandidate_zero_eq_parameterCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} (hdomain : (0, state) ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian 0 state)) : massNormalizedCandidate F energyFunction 0 state = parameterCoefficient (Function.uncurry (normalizationResidual F energyFunction)) state

At mass zero the normalized candidate is exactly the first parameter coefficient of the joint residual.

theorem LeanPool.PoincareThreeBody.parameterCoefficient_normalizationResidual {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} (hdomain : (0, state) ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian 0 state)) : parameterCoefficient (Function.uncurry (normalizationResidual F energyFunction)) state = parameterCoefficient (Function.uncurry F) state - deriv energyFunction (hamiltonian 0 state) * firstMassPerturbation state

Explicit coefficient bookkeeping for one normalization step: the new zeroth coefficient is the old first mass coefficient minus the energy derivative times the Hamiltonian perturbation.

theorem LeanPool.PoincareThreeBody.massNormalizedCandidate_zero_eq_nextCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} (hdomain : (0, state) ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian 0 state)) : massNormalizedCandidate F energyFunction 0 state = parameterCoefficient (Function.uncurry F) state - deriv energyFunction (hamiltonian 0 state) * firstMassPerturbation state

Explicit value of the removable quotient at mass zero.