Iterated Poincaré normalization

This file packages the algebra common to every order of Poincaré's coefficient induction. At each step one subtracts a function of the Hamiltonian and divides by the mass. Exact finite-order expansions then express the original candidate as a function of the Hamiltonian modulo an arbitrarily high power of the mass parameter.

noncomputable def LeanPool.PoincareThreeBody.iteratedMassNormalization (F : ℝ → PhaseSpace → ℝ) (energyFunction : ℕ → ℝ → ℝ) : ℕ → ℝ → PhaseSpace → ℝ

The sequence obtained by repeatedly subtracting a chosen energy function and dividing by the mass parameter.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.PoincareThreeBody.iteratedMassNormalization F energyFunction 0 = F

@[simp]

theorem LeanPool.PoincareThreeBody.iteratedMassNormalization_zero (F : ℝ → PhaseSpace → ℝ) (energyFunction : ℕ → ℝ → ℝ) : iteratedMassNormalization F energyFunction 0 = F

@[simp]

theorem LeanPool.PoincareThreeBody.iteratedMassNormalization_succ (F : ℝ → PhaseSpace → ℝ) (energyFunction : ℕ → ℝ → ℝ) (n : ℕ) : iteratedMassNormalization F energyFunction (n + 1) = domainMassNormalizedCandidate (iteratedMassNormalization F energyFunction n) (energyFunction n)

noncomputable def LeanPool.PoincareThreeBody.accumulatedEnergy (energyFunction : ℕ → ℝ → ℝ) (n : ℕ) (mass energy : ℝ) : ℝ

The finite sum of energy-dependent terms accumulated through order n - 1.

Equations

• LeanPool.PoincareThreeBody.accumulatedEnergy energyFunction n mass energy = ∑ k ∈ Finset.range n, mass ^ k * energyFunction k energy

@[simp]

theorem LeanPool.PoincareThreeBody.accumulatedEnergy_zero (energyFunction : ℕ → ℝ → ℝ) (mass energy : ℝ) : accumulatedEnergy energyFunction 0 mass energy = 0

theorem LeanPool.PoincareThreeBody.accumulatedEnergy_succ (energyFunction : ℕ → ℝ → ℝ) (n : ℕ) (mass energy : ℝ) : accumulatedEnergy energyFunction (n + 1) mass energy = accumulatedEnergy energyFunction n mass energy + mass ^ n * energyFunction n energy

theorem LeanPool.PoincareThreeBody.iteratedMassNormalization_exact_expansion {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℕ → ℝ → ℝ} (hcancel : ∀ (n : ℕ) (state : PhaseSpace), (0, state) ∈ collisionFree → iteratedMassNormalization F energyFunction n 0 state = energyFunction n (hamiltonian 0 state)) (n : ℕ) (mass : ℝ) (state : PhaseSpace) (hcollision : (0, state) ∈ collisionFree) : F mass state = accumulatedEnergy energyFunction n mass (hamiltonian mass state) + mass ^ n * iteratedMassNormalization F energyFunction n mass state

If every normalization step cancels its zeroth coefficient, the original candidate has an exact expansion through every finite order, with the next normalized candidate as remainder.

theorem LeanPool.PoincareThreeBody.iteratedMassNormalization_remainder {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℕ → ℝ → ℝ} (hcancel : ∀ (n : ℕ) (state : PhaseSpace), (0, state) ∈ collisionFree → iteratedMassNormalization F energyFunction n 0 state = energyFunction n (hamiltonian 0 state)) (n : ℕ) (mass : ℝ) (state : PhaseSpace) (hcollision : (0, state) ∈ collisionFree) : F mass state - accumulatedEnergy energyFunction n mass (hamiltonian mass state) = mass ^ n * iteratedMassNormalization F energyFunction n mass state

The expansion remainder is divisible by mass ^ n after subtracting the accumulated function of the Hamiltonian.

theorem LeanPool.PoincareThreeBody.differentiableAt_accumulatedEnergy {energyFunction : ℕ → ℝ → ℝ} {n : ℕ} {mass energy : ℝ} (henergy : ∀ k < n, DifferentiableAt ℝ (energyFunction k) energy) : DifferentiableAt ℝ (accumulatedEnergy energyFunction n mass) energy

Differentiability of each energy coefficient makes their finite accumulated sum differentiable in energy.

theorem LeanPool.PoincareThreeBody.massDifferentialMinor_eq_pow_mul_iteratedNormalization {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℕ → ℝ → ℝ} (hcancel : ∀ (n : ℕ) (state : PhaseSpace), (0, state) ∈ collisionFree → iteratedMassNormalization F energyFunction n 0 state = energyFunction n (hamiltonian 0 state)) {n : ℕ} {mass : ℝ} {state : PhaseSpace} (hcollision : (0, state) ∈ collisionFree) (hhamiltonian : DifferentiableAt ℝ (hamiltonian mass) state) (hnormalized : DifferentiableAt ℝ (iteratedMassNormalization F energyFunction n mass) state) (henergy : ∀ k < n, DifferentiableAt ℝ (energyFunction k) (hamiltonian mass state)) (i j : Fin 4) : massDifferentialMinor F i j mass state = mass ^ n * phaseCovectorMinor (fderiv ℝ (hamiltonian mass) state) (fderiv ℝ (iteratedMassNormalization F energyFunction n mass) state) i j

