Imports
The Classical Harmonic Oscillator
i. Overview
The classical harmonic oscillator is a classical mechanical system corresponding to a
mass m under a force - k x where k is the spring constant and x is the position.
In this file, a coordinate system is assumed where position and velocity both have type
EuclideanSpace ℝ (Fin 1). This is a simpler model often used for pedagogical purpose,
but only works because both the configuration space (position) and its tangent space (velocity)
are isomorphic to Euclidean Space. A proper formalisation should include the geometric properties
of the state space via manifolds and tangent bundles.
ii. Key results
The key results in the study of the classical harmonic oscillator are the follows:
In the Basic module:
HarmonicOscillator contains the input data to the problem.
EquationOfMotion defines the equation of motion for the harmonic oscillator.
energy_conservation_of_equationOfMotion proves that a trajectory satisfying the
equation of motion conserves energy.
equationOfMotion_tfae proves that the equation of motion of motion is equivalent to
Newton's second law,
Hamilton's equations,
the variational principal for the action,
the Hamilton variation principal.
In the Solution module:
InitialConditions is a structure for the initial conditions for the harmonic oscillator.
trajectories is the trajectories to the harmonic oscillator for given initial conditions.
trajectories_equationOfMotion proves that the solution satisfies the equation of motion.
iii. Table of contents
A. The input data
B. The angular frequency
C. The energies
C.1. The definitions of the energies
C.2. Simple equalities for the energies
C.3. Differentiability of the energies
C.4. Time derivatives of the energies
D. Lagrangian and the equation of motion
D.1. The Lagrangian
D.1.1. Equalities for the lagrangian
D.1.2. Smoothness of the lagrangian
D.1.3. Gradients of the lagrangian
D.2. The variational derivative of the action
D.3. The equation of motion
E. Newton's second law
E.1. The force
E.2. Variational derivative of lagrangian and force
E.3. Equation of motion if and only if Newton's second law
F. Energy conservation
F.1. Energy conservation in terms of time derivatives
F.2. Energy conservation in terms of constant energy
G. Hamiltonian formulation
G.1. The canonical momentum
G.2. The Hamiltonian
G.2.1. Equality for the Hamiltonian
G.2.2. Smoothness of the Hamiltonian
G.2.3. Gradients of the Hamiltonian
G.3. Relation between Hamiltonian and energy
G.4. Hamilton equation operator
G.5. Equation of motion if and only if Hamilton's equations
H. Equivalences between the different formulations of the equations of motion
iv. References
References for the classical harmonic oscillator include:
Landau & Lifshitz, Mechanics, page 58, section 21.
@[ expose ] public section TODO "Create a new file for the geometric model which properly models the position as a
configuration space and velocity as its tangent space, then show explicitly how this
coordinate model is a simplification of the geometric model.
A nice reference for such an analysis is:
https://web.williams.edu/Mathematics/it3/texts/var_noether.pdf"
We start by defining a structure containing the input data of the harmonic oscillator, and
proving basic properties thereof. The input data consists of the mass m
of the particle and the spring constant k.
The classical harmonic oscillator is specified by a mass m, and a spring constant k.
Both the mass and the string constant are assumed to be positive.
The mass of the harmonic Oscillator.
The spring constant of the harmonic oscillator.
structure HarmonicOscillator where m : ℝ k : ℝ
m_pos : 0 < m
k_pos : 0 < k
@[ simp ]
lemma k_ne_zero : S . k ≠ 0 := S . k_pos . ne' @[ simp ]
lemma m_ne_zero : S . m ≠ 0 := S . m_pos . ne'
B. The angular frequency
From the input data, it is possible to define the angular frequency ω of the harmonic oscillator,
as √(k/m).
The angular frequency appears in the solutions to the equations of motion of the harmonic
oscillator.
Here we both define and prove properties related to the angular frequency.
The angular frequency of the classical harmonic oscillator is positive.
@[ simp ]
lemma ω_pos : 0 < S . ω := sqrt_pos . mpr ( div_pos S . k_pos S . m_pos )
The square of the angular frequency of the classical harmonic oscillator is equal to k/m.
lemma ω_sq : S . ω ^ 2 = S . k / S . m := sq_sqrt ( div_pos S . k_pos S . m_pos ) . le
The angular frequency of the classical harmonic oscillator is not equal to zero.
lemma ω_ne_zero : S . ω ≠ 0 := S . ω_pos . ne'
The inverse of the square of the angular frequency of the classical harmonic oscillator
is m/k.
C. The energies
The harmonic oscillator has a kinetic energy determined by it's velocity and
a potential energy determined by it's position.
These combine to give the total energy of the harmonic oscillator.
Here we state and prove a number of properties of these energies.
C.1. The definitions of the energies
We define the three energies, it is these energies which will control the dynamics
of the harmonic oscillator, through the lagrangian.
C.2. Simple equalities for the energies
C.3. Differentiability of the energies
On smooth trajectories the energies are differentiable.
C.4. Time derivatives of the energies
For a general smooth trajectory (which may not satisfy the equations of motion) we can compute
the time derivatives of the energies.
lemma kineticEnergy_deriv ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) ) ( hx : ContDiff ℝ ∞ xₜ ) :
∂ₜ ( kineticEnergy S xₜ ) = fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ∂ₜ ( S . kineticEnergy xₜ ) = fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ
funext t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ∂ₜ ( S . kineticEnergy xₜ ) t = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ
unfold kineticEnergy S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ∂ₜ (fun t => 1 / 2 * S . m * ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ ) t = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ
have hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t :=
( deriv_differentiable_of_contDiff xₜ hx ) . differentiableAt S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ∂ₜ (fun t => 1 / 2 * S . m * ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ ) t = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ
rw [ Time.deriv_eq , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( fderiv ℝ (fun t => 1 / 2 * S . m * ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ ) t ) 1 = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ fderiv_const_mul ( by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ DifferentiableAt ℝ (fun t => ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ ) t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ fun_prop All goals completed! 🐙 S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ ) , _root_.smul_apply , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( fderiv ℝ (fun t => ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ ) t ) 1 = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ
fderiv_inner_apply ( 𝕜 := ℝ ) hd hd , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ( fderiv ℝ ( ∂ₜ xₜ ) t ) 1 ⟫_ ℝ + ⟪ ( fderiv ℝ ( ∂ₜ xₜ ) t ) 1 , ∂ₜ xₜ t ⟫_ ℝ ) =
⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ ← Time.deriv_eq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ ( 1 / 2 * S . m ) • ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ ( ∂ₜ xₜ ) t , ∂ₜ xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ
simp [ inner_smul_right , real_inner_comm ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ ( ∂ₜ xₜ ) t ⊢ 2 ⁻¹ * S . m * ( ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ ) = S . m * ⟪ ∂ₜ xₜ t , ∂ₜ ( ∂ₜ xₜ ) t ⟫_ ℝ
ring All goals completed! 🐙
lemma potentialEnergy_deriv ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) ) ( hx : ContDiff ℝ ∞ xₜ ) :
∂ₜ ( fun t => potentialEnergy S ( xₜ t ) ) = fun t => ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ( ∂ₜ fun t => S . potentialEnergy ( xₜ t ) ) = fun t => ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ
funext t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ∂ₜ (fun t => S . potentialEnergy ( xₜ t ) ) t = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ
have hd : DifferentiableAt ℝ xₜ t := ( hx . differentiable ( by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ∞ ≠ 0 S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ∂ₜ (fun t => S . potentialEnergy ( xₜ t ) ) t = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ simp All goals completed! 🐙 S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ∂ₜ (fun t => S . potentialEnergy ( xₜ t ) ) t = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ ) ) . differentiableAt S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ∂ₜ (fun t => S . potentialEnergy ( xₜ t ) ) t = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ
simp only [ potentialEnergy_eq , smul_eq_mul , ← mul_assoc ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ∂ₜ (fun t => 1 / 2 * S . k * ⟪ xₜ t , xₜ t ⟫_ ℝ ) t = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ
rw [ Time.deriv_eq , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( fderiv ℝ (fun t => 1 / 2 * S . k * ⟪ xₜ t , xₜ t ⟫_ ℝ ) t ) 1 = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ fderiv_const_mul ( by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ DifferentiableAt ℝ (fun t => ⟪ xₜ t , xₜ t ⟫_ ℝ ) t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ fun_prop All goals completed! 🐙 S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ ) , _root_.smul_apply , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( fderiv ℝ (fun t => ⟪ xₜ t , xₜ t ⟫_ ℝ ) t ) 1 = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ
fderiv_inner_apply ( 𝕜 := ℝ ) hd hd , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ( fderiv ℝ xₜ t ) 1 ⟫_ ℝ + ⟪ ( fderiv ℝ xₜ t ) 1 , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ ← Time.deriv_eq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ ( 1 / 2 * S . k ) • ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ ∂ₜ xₜ t , xₜ t ⟫_ ℝ ) = ⟪ ∂ₜ xₜ t , S . k • xₜ t ⟫_ ℝ
simp [ inner_smul_right , real_inner_comm ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time hd : DifferentiableAt ℝ xₜ t ⊢ 2 ⁻¹ * S . k * ( ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ ) = S . k * ⟪ xₜ t , ∂ₜ xₜ t ⟫_ ℝ
ring All goals completed! 🐙
lemma energy_deriv ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) ) ( hx : ContDiff ℝ ∞ xₜ ) :
∂ₜ ( energy S xₜ ) = fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ∂ₜ ( S . energy xₜ ) = fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ
unfold energy S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ( ∂ₜ fun t => S . kineticEnergy xₜ t + S . potentialEnergy ( xₜ t ) ) = fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ
funext t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ∂ₜ (fun t => S . kineticEnergy xₜ t + S . potentialEnergy ( xₜ t ) ) t = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ
rw [ Time.deriv_eq , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ( fderiv ℝ (fun t => S . kineticEnergy xₜ t + S . potentialEnergy ( xₜ t ) ) t ) 1 = ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ( fderiv ℝ ( S . kineticEnergy xₜ ) t + fderiv ℝ (fun t => S . potentialEnergy ( xₜ t ) ) t ) 1 =
⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ fderiv_fun_add ( by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ DifferentiableAt ℝ ( S . kineticEnergy xₜ ) t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ( fderiv ℝ ( S . kineticEnergy xₜ ) t + fderiv ℝ (fun t => S . potentialEnergy ( xₜ t ) ) t ) 1 =
⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ fun_prop All goals completed! 🐙 S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ( fderiv ℝ ( S . kineticEnergy xₜ ) t + fderiv ℝ (fun t => S . potentialEnergy ( xₜ t ) ) t ) 1 =
⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ ) ( S . potentialEnergy_differentiable xₜ hx t ) ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ t : Time ⊢ ( fderiv ℝ ( S . kineticEnergy xₜ ) t + fderiv ℝ (fun t => S . potentialEnergy ( xₜ t ) ) t ) 1 =
⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ
simp only [ _root_.add_apply , ← Time.deriv_eq , kineticEnergy_deriv _ _ hx ,
potentialEnergy_deriv _ _ hx , ← inner_add_right ] All goals completed! 🐙
D. Lagrangian and the equation of motion
We state the lagrangian, and derive from that the equation of motion for the harmonic oscillator.
D.1. The Lagrangian
We define the lagrangian of the harmonic oscillator, as a function of phase-space. It is given by
$$L(t, x, v) := \frac{1}{2} m ‖v‖^2 - \frac{1}{2} k ‖x‖^2$$
In theory this definition is the kinetic energy minus the potential energy, however
to make the lagrangian a function on phase-space we reserve this result for a lemma.
The lagrangian of the harmonic oscillator is the kinetic energy minus the potential energy.
set_option linter.unusedVariables false in @[ nolint unusedArguments ]
noncomputable def lagrangian ( t : Time ) ( x : EuclideanSpace ℝ ( Fin 1 ) )
( v : EuclideanSpace ℝ ( Fin 1 ) ) : ℝ :=
1 / ( 2 : ℝ ) * S . m * ⟪ v , v ⟫_ ℝ - S . potentialEnergy x
D.1.1. Equalities for the lagrangian
Equalities for the lagrangian. We prove some simple equalities for the lagrangian,
in particular that when applied to a trajectory it is the kinetic energy minus the potential energy.
D.1.2. Smoothness of the lagrangian
The lagrangian is smooth in all its arguments.
@[ fun_prop ]
lemma contDiff_lagrangian ( n : WithTop ℕ∞ ) : ContDiff ℝ n ↿ S . lagrangian := by S : HarmonicOscillator n : ℕ∞ω ⊢ ContDiff ℝ n ↿ S . lagrangian
rw [ lagrangian_eq S : HarmonicOscillator n : ℕ∞ω ⊢ ContDiff ℝ n ↿ fun t x v => 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ - 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ S : HarmonicOscillator n : ℕ∞ω ⊢ ContDiff ℝ n ↿ fun t x v => 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ - 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ] S : HarmonicOscillator n : ℕ∞ω ⊢ ContDiff ℝ n ↿ fun t x v => 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ - 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ
fun_prop All goals completed! 🐙 lemma toDual_symm_innerSL ( x : EuclideanSpace ℝ ( Fin 1 ) ) :
( InnerProductSpace.toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( innerSL ℝ x ) = x :=
( InnerProductSpace.toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm_apply_apply x
lemma gradient_inner_self ( x : EuclideanSpace ℝ ( Fin 1 ) ) :
gradient ( fun y : EuclideanSpace ℝ ( Fin 1 ) => ⟪ y , y ⟫_ ℝ ) x = ( 2 : ℝ ) • x := by x : EuclideanSpace ℝ ( Fin 1 ) ⊢ gradient (fun y => ⟪ y , y ⟫_ ℝ ) x = 2 • x
refine ext_inner_right ( 𝕜 := ℝ ) fun y => ? _ x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ ⟪ gradient (fun y => ⟪ y , y ⟫_ ℝ ) x , y ⟫_ ℝ = ⟪ 2 • x , y ⟫_ ℝ
unfold gradient x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ ⟪ ( toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x ) , y ⟫_ ℝ = ⟪ 2 • x , y ⟫_ ℝ
rw [ InnerProductSpace.toDual_symm_apply , x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ ( fderiv ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x ) y = ⟪ 2 • x , y ⟫_ ℝ x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ ⟪ x , ( fderiv ℝ (fun x => x ) x ) y ⟫_ ℝ + ⟪ ( fderiv ℝ (fun x => x ) x ) y , x ⟫_ ℝ = ⟪ 2 • x , y ⟫_ ℝ
fderiv_inner_apply ( 𝕜 := ℝ ) differentiableAt_fun_id differentiableAt_fun_id x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ ⟪ x , ( fderiv ℝ (fun x => x ) x ) y ⟫_ ℝ + ⟪ ( fderiv ℝ (fun x => x ) x ) y , x ⟫_ ℝ = ⟪ 2 • x , y ⟫_ ℝ x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ ⟪ x , ( fderiv ℝ (fun x => x ) x ) y ⟫_ ℝ + ⟪ ( fderiv ℝ (fun x => x ) x ) y , x ⟫_ ℝ = ⟪ 2 • x , y ⟫_ ℝ ] x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ ⟪ x , ( fderiv ℝ (fun x => x ) x ) y ⟫_ ℝ + ⟪ ( fderiv ℝ (fun x => x ) x ) y , x ⟫_ ℝ = ⟪ 2 • x , y ⟫_ ℝ
simp [ real_inner_comm , inner_smul_right , two_mul ] All goals completed! 🐙
lemma gradient_const_mul_inner_self ( c : ℝ ) ( x : EuclideanSpace ℝ ( Fin 1 ) ) :
gradient ( fun y : EuclideanSpace ℝ ( Fin 1 ) => c * ⟪ y , y ⟫_ ℝ ) x = ( 2 * c ) • x := by c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ gradient (fun y => c * ⟪ y , y ⟫_ ℝ ) x = ( 2 * c ) • x
unfold gradient c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ ( toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv ℝ (fun y => c * ⟪ y , y ⟫_ ℝ ) x ) = ( 2 * c ) • x
rw [ fderiv_const_mul ( by c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ DifferentiableAt ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ c • ( toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x ) = ( 2 * c ) • x fun_prop All goals completed! 🐙 c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ c • ( toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x ) = ( 2 * c ) • x ) c , map_smul c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ c • ( toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x ) = ( 2 * c ) • x c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ c • ( toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x ) = ( 2 * c ) • x ] c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ c • ( toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv ℝ (fun y => ⟪ y , y ⟫_ ℝ ) x ) = ( 2 * c ) • x
show c • gradient ( fun y : EuclideanSpace ℝ ( Fin 1 ) => ⟪ y , y ⟫_ ℝ ) x = ( 2 * c ) • x c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ c • gradient (fun y => ⟪ y , y ⟫_ ℝ ) x = ( 2 * c ) • x
rw [ gradient_inner_self , c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ c • 2 • x = ( 2 * c ) • x All goals completed! 🐙 smul_smul , c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ ( c * 2 ) • x = ( 2 * c ) • x All goals completed! 🐙 mul_comm c : ℝ x : EuclideanSpace ℝ ( Fin 1 ) ⊢ ( 2 * c ) • x = ( 2 * c ) • x All goals completed! 🐙 ] All goals completed! 🐙
D.1.3. Gradients of the lagrangian
We now show results related to the gradients of the lagrangian with respect to the
position and velocity.
private lemma gradient_add_const' { f : EuclideanSpace ℝ ( Fin 1 ) → ℝ } { c : ℝ }
( x : EuclideanSpace ℝ ( Fin 1 ) ) :
gradient ( fun y => f y + c ) x = gradient f x :=
congrArg ( InnerProductSpace.toDual ℝ ( EuclideanSpace ℝ ( Fin 1 ) ) ) . symm ( fderiv_add_const c )
lemma gradient_lagrangian_position_eq ( t : Time ) ( x : EuclideanSpace ℝ ( Fin 1 ) )
( v : EuclideanSpace ℝ ( Fin 1 ) ) :
gradient ( fun x => lagrangian S t x v ) x = - S . k • x := by S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) ⊢ gradient (fun x => S . lagrangian t x v ) x = - S . k • x
have h_eq : ( fun y : EuclideanSpace ℝ ( Fin 1 ) => lagrangian S t y v ) =
fun y => ( - ( 1 / ( 2 : ℝ ) ) * S . k ) * ⟪ y , y ⟫_ ℝ + ( 1 / ( 2 : ℝ ) * S . m * ⟪ v , v ⟫_ ℝ ) := by
funext y S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . lagrangian t y v = - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ gradient (fun x => S . lagrangian t x v ) x = - S . k • x ; simp only [ lagrangian_eq ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ - 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ = - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ gradient (fun x => S . lagrangian t x v ) x = - S . k • x ; ring S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ gradient (fun x => S . lagrangian t x v ) x = - S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ gradient (fun x => S . lagrangian t x v ) x = - S . k • x
rw [ h_eq , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ gradient (fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ) x = - S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ ( 2 * ( - ( 1 / 2 ) * S . k ) ) • x = - S . k • x gradient_add_const' , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ gradient (fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ ) x = - S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ ( 2 * ( - ( 1 / 2 ) * S . k ) ) • x = - S . k • x gradient_const_mul_inner_self S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ ( 2 * ( - ( 1 / 2 ) * S . k ) ) • x = - S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ ( 2 * ( - ( 1 / 2 ) * S . k ) ) • x = - S . k • x ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t y v ) = fun y => - ( 1 / 2 ) * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . m * ⟪ v , v ⟫_ ℝ ⊢ ( 2 * ( - ( 1 / 2 ) * S . k ) ) • x = - S . k • x
module All goals completed! 🐙
lemma gradient_lagrangian_velocity_eq ( t : Time ) ( x : EuclideanSpace ℝ ( Fin 1 ) )
( v : EuclideanSpace ℝ ( Fin 1 ) ) :
gradient ( lagrangian S t x ) v = S . m • v := by S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) ⊢ gradient ( S . lagrangian t x ) v = S . m • v
have h_eq : ( fun y : EuclideanSpace ℝ ( Fin 1 ) => lagrangian S t x y ) =
fun y => ( ( 1 / ( 2 : ℝ ) ) * S . m ) * ⟪ y , y ⟫_ ℝ + ( - ( 1 / ( 2 : ℝ ) ) * S . k * ⟪ x , x ⟫_ ℝ ) := by
funext y S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . lagrangian t x y = 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient ( S . lagrangian t x ) v = S . m • v ; simp only [ lagrangian_eq ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ - 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ = 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient ( S . lagrangian t x ) v = S . m • v ; ring S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient ( S . lagrangian t x ) v = S . m • v S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient ( S . lagrangian t x ) v = S . m • v
change gradient ( fun y : EuclideanSpace ℝ ( Fin 1 ) => lagrangian S t x y ) v = S . m • v S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun y => S . lagrangian t x y ) v = S . m • v
rw [ h_eq , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ) v = S . m • v S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . m ) ) • v = S . m • v gradient_add_const' , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ ) v = S . m • v S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . m ) ) • v = S . m • v gradient_const_mul_inner_self S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . m ) ) • v = S . m • v S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . m ) ) • v = S . m • v ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) v : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . lagrangian t x y ) = fun y => 1 / 2 * S . m * ⟪ y , y ⟫_ ℝ + - ( 1 / 2 ) * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . m ) ) • v = S . m • v
module All goals completed! 🐙
D.2. The variational derivative of the action
We now write down the variational derivative for the harmonic oscillator, for
a trajectory $x(t)$ this is equal to
$$t\mapsto \left.\frac{\partial L(t, \dot x (t), q)}{\partial q}\right|{q = x(t)} -
\frac{d}{dt} \left.\frac{\partial L(t, v, x(t))}{\partial v}\right| {v = \dot x (t)}$$
Setting this equal to zero corresponds to the Euler-Lagrange equations, and thereby the
equation of motion.
D.2.1. Equality for the variational derivative
Basic equalities for the variational derivative of the action.
D.3. The equation of motion
The equation of motion for the harmonic oscillator is given by setting the
variational derivative of the action equal to zero.
The equation of motion for the Harmonic oscillator.
def EquationOfMotion ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) ) : Prop :=
S . gradLagrangian xₜ = 0
D.3.1. Equation of motion if and only if variational-gradient of Lagrangian is zero
We write a simple iff statement for the definition of the equation of motions.
E. Newton's second law
We define the force of the harmonic oscillator, and show that the equation of
motion is equivalent to Newton's second law.
E.1. The force
We define the force of the harmonic oscillator as the negative gradient of the potential energy,
and show that this is equal to - k x.
E.1.1. The force is equal to - k x
We now show that the force is equal to - k x.
The force on the classical harmonic oscillator is - k x.
lemma force_eq_linear ( x : EuclideanSpace ℝ ( Fin 1 ) ) : force S x = - S . k • x := by S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . force x = - S . k • x
have hpot : potentialEnergy S = fun y : EuclideanSpace ℝ ( Fin 1 ) =>
( ( 1 / ( 2 : ℝ ) ) * S . k ) * ⟪ y , y ⟫_ ℝ := by
funext y S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . potentialEnergy y = 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ S . force x = - S . k • x
simp [ potentialEnergy , mul_assoc ] S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ S . force x = - S . k • x S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ S . force x = - S . k • x
unfold force S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ - gradient S . potentialEnergy x = - S . k • x
rw [ hpot , S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ - gradient (fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ) x = - S . k • x S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ - ( ( 2 * ( 1 / 2 * S . k ) ) • x ) = - S . k • x gradient_const_mul_inner_self S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ - ( ( 2 * ( 1 / 2 * S . k ) ) • x ) = - S . k • x S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ - ( ( 2 * ( 1 / 2 * S . k ) ) • x ) = - S . k • x ] S : HarmonicOscillator x : EuclideanSpace ℝ ( Fin 1 ) hpot : S . potentialEnergy = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ⊢ - ( ( 2 * ( 1 / 2 * S . k ) ) • x ) = - S . k • x
module All goals completed! 🐙
E.2. Variational derivative of lagrangian and force
We relate the variational derivative of lagrangian to the force, and show the relation
to Newton's second law.
The Euler lagrange operator corresponds to Newton's second law.
E.3. Equation of motion if and only if Newton's second law
We show that the equation of motion is equivalent to Newton's second law.
lemma equationOfMotion_iff_newtons_2nd_law ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) )
( hx : ContDiff ℝ ∞ xₜ ) :
S . EquationOfMotion xₜ ↔
( ∀ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t = force S ( xₜ t ) ) := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t )
rw [ EquationOfMotion , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . gradLagrangian xₜ = 0 ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( x : Time ), S . force ( xₜ x ) - S . m • ∂ₜ ( ∂ₜ xₜ ) x = 0 x ) ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) gradLagrangian_eq_force S xₜ hx , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (fun t => S . force ( xₜ t ) - S . m • ∂ₜ ( ∂ₜ xₜ ) t ) = 0 ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( x : Time ), S . force ( xₜ x ) - S . m • ∂ₜ ( ∂ₜ xₜ ) x = 0 x ) ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) funext_iff S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( x : Time ), S . force ( xₜ x ) - S . m • ∂ₜ ( ∂ₜ xₜ ) x = 0 x ) ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( x : Time ), S . force ( xₜ x ) - S . m • ∂ₜ ( ∂ₜ xₜ ) x = 0 x ) ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( x : Time ), S . force ( xₜ x ) - S . m • ∂ₜ ( ∂ₜ xₜ ) x = 0 x ) ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t )
simp only [ Pi.zero_apply , sub_eq_zero ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( x : Time ), S . force ( xₜ x ) = S . m • ∂ₜ ( ∂ₜ xₜ ) x ) ↔ ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t )
exact forall_congr' fun t => eq_comm All goals completed! 🐙
F. Energy conservation
In this section we show that any trajectory satisfying the equation of motion
conserves energy. This result simply follows from the definition of the energies,
and their derivatives, as well as the statement that the equations of motion are equivalent
to Newton's second law.
F.1. Energy conservation in terms of time derivatives
We prove that the time derivative of the energy is zero for any trajectory satisfying
the equation of motion.
lemma energy_conservation_of_equationOfMotion ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) )
( hx : ContDiff ℝ ∞ xₜ )
( h : S . EquationOfMotion xₜ ) : ∂ₜ ( S . energy xₜ ) = 0 := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : S . EquationOfMotion xₜ ⊢ ∂ₜ ( S . energy xₜ ) = 0
rw [ equationOfMotion_iff_newtons_2nd_law _ _ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ⊢ ∂ₜ ( S . energy xₜ ) = 0 S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ⊢ ∂ₜ ( S . energy xₜ ) = 0 ] at h S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ⊢ ∂ₜ ( S . energy xₜ ) = 0
funext t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) t : Time ⊢ ∂ₜ ( S . energy xₜ ) t = 0 t
rw [ energy_deriv _ _ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) t : Time ⊢ (fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ ) t = 0 t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) t : Time ⊢ (fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ ) t = 0 t ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ h : ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) t : Time ⊢ (fun t => ⟪ ∂ₜ xₜ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t + S . k • xₜ t ⟫_ ℝ ) t = 0 t
simp [ h , force_eq_linear ] All goals completed! 🐙
F.2. Energy conservation in terms of constant energy
We prove that the energy is constant for any trajectory satisfying the equation of motion.
We now turn to the Hamiltonian formulation of the harmonic oscillator.
We define the canonical momentum, the Hamiltonian, and show that the equations of
motion are equivalent to Hamilton's equations.
G.1. The canonical momentum
We define the canonical momentum as the gradient of the lagrangian with respect to
the velocity.
G.1.1. Equality for the canonical momentum
An simple equality for the canonical momentum.
G.2. The Hamiltonian
The hamiltonian is defined as a function of time, canonical momentum and position, as
H = ⟪p, v⟫ - L(t, x, v)
where v is a function of p and x through the canonical momentum.
G.2.1. Equality for the Hamiltonian
We prove a simple equality for the Hamiltonian, to help in computations.
lemma hamiltonian_eq :
hamiltonian S = fun _ p x => ( 1 / ( 2 : ℝ ) ) * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ +
( 1 / ( 2 : ℝ ) ) * S . k * ⟪ x , x ⟫_ ℝ := by S : HarmonicOscillator ⊢ S . hamiltonian = fun x p x_1 => 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ + 1 / 2 * S . k * ⟪ x_1 , x_1 ⟫_ ℝ
funext t x p S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . hamiltonian t x p = 1 / 2 * ( 1 / S . m ) * ⟪ x , x ⟫_ ℝ + 1 / 2 * S . k * ⟪ p , p ⟫_ ℝ
simp only [ hamiltonian , toCanonicalMomentum , lagrangian_eq , one_div , LinearEquiv.coe_symm_mk' ,
inner_smul_right , inner_smul_left , map_inv₀ , ringHom_apply ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . m ⁻¹ * ⟪ x , x ⟫_ ℝ - ( 2 ⁻¹ * S . m * ( S . m ⁻¹ * ( S . m ⁻¹ * ⟪ x , x ⟫_ ℝ ) ) - 2 ⁻¹ * S . k * ⟪ p , p ⟫_ ℝ ) =
2 ⁻¹ * S . m ⁻¹ * ⟪ x , x ⟫_ ℝ + 2 ⁻¹ * S . k * ⟪ p , p ⟫_ ℝ
field_simp S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) ⊢ ⟪ x , x ⟫_ ℝ * 2 - ( ⟪ x , x ⟫_ ℝ - S . m * S . k * ⟪ p , p ⟫_ ℝ ) = ⟪ x , x ⟫_ ℝ + S . m * S . k * ⟪ p , p ⟫_ ℝ
ring All goals completed! 🐙
G.2.2. Smoothness of the Hamiltonian
We show that the Hamiltonian is smooth in all its arguments.
G.2.3. Gradients of the Hamiltonian
We now write down the gradients of the Hamiltonian with respect to the momentum and position.
lemma gradient_hamiltonian_position_eq ( t : Time ) ( x : EuclideanSpace ℝ ( Fin 1 ) )
( p : EuclideanSpace ℝ ( Fin 1 ) ) :
gradient ( hamiltonian S t p ) x = S . k • x := by S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) ⊢ gradient ( S . hamiltonian t p ) x = S . k • x
have h_eq : ( fun y : EuclideanSpace ℝ ( Fin 1 ) => hamiltonian S t p y ) =
fun y => ( ( 1 / ( 2 : ℝ ) ) * S . k ) * ⟪ y , y ⟫_ ℝ +
( ( 1 / ( 2 : ℝ ) ) * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ) := by
funext y S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . hamiltonian t p y = 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ gradient ( S . hamiltonian t p ) x = S . k • x
simp only [ hamiltonian_eq ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ + 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ = 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ gradient ( S . hamiltonian t p ) x = S . k • x
ring S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ gradient ( S . hamiltonian t p ) x = S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ gradient ( S . hamiltonian t p ) x = S . k • x
change gradient ( fun y : EuclideanSpace ℝ ( Fin 1 ) => hamiltonian S t p y ) x = S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ gradient (fun y => S . hamiltonian t p y ) x = S . k • x
rw [ h_eq , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ gradient (fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ) x = S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . k ) ) • x = S . k • x gradient_add_const' , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ gradient (fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ ) x = S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . k ) ) • x = S . k • x gradient_const_mul_inner_self S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . k ) ) • x = S . k • x S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . k ) ) • x = S . k • x ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t p y ) = fun y => 1 / 2 * S . k * ⟪ y , y ⟫_ ℝ + 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * S . k ) ) • x = S . k • x
module All goals completed! 🐙
lemma gradient_hamiltonian_momentum_eq ( t : Time ) ( x : EuclideanSpace ℝ ( Fin 1 ) )
( p : EuclideanSpace ℝ ( Fin 1 ) ) :
gradient ( hamiltonian S t · x ) p = ( 1 / S . m ) • p := by S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) ⊢ gradient (fun x_1 => S . hamiltonian t x_1 x ) p = ( 1 / S . m ) • p
have h_eq : ( fun y : EuclideanSpace ℝ ( Fin 1 ) => hamiltonian S t y x ) =
fun y => ( ( 1 / ( 2 : ℝ ) ) * ( 1 / S . m ) ) * ⟪ y , y ⟫_ ℝ +
( ( 1 / ( 2 : ℝ ) ) * S . k * ⟪ x , x ⟫_ ℝ ) := by
funext y S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) y : EuclideanSpace ℝ ( Fin 1 ) ⊢ S . hamiltonian t y x = 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun x_1 => S . hamiltonian t x_1 x ) p = ( 1 / S . m ) • p
simp only [ hamiltonian_eq ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun x_1 => S . hamiltonian t x_1 x ) p = ( 1 / S . m ) • p S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun x_1 => S . hamiltonian t x_1 x ) p = ( 1 / S . m ) • p
change gradient ( fun y : EuclideanSpace ℝ ( Fin 1 ) => hamiltonian S t y x ) p = ( 1 / S . m ) • p S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun x_1 => S . hamiltonian t x_1 x ) p = ( 1 / S . m ) • p
rw [ h_eq , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ) p = ( 1 / S . m ) • p S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * ( 1 / S . m ) ) ) • p = ( 1 / S . m ) • p gradient_add_const' , S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ gradient (fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ ) p = ( 1 / S . m ) • p S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * ( 1 / S . m ) ) ) • p = ( 1 / S . m ) • p gradient_const_mul_inner_self S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * ( 1 / S . m ) ) ) • p = ( 1 / S . m ) • p S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * ( 1 / S . m ) ) ) • p = ( 1 / S . m ) • p ] S : HarmonicOscillator t : Time x : EuclideanSpace ℝ ( Fin 1 ) p : EuclideanSpace ℝ ( Fin 1 ) h_eq : (fun y => S . hamiltonian t y x ) = fun y => 1 / 2 * ( 1 / S . m ) * ⟪ y , y ⟫_ ℝ + 1 / 2 * S . k * ⟪ x , x ⟫_ ℝ ⊢ ( 2 * ( 1 / 2 * ( 1 / S . m ) ) ) • p = ( 1 / S . m ) • p
module All goals completed! 🐙
G.3. Relation between Hamiltonian and energy
We show that the Hamiltonian, when evaluated on any trajectory, is equal to the energy.
This is independent of whether the trajectory satisfies the equations of motion or not.
lemma hamiltonian_eq_energy ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) ) :
( fun t => hamiltonian S t ( toCanonicalMomentum S t ( xₜ t ) ( ∂ₜ xₜ t ) ) ( xₜ t ) ) = energy S xₜ := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) ⊢ (fun t => S . hamiltonian t ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ( xₜ t ) ) = S . energy xₜ
funext t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) t : Time ⊢ S . hamiltonian t ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ( xₜ t ) = S . energy xₜ t
rw [ hamiltonian_eq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) t : Time ⊢ (fun x p x_1 => 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ + 1 / 2 * S . k * ⟪ x_1 , x_1 ⟫_ ℝ ) t
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ( xₜ t ) =
S . energy xₜ t S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) t : Time ⊢ (fun x p x_1 => 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ + 1 / 2 * S . k * ⟪ x_1 , x_1 ⟫_ ℝ ) t
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ( xₜ t ) =
S . energy xₜ t ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) t : Time ⊢ (fun x p x_1 => 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ + 1 / 2 * S . k * ⟪ x_1 , x_1 ⟫_ ℝ ) t
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ( xₜ t ) =
S . energy xₜ t
unfold energy kineticEnergy potentialEnergy S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) t : Time ⊢ (fun x p x_1 => 1 / 2 * ( 1 / S . m ) * ⟪ p , p ⟫_ ℝ + 1 / 2 * S . k * ⟪ x_1 , x_1 ⟫_ ℝ ) t
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ( xₜ t ) =
1 / 2 * S . m * ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + ( 1 / 2 ) • S . k • ⟪ xₜ t , xₜ t ⟫_ ℝ
simp only [ toCanonicalMomentum_eq , inner_smul_left , inner_smul_right , smul_eq_mul , ringHom_apply ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) t : Time ⊢ 1 / 2 * ( 1 / S . m ) * ( S . m * ( S . m * ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ ) ) + 1 / 2 * S . k * ⟪ xₜ t , xₜ t ⟫_ ℝ =
1 / 2 * S . m * ⟪ ∂ₜ xₜ t , ∂ₜ xₜ t ⟫_ ℝ + 1 / 2 * ( S . k * ⟪ xₜ t , xₜ t ⟫_ ℝ )
field_simp All goals completed! 🐙
G.4. Hamilton equation operator
We define the operator on momentum-position phase-space whose vanishing is equivalent
to Hamilton's equations.
G.5. Equation of motion if and only if Hamilton's equations
We show that the equation of motion is equivalent to Hamilton's equations, that is
to the vanishing of the Hamilton equation operator.
lemma equationOfMotion_iff_hamiltonEqOp_eq_zero ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) )
( hx : ContDiff ℝ ∞ xₜ ) : S . EquationOfMotion xₜ ↔
hamiltonEqOp S ( fun t => S . toCanonicalMomentum t ( xₜ t ) ( ∂ₜ xₜ t ) ) xₜ = 0 := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔ S . hamiltonEqOp (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) xₜ = 0
rw [ hamiltonEqOp , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) xₜ = 0 S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔
(∀ ( t : Time ), ∂ₜ xₜ t = gradient (fun x => S . hamiltonian t x ( xₜ t ) ) ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ) ∧
∀ ( t : Time ),
∂ₜ (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) t =
- gradient (fun x => S . hamiltonian t ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) x ) ( xₜ t ) hamiltonEqOp_eq_zero_iff_hamiltons_equations S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔
(∀ ( t : Time ), ∂ₜ xₜ t = gradient (fun x => S . hamiltonian t x ( xₜ t ) ) ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ) ∧
∀ ( t : Time ),
∂ₜ (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) t =
- gradient (fun x => S . hamiltonian t ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) x ) ( xₜ t ) S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔
(∀ ( t : Time ), ∂ₜ xₜ t = gradient (fun x => S . hamiltonian t x ( xₜ t ) ) ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ) ∧
∀ ( t : Time ),
∂ₜ (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) t =
- gradient (fun x => S . hamiltonian t ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) x ) ( xₜ t ) ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔
(∀ ( t : Time ), ∂ₜ xₜ t = gradient (fun x => S . hamiltonian t x ( xₜ t ) ) ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) ) ∧
∀ ( t : Time ),
∂ₜ (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) t =
- gradient (fun x => S . hamiltonian t ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) x ) ( xₜ t )
simp [ toCanonicalMomentum_eq , gradient_hamiltonian_momentum_eq , gradient_hamiltonian_position_eq ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ S . EquationOfMotion xₜ ↔ ∀ ( t : Time ), ∂ₜ (fun t => S . m • ∂ₜ xₜ t ) t = - ( S . k • xₜ t )
rw [ equationOfMotion_iff_newtons_2nd_law _ _ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ) ↔ ∀ ( t : Time ), ∂ₜ (fun t => S . m • ∂ₜ xₜ t ) t = - ( S . k • xₜ t ) S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ) ↔ ∀ ( t : Time ), ∂ₜ (fun t => S . m • ∂ₜ xₜ t ) t = - ( S . k • xₜ t ) ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ (∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ) ↔ ∀ ( t : Time ), ∂ₜ (fun t => S . m • ∂ₜ xₜ t ) t = - ( S . k • xₜ t )
simp [ Time.deriv_smul _ S . m ( deriv_differentiable_of_contDiff xₜ hx ) , force_eq_linear ] All goals completed! 🐙
We show that the following are equivalent statements for a smooth trajectory xₜ:
The equation of motion holds. (aka the Euler-Lagrange equations hold.)
Newton's second law holds.
Hamilton's equations hold.
The variational principle for the action holds.
The Hamilton variational principle holds.
lemma equationOfMotion_tfae ( xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) ) ( hx : ContDiff ℝ ∞ xₜ ) :
List.TFAE [ S . EquationOfMotion xₜ ,
( ∀ t , S . m • ∂ₜ ( ∂ₜ xₜ ) t = force S ( xₜ t ) ) ,
hamiltonEqOp S ( fun t => S . toCanonicalMomentum t ( xₜ t ) ( ∂ₜ xₜ t ) ) xₜ = 0 ,
( δ ( q' := xₜ ) , ∫ t , lagrangian S t ( q' t ) ( fderiv ℝ q' t 1 ) ) = 0 ,
( δ ( pq' := fun t => ( S . toCanonicalMomentum t ( xₜ t ) ( ∂ₜ xₜ t ) , xₜ t ) ) ,
∫ t , ⟪ ( pq' t ) . 1 , ∂ₜ ( Prod.snd ∘ pq' ) t ⟫_ ℝ - S . hamiltonian t ( pq' t ) . 1 ( pq' t ) . 2 ) = 0 ] := by S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) ,
S . hamiltonEqOp (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) ) xₜ = 0 ,
varGradient (fun q' t => S . lagrangian t ( q' t ) ( ( fderiv ℝ q' t ) 1 ) ) xₜ = 0 ,
( varGradient (fun pq' t => ⟪ ( pq' t ) .1 , ∂ₜ ( Prod.snd ∘ pq' ) t ⟫_ ℝ - S . hamiltonian t ( pq' t ) .1 ( pq' t ) .2 ) fun t =>
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) ) =
0 ] . TFAE
rw [ ← equationOfMotion_iff_hamiltonEqOp_eq_zero , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , ∀ ( t : Time ), S . m • ∂ₜ ( ∂ₜ xₜ ) t = S . force ( xₜ t ) , S . EquationOfMotion xₜ ,
varGradient (fun q' t => S . lagrangian t ( q' t ) ( ( fderiv ℝ q' t ) 1 ) ) xₜ = 0 ,
( varGradient (fun pq' t => ⟪ ( pq' t ) .1 , ∂ₜ ( Prod.snd ∘ pq' ) t ⟫_ ℝ - S . hamiltonian t ( pq' t ) .1 ( pq' t ) .2 ) fun t =>
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) ) =
0 ] . TFAE hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
varGradient (fun q' t => S . lagrangian t ( q' t ) ( ( fderiv ℝ q' t ) 1 ) ) xₜ = 0 ,
( varGradient (fun pq' t => ⟪ ( pq' t ) .1 , ∂ₜ ( Prod.snd ∘ pq' ) t ⟫_ ℝ - S . hamiltonian t ( pq' t ) .1 ( pq' t ) .2 ) fun t =>
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) ) =
0 ] . TFAE hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ ← equationOfMotion_iff_newtons_2nd_law S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
varGradient (fun q' t => S . lagrangian t ( q' t ) ( ( fderiv ℝ q' t ) 1 ) ) xₜ = 0 ,
( varGradient (fun pq' t => ⟪ ( pq' t ) .1 , ∂ₜ ( Prod.snd ∘ pq' ) t ⟫_ ℝ - S . hamiltonian t ( pq' t ) .1 ( pq' t ) .2 ) fun t =>
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) ) =
0 ] . TFAE hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
varGradient (fun q' t => S . lagrangian t ( q' t ) ( ( fderiv ℝ q' t ) 1 ) ) xₜ = 0 ,
( varGradient (fun pq' t => ⟪ ( pq' t ) .1 , ∂ₜ ( Prod.snd ∘ pq' ) t ⟫_ ℝ - S . hamiltonian t ( pq' t ) .1 ( pq' t ) .2 ) fun t =>
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) ) =
0 ] . TFAE hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
varGradient (fun q' t => S . lagrangian t ( q' t ) ( ( fderiv ℝ q' t ) 1 ) ) xₜ = 0 ,
( varGradient (fun pq' t => ⟪ ( pq' t ) .1 , ∂ₜ ( Prod.snd ∘ pq' ) t ⟫_ ℝ - S . hamiltonian t ( pq' t ) .1 ( pq' t ) .2 ) fun t =>
( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) ) =
0 ] . TFAE hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
rw [ hamiltons_equations_varGradient , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
varGradient (fun q' t => S . lagrangian t ( q' t ) ( ( fderiv ℝ q' t ) 1 ) ) xₜ = 0 ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .1 )
(fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .2 ) t ) =
0 ] . TFAE hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , eulerLagrangeOp S . lagrangian xₜ = 0 ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .1 )
(fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .2 ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ euler_lagrange_varGradient S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , eulerLagrangeOp S . lagrangian xₜ = 0 ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .1 )
(fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .2 ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , eulerLagrangeOp S . lagrangian xₜ = 0 ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .1 )
(fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .2 ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , S . EquationOfMotion xₜ , eulerLagrangeOp S . lagrangian xₜ = 0 ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .1 )
(fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) .2 ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
simp only [ List.tfae_cons_self ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , eulerLagrangeOp S . lagrangian xₜ = 0 ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) )
(fun t => xₜ t ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
rw [ ← gradLagrangian_eq_eulerLagrangeOp , S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . gradLagrangian xₜ = 0 ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) )
(fun t => xₜ t ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) )
(fun t => xₜ t ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ ← equationOfMotion_iff_gradLagrangian_zero S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) )
(fun t => xₜ t ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) )
(fun t => xₜ t ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) )
(fun t => xₜ t ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
simp only [ List.tfae_cons_self ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ ,
(fun t =>
ClassicalMechanics.hamiltonEqOp S . hamiltonian (fun t => ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) )
(fun t => xₜ t ) t ) =
0 ] . TFAE hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
erw [ ← equationOfMotion_iff_hamiltonEqOp_eq_zero S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ] . TFAE hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ ] S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ [ S . EquationOfMotion xₜ , S . EquationOfMotion xₜ ] . TFAE hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
simp only [ List.tfae_cons_self , List.tfae_singleton ] hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hq S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . lagrangian hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
repeat fun_prop hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( ( S . toCanonicalMomentum t ( xₜ t ) ) ( ∂ₜ xₜ t ) , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
simp [ toCanonicalMomentum_eq ] hp S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ fun t => ( S . m • ∂ₜ xₜ t , xₜ t ) hL S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ ↿ S . hamiltonian hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ hx S : HarmonicOscillator xₜ : Time → EuclideanSpace ℝ ( Fin 1 ) hx : ContDiff ℝ ∞ xₜ ⊢ ContDiff ℝ ∞ xₜ
repeat fun_prop All goals completed! 🐙