Hamiltonian vector fields and canonical pullback, using complex Frechet derivatives and X_H = (-H_q, H_p). Derivative identities require differentiability or derive it from analyticity. Canonical maps preserve the specified symplectic form.

noncomputable def KamProject.Arnold1963.pGradient {n : ℕ} (H : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : ComplexSpace n

The action-coordinate derivatives of a complex Hamiltonian.

Equations

• KamProject.Arnold1963.pGradient H x j = (fderiv ℂ H x) (KamProject.Arnold1963.pDirection j)

noncomputable def KamProject.Arnold1963.qGradient {n : ℕ} (H : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : ComplexSpace n

The angle-coordinate derivatives of a complex Hamiltonian.

Equations

• KamProject.Arnold1963.qGradient H x j = (fderiv ℂ H x) (KamProject.Arnold1963.qDirection j)

theorem KamProject.Arnold1963.pGradient_eq_of_hasFDerivAt {n : ℕ} {H : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} {L : ComplexPhaseSpace n →L[ℂ] ℂ} (hH : HasFDerivAt H L x) : pGradient H x = fun (j : Fin n) => L (pDirection j)

theorem KamProject.Arnold1963.qGradient_eq_of_hasFDerivAt {n : ℕ} {H : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} {L : ComplexPhaseSpace n →L[ℂ] ℂ} (hH : HasFDerivAt H L x) : qGradient H x = fun (j : Fin n) => L (qDirection j)

theorem KamProject.Arnold1963.pGradient_eq_zero_of_not_differentiableAt {n : ℕ} {H : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hH : ¬DifferentiableAt ℂ H x) : pGradient H x = 0

theorem KamProject.Arnold1963.qGradient_eq_zero_of_not_differentiableAt {n : ℕ} {H : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hH : ¬DifferentiableAt ℂ H x) : qGradient H x = 0

noncomputable def KamProject.Arnold1963.hamiltonianVectorField {n : ℕ} (H : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : ComplexPhaseSpace n

Hamilton's vector field with action component -∂q H and angle component ∂p H.

Equations

• KamProject.Arnold1963.hamiltonianVectorField H x = (-KamProject.Arnold1963.qGradient H x, KamProject.Arnold1963.pGradient H x)

theorem KamProject.Arnold1963.hamiltonianVectorField_mathlibJ {n : ℕ} (H : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : phaseCoordinate (hamiltonianVectorField H x) = (Matrix.J (Fin n) ℂ).mulVec (phaseCoordinate (pGradient H x, qGradient H x))

theorem KamProject.Arnold1963.hamiltonianVectorField_eq_sharp {n : ℕ} (H : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : hamiltonianVectorField H x = symplecticSharp ↑(fderiv ℂ H x)

theorem KamProject.Arnold1963.norm_hamiltonianVectorField_le {n : ℕ} (H : ComplexPhaseSpace n → ℂ) (x : ComplexPhaseSpace n) : ‖hamiltonianVectorField H x‖ ≤ ‖fderiv ℂ H x‖

theorem KamProject.Arnold1963.hamiltonianVectorField_actionOnly {n : ℕ} {h : ComplexSpace n → ℂ} (x : ComplexPhaseSpace n) (hh : DifferentiableAt ℂ h x.1) : hamiltonianVectorField (h ∘ Prod.fst) x = (0, fun (j : Fin n) => (fderiv ℂ h x.1) (Pi.single j 1))

theorem KamProject.Arnold1963.hamiltonianVectorField_add {n : ℕ} {H K : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} (hH : DifferentiableAt ℂ H x) (hK : DifferentiableAt ℂ K x) : hamiltonianVectorField (H + K) x = hamiltonianVectorField H x + hamiltonianVectorField K x

theorem KamProject.Arnold1963.HasFDerivAt.symplectic_identity {n : ℕ} {H : ComplexPhaseSpace n → ℂ} {x : ComplexPhaseSpace n} {L : ComplexPhaseSpace n →L[ℂ] ℂ} (hH : HasFDerivAt H L x) (v : ComplexPhaseSpace n) : symplecticForm v (hamiltonianVectorField H x) = L v

theorem KamProject.Arnold1963.AnalyticPhaseFunction.hasFDerivAt {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (H : AnalyticPhaseFunction n G ρ) {x : ComplexPhaseSpace n} (hx : x ∈ phaseDomain G ρ) : HasFDerivAt H.toFun (fderiv ℂ H.toFun x) x

theorem KamProject.Arnold1963.AnalyticPhaseFunction.symplectic_identity {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (H : AnalyticPhaseFunction n G ρ) {x : ComplexPhaseSpace n} (hx : x ∈ phaseDomain G ρ) (v : ComplexPhaseSpace n) : symplecticForm v (hamiltonianVectorField H.toFun x) = (fderiv ℂ H.toFun x) v

def KamProject.Arnold1963.CanonicalAt {n : ℕ} (B : ComplexPhaseSpace n → ComplexPhaseSpace n) (x : ComplexPhaseSpace n) : Prop

Differentiability and symplecticity of a transformation's derivative at one point.

Equations

• KamProject.Arnold1963.CanonicalAt B x = (DifferentiableAt ℂ B x ∧ KamProject.Arnold1963.IsSymplecticLinear ↑(fderiv ℂ B x))

def KamProject.Arnold1963.CanonicalOn {n : ℕ} (B : ComplexPhaseSpace n → ComplexPhaseSpace n) (S : Set (ComplexPhaseSpace n)) : Prop

Pointwise canonicality of a phase transformation throughout a set.

Equations

• KamProject.Arnold1963.CanonicalOn B S = ∀ x ∈ S, KamProject.Arnold1963.CanonicalAt B x

theorem KamProject.Arnold1963.canonicalAt_id {n : ℕ} (x : ComplexPhaseSpace n) : CanonicalAt id x

theorem KamProject.Arnold1963.CanonicalAt.derivative_bijective {n : ℕ} {B : ComplexPhaseSpace n → ComplexPhaseSpace n} {x : ComplexPhaseSpace n} (hB : CanonicalAt B x) : Function.Bijective ⇑(fderiv ℂ B x)

theorem KamProject.Arnold1963.CanonicalAt.matrix_identity {n : ℕ} {B : ComplexPhaseSpace n → ComplexPhaseSpace n} {x : ComplexPhaseSpace n} (hB : CanonicalAt B x) : (phaseLinearMatrix ↑(fderiv ℂ B x)).transpose * symplecticMatrix n * phaseLinearMatrix ↑(fderiv ℂ B x) = symplecticMatrix n

theorem KamProject.Arnold1963.CanonicalAt.comp {n : ℕ} {B C : ComplexPhaseSpace n → ComplexPhaseSpace n} {x : ComplexPhaseSpace n} (hB : CanonicalAt B (C x)) (hC : CanonicalAt C x) : CanonicalAt (B ∘ C) x

theorem KamProject.Arnold1963.CanonicalOn.comp {n : ℕ} {B C : ComplexPhaseSpace n → ComplexPhaseSpace n} {S T : Set (ComplexPhaseSpace n)} (hB : CanonicalOn B T) (hC : CanonicalOn C S) (hmap : Set.MapsTo C S T) : CanonicalOn (B ∘ C) S

theorem KamProject.Arnold1963.CanonicalAt.map_hamiltonianVectorField {n : ℕ} {B : ComplexPhaseSpace n → ComplexPhaseSpace n} {x : ComplexPhaseSpace n} (hB : CanonicalAt B x) {H : ComplexPhaseSpace n → ℂ} (hH : DifferentiableAt ℂ H (B x)) : (fderiv ℂ B x) (hamiltonianVectorField (H ∘ B) x) = hamiltonianVectorField H (B x)

theorem KamProject.Arnold1963.AnalyticPhaseFunction.canonical_pullback {n : ℕ} {G : Set (ComplexSpace n)} {ρ : NNReal} (H : AnalyticPhaseFunction n G ρ) {B : ComplexPhaseSpace n → ComplexPhaseSpace n} {S : Set (ComplexPhaseSpace n)} (hB : CanonicalOn B S) (hmap : Set.MapsTo B S (phaseDomain G ρ)) {x : ComplexPhaseSpace n} (hx : x ∈ S) : (fderiv ℂ B x) (hamiltonianVectorField (H.toFun ∘ B) x) = hamiltonianVectorField H.toFun (B x)