At every finite normalization order, each differential minor of the original candidate is a power of the mass times the corresponding minor of the normalized remainder.

theorem LeanPool.PoincareThreeBody.iteratedDeriv_eq_zero_of_eventually_eq_pow_mul {f g : ℝ → ℝ} {order power : ℕ} (horder : order < power) (hg : ContDiffAt ℝ (↑order) g 0) (heq : f =ᶠ[nhds 0] fun (mass : ℝ) => mass ^ power * g mass) : iteratedDeriv order f 0 = 0

A germ divisible by a strictly higher power than the requested derivative order has that derivative equal to zero.

theorem LeanPool.PoincareThreeBody.massDifferentialMinor_flat_of_iterated_normalizations {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℕ → ℝ → ℝ} (hδ : 0 < δ) (hnormalized : ∀ (n : ℕ), IsJointlyAnalytic δ (iteratedMassNormalization F energyFunction n)) (henergy : ∀ (n : ℕ) (energy : ℝ), AnalyticAt ℝ (energyFunction n) energy) (hcancel : ∀ (n : ℕ) (state : PhaseSpace), (0, state) ∈ collisionFree → iteratedMassNormalization F energyFunction n 0 state = energyFunction n (hamiltonian 0 state)) {state : PhaseSpace} (hcollision : (0, state) ∈ collisionFree) (i j : Fin 4) (order : ℕ) : iteratedDeriv order (fun (mass : ℝ) => massDifferentialMinor F i j mass state) 0 = 0

If every normalized remainder stays jointly analytic and every zeroth coefficient is removed as a function of the Hamiltonian, every mass derivative of every original differential minor vanishes at zero. This is the formal infinite-order conclusion of Poincaré's induction.

theorem LeanPool.PoincareThreeBody.not_linearIndependent_of_iterated_normalizations_of_vertical_ne_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℕ → ℝ → ℝ} (hδ : 0 < δ) (hnormalized : ∀ (n : ℕ), IsJointlyAnalytic δ (iteratedMassNormalization F energyFunction n)) (henergy : ∀ (n : ℕ) (energy : ℝ), AnalyticAt ℝ (energyFunction n) energy) (hcancel : ∀ (n : ℕ) (state : PhaseSpace), (0, state) ∈ collisionFree → iteratedMassNormalization F energyFunction n 0 state = energyFunction n (hamiltonian 0 state)) {mass : ℝ} (hmass : |mass| < δ) {state : PhaseSpace} (hvertical : state 1 ≠ 0) : ¬LinearIndependent ℝ ![fderiv ℝ (hamiltonian mass) state, fderiv ℝ (F mass) state]

The infinite normalization conclusion rules out independence at every point off the horizontal axis. For such a phase point, its whole mass interval avoids both collision cylinders and hence lies in one connected mass fiber.

def LeanPool.PoincareThreeBody.verticalPerturbation (state : PhaseSpace) (offset : ℝ) : PhaseSpace

Perturb only the vertical position coordinate.

Equations

• LeanPool.PoincareThreeBody.verticalPerturbation state offset = state + offset • LeanPool.PoincareThreeBody.coordinateVector 1

@[simp]

theorem LeanPool.PoincareThreeBody.verticalPerturbation_vertical (state : PhaseSpace) (offset : ℝ) : verticalPerturbation state offset 1 = state 1 + offset

theorem LeanPool.PoincareThreeBody.not_isIndependentSomewhere_of_iterated_normalizations {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℕ → ℝ → ℝ} (hδ : 0 < δ) (hnormalized : ∀ (n : ℕ), IsJointlyAnalytic δ (iteratedMassNormalization F energyFunction n)) (henergy : ∀ (n : ℕ) (energy : ℝ), AnalyticAt ℝ (energyFunction n) energy) (hcancel : ∀ (n : ℕ) (state : PhaseSpace), (0, state) ∈ collisionFree → iteratedMassNormalization F energyFunction n 0 state = energyFunction n (hamiltonian 0 state)) : ¬IsIndependentSomewhere δ F

The full abstract endpoint of the infinite coefficient induction. Independence at a point on the horizontal axis persists under a small vertical perturbation, reducing it to the connected mass-fiber result above.

def LeanPool.PoincareThreeBody.ClassicalNormalizationPrinciple : Prop

The remaining classical input, isolated as an induction principle: every analytic first integral admits energy functions which cancel all successive Kepler-limit coefficients while the normalized remainders remain jointly analytic.

Equations

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

theorem LeanPool.PoincareThreeBody.nonintegrability_of_classicalNormalizationPrinciple (hprinciple : ClassicalNormalizationPrinciple) : ¬∃ (δ : ℝ), 0 < δ ∧ ∃ (F : ℝ → PhaseSpace → ℝ), IsJointlyAnalytic δ F ∧ IsFirstIntegralFamily δ F ∧ IsIndependentSomewhere δ F

Poincaré nonintegrability follows from the classical all-orders normalization principle.