Analyticity and flatness of differential minors

The final output of Poincaré's coefficient induction is that every mass derivative of each coordinate minor vanishes at zero. This file proves the analytic consequences: the minors are analytic mass germs, infinite-order vanishing makes them locally zero, and the identity principle propagates that equality along any connected collision-free mass fiber.

noncomputable def LeanPool.PoincareThreeBody.massDifferentialMinor (F : ℝ → PhaseSpace → ℝ) (i j : Fin 4) (mass : ℝ) (state : PhaseSpace) : ℝ

A coordinate minor of the Hamiltonian and candidate phase differentials at fixed mass and phase.

Equations

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

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.mass_zero_differentialMinor_eq_zero_on_liftedEllipse {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) (hdense : HasDenseClassicalPoincareSet) {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) (i j : Fin 4) : massDifferentialMinor F i j 0 (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = 0

Coordinate-minor form of the physical leading obstruction, suitable for analytic continuation.

noncomputable def LeanPool.PoincareThreeBody.jointDifferentialMinor (F : ℝ → PhaseSpace → ℝ) (i j : Fin 4) (z : ℝ × PhaseSpace) : ℝ

The same phase-coordinate minor, expressed using the joint mass/phase differentials. This form is analytic on the full parameter domain, so the several-variable identity principle can propagate a local Poincaré obstruction between different phase points as well as different masses.

Equations

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

theorem LeanPool.PoincareThreeBody.jointDifferentialMinor_eq_massDifferentialMinor {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) {z : ℝ × PhaseSpace} (hz : z ∈ parameterDomain δ) (i j : Fin 4) : jointDifferentialMinor F i j z = massDifferentialMinor F i j z.1 z.2

On the analytic domain, the joint and curried formulations of a phase minor agree.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticOnNhd_jointDifferentialMinor {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) (i j : Fin 4) : AnalyticOnNhd ℝ (jointDifferentialMinor F i j) (parameterDomain δ)

Joint coordinate minors are analytic on the complete collision-free parameter domain.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticOnNhd_massZeroDifferentialMinor {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (i j : Fin 4) : AnalyticOnNhd ℝ (fun (state : PhaseSpace) => massDifferentialMinor F i j 0 state) massZeroCollisionFree

At mass zero, every phase differential minor is analytic on the full collision-free phase domain.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.massZeroDifferentialMinor_eq_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {base : PhaseSpace} (hbase : base ∈ massZeroCollisionFree) (i j : Fin 4) (hlocal : ∀ᶠ (state : PhaseSpace) in nhds base, massDifferentialMinor F i j 0 state = 0) : Set.EqOn (fun (state : PhaseSpace) => massDifferentialMinor F i j 0 state) 0 massZeroCollisionFree

A mass-zero minor that vanishes near one collision-free phase point vanishes on the entire connected mass-zero phase domain.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.jointDifferentialMinor_eq_zero_on_preconnected {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) (hpreconnected : IsPreconnected (parameterDomain δ)) {base : ℝ × PhaseSpace} (hbase : base ∈ parameterDomain δ) (i j : Fin 4) (hlocal : ∀ᶠ (z : ℝ × PhaseSpace) in nhds base, jointDifferentialMinor F i j z = 0) : Set.EqOn (jointDifferentialMinor F i j) 0 (parameterDomain δ)

A joint minor which vanishes near one point vanishes throughout a connected parameter domain. Unlike continuation along a fixed-state mass fiber, this permits paths which move around the collision cylinders.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.not_isIndependentSomewhere_of_local_minors_eq_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) (hpreconnected : IsPreconnected (parameterDomain δ)) {base : ℝ × PhaseSpace} (hbase : base ∈ parameterDomain δ) (hlocal : ∀ (i j : Fin 4), ∀ᶠ (z : ℝ × PhaseSpace) in nhds base, jointDifferentialMinor F i j z = 0) : ¬IsIndependentSomewhere δ F

The analytic-continuation endpoint of Poincaré's coefficient argument: local vanishing of all phase-differential minors at one point contradicts functional independence anywhere in the connected collision-free parameter domain.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.not_isIndependentSomewhere_of_local_minors_eq_zero' {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {base : ℝ × PhaseSpace} (hbase : base ∈ parameterDomain δ) (hlocal : ∀ (i j : Fin 4), ∀ᶠ (z : ℝ × PhaseSpace) in nhds base, jointDifferentialMinor F i j z = 0) : ¬IsIndependentSomewhere δ F

The connectedness-specialized form used by the final nonintegrability proof.

theorem LeanPool.PoincareThreeBody.analyticAt_phaseFDeriv_massSlice {G : ℝ × PhaseSpace → ℝ} {mass : ℝ} {state direction : PhaseSpace} (hG : AnalyticAt ℝ G (mass, state)) : AnalyticAt ℝ (fun (candidateMass : ℝ) => (fderiv ℝ (fun (candidate : PhaseSpace) => G (candidateMass, candidate)) state) direction) mass

A pure phase partial derivative of a jointly analytic family is analytic as the mass varies with phase held fixed.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticAt_massDifferentialMinor_massSlice {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) {mass : ℝ} {state : PhaseSpace} (hdomain : (mass, state) ∈ parameterDomain δ) (i j : Fin 4) : AnalyticAt ℝ (fun (candidateMass : ℝ) => massDifferentialMinor F i j candidateMass state) mass

Every Hamiltonian/candidate coordinate minor is analytic along a collision-free mass fiber.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticOnNhd_massDifferentialMinor_massSlice {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} {massSet : Set ℝ} (hdomain : ∀ mass ∈ massSet, (mass, state) ∈ parameterDomain δ) (i j : Fin 4) : AnalyticOnNhd ℝ (fun (mass : ℝ) => massDifferentialMinor F i j mass state) massSet

Analyticity throughout a collision-free mass subset.

theorem LeanPool.PoincareThreeBody.AnalyticAt.eventually_eq_zero_of_iteratedDeriv_eq_zero {f : ℝ → ℝ} {base : ℝ} (hf : AnalyticAt ℝ f base) (hflat : ∀ (n : ℕ), iteratedDeriv n f base = 0) : ∀ᶠ (argument : ℝ) in nhds base, f argument = 0

Infinite-order vanishing of an analytic real germ makes it identically zero on a neighborhood.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.massDifferentialMinor_eq_zero_on_preconnected {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} {massSet : Set ℝ} (hpreconnected : IsPreconnected massSet) (hzero : 0 ∈ massSet) (hdomain : ∀ mass ∈ massSet, (mass, state) ∈ parameterDomain δ) (i j : Fin 4) (hflat : ∀ (n : ℕ), iteratedDeriv n (fun (mass : ℝ) => massDifferentialMinor F i j mass state) 0 = 0) : Set.EqOn (fun (mass : ℝ) => massDifferentialMinor F i j mass state) 0 massSet

Taylor-flat differential minors vanish on every connected collision-free mass set containing zero.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.not_independent_on_preconnected_massFiber_of_minors_flat {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hanalytic : IsJointlyAnalytic δ F) {state : PhaseSpace} {massSet : Set ℝ} (hpreconnected : IsPreconnected massSet) (hzero : 0 ∈ massSet) (hdomain : ∀ mass ∈ massSet, (mass, state) ∈ parameterDomain δ) (hflat : ∀ (i j : Fin 4) (n : ℕ), iteratedDeriv n (fun (mass : ℝ) => massDifferentialMinor F i j mass state) 0 = 0) {mass : ℝ} (hmass : mass ∈ massSet) : ¬LinearIndependent ℝ ![fderiv ℝ (hamiltonian mass) state, fderiv ℝ (F mass) state]

Flatness of every minor at zero rules out functional independence at every mass in the same connected collision-free fiber.