Physlib

Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Solution

Existence and uniqueness of the solutions of the simple pendulum

i. Overview

The equation of motion of the simple pendulum, `θ̈ + ω² sin θ = 0`, is nonlinear, and unlike the harmonic oscillator it has no solution in closed elementary form. Whatever is to be proved about "the" motion of the pendulum released with a given angle and angular velocity must therefore rest on the general theory of ordinary differential equations rather than on an explicit formula. This module supplies that foundation: two smooth solutions of the equation of motion with the same initial angle and the same initial angular velocity coincide for all time, and for any initial angle and angular velocity there is a curve with that initial data satisfying the equation of motion on some interval of time about the initial instant.

The argument is the one used for the damped harmonic oscillator. The second-order equation is rewritten as the first-order system `(θ, θ̇)' = (θ̇, -ω² sin θ)` on the phase space, whose right-hand side, the phase-space vector field of the pendulum, is globally Lipschitz because `sin` is. The global uniqueness theorem for Lipschitz first-order systems, Mathlib's `ODE_solution_unique_univ`, then gives the uniqueness. The uniqueness is global in time and does not depend on the size of the motion: it holds for librations and rotations alike. Existence comes from the Picard–Lindelöf theorem applied to the same first-order system, the phase-space vector field being smooth; the theorem is local, and so is the statement proved here.

The equation of motion contains no first derivative of the angle: there is no damping. Reversing the direction of time therefore carries solutions to solutions, and combined with uniqueness this shows that a pendulum released from rest retraces its path, the angle being an even function of the time since release.

ii. Key results

- `SimplePendulum.phaseVectorField` is the phase-space vector field `(θ, θ̇) ↦ (θ̇, -ω² sin θ)`, and `SimplePendulum.phaseVectorField_lipschitz` proves that it is globally Lipschitz, with constant `1 + ω²`. - `SimplePendulum.acceleration_eq_of_equationOfMotion` solves the equation of motion for the angular acceleration, and `SimplePendulum.phaseCurve_hasDerivAt` shows that the phase curve `(θ, θ̇)` of a smooth solution is an integral curve of the phase-space vector field. - `SimplePendulum.equationOfMotion_unique` proves that two smooth solutions of the equation of motion with the same initial angle and angular velocity are equal, and `SimplePendulum.IsSolution.eq_of_initial` is the same statement for solutions. - `SimplePendulum.isSolution_comp_neg` proves that the time reversal `t ↦ θ (-t)` of a solution is a solution, and `SimplePendulum.releasedFromRest_even` that a solution released from rest is an even function of time. - `SimplePendulum.exists_local_solution` proves, from the Picard–Lindelöf theorem, that for any initial angle and angular velocity there is a curve with that initial data, differentiable together with its velocity and satisfying the equation of motion at all times within some `ε > 0` of the initial instant.

iii. Table of contents

- A. The phase-space vector field - A.1. The definition of the vector field - A.2. The Lipschitz bound - B. The phase curve of a solution - B.1. The angular acceleration along a solution - B.2. The phase curve as an integral curve - C. Uniqueness of the solutions - D. Time-reversal symmetry - D.1. Time reversal of solutions - D.2. Motions released from rest - E. Local existence - E.1. Smoothness of the phase-space vector field - E.2. Local existence of solutions

iv. References

References for the motion of the pendulum, its phase plane, and the existence and uniqueness theorem for ordinary differential equations include: - Landau & Lifshitz, Mechanics, 3rd ed., §11, for motion in one dimension. - Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4, for the phase plane of the pendulum. - Arnold, Ordinary Differential Equations, Chapter 4 (Proofs of the main theorems), for the existence and uniqueness theorem by Picard iteration.

The reduction to a first-order system on the phase space follows `DampedHarmonicOscillator.equationOfMotion_unique`.

A. The phase-space vector field

The equation of motion `θ̈ + ω² sin θ = 0` is of second order. Taking the angular velocity as a second unknown turns it into the first-order system `(θ, θ̇)' = (θ̇, -ω² sin θ)` on the phase space, the product of two copies of the one-dimensional Euclidean space carrying the angle and its rate of change. The right-hand side of this system is the phase-space vector field of the pendulum. Its first component is the projection onto the angular velocity, and its second is `-ω²` times the sine of the angle; as the derivative of `sin` is bounded by one, the field is globally Lipschitz on the phase space. This is the hypothesis under which the general uniqueness theorem for first-order systems applies with no restriction on the time interval or on the size of the motion.

A.1. The definition of the vector field

A.2. The Lipschitz bound

B. The phase curve of a solution

A smooth lift `θ` of the angle satisfying the equation of motion determines the phase curve `t ↦ (θ t, θ̇ t)` in the phase space. Solving the equation of motion for the angular acceleration shows that this curve is an integral curve of the phase-space vector field: its velocity at every instant is the value of the field at its position. The curve is parametrised here by a real variable through the canonical equivalence `Time.toRealCLE.symm : ℝ ≃L[ℝ] Time`, as the uniqueness theorem of Mathlib is stated for curves on `ℝ`.

B.1. The angular acceleration along a solution

B.2. The phase curve as an integral curve

C. Uniqueness of the solutions

The phase curves of two smooth solutions with the same initial angle and angular velocity are two integral curves of the same globally Lipschitz vector field through the same point at time zero. By the global uniqueness theorem `ODE_solution_unique_univ` they coincide, and reading off the first component the two solutions are equal. The energy is conserved along a solution, but it is not used here: the nonlinear equation of motion is handled exactly as the linear damped one, by the first-order reduction alone.

D. Time-reversal symmetry

The equation of motion `I θ̈ = τ(θ)` is of second order and contains no first derivative of the angle: there is no damping. Under the reversal of time `t ↦ -t` the angular velocity changes sign and the angular acceleration does not, so the reversed curve `t ↦ θ (-t)` of a solution is again a solution. Together with the uniqueness of section C this has a physical consequence: a pendulum released from rest at the instant `0` retraces its path, the angle at time `-t` being the angle at time `t`. The bookkeeping of the derivatives under the reflection of `Time` is done by the chain rule `Time.deriv_comp_neg` and its second-order form `Time.deriv_deriv_comp_neg`.

D.1. Time reversal of solutions

D.2. Motions released from rest

E. Local existence

The uniqueness of section C says that a solution with given initial angle and angular velocity is unique if it exists. Existence comes from the Picard–Lindelöf theorem, in the form Mathlib states it for a time-independent `C¹` vector field: the field admits an integral curve through any point, defined on an open interval about the initial instant. Applied to the phase-space vector field of the pendulum, which is smooth, this gives a curve `(θ, θ̇)` in the phase space through the initial data, and its first component is the required angle. Mathlib's curve is parametrised by `ℝ`, so it is pulled back to `Time` through `Time.toRealCLE`; its derivative is read off through `Time.deriv_comp_toRealCLE_of_hasDerivAt`, the converse of the bridge lemma `Time.hasDerivAt_comp_toRealCLE_symm`.

The statement is local: at the times within `ε` of the initial instant, for some `ε > 0`, the angle and its velocity are differentiable and the equation of motion holds, and nothing is claimed about the curve outside that interval. The differentiability is part of the conclusion so that the equation of motion there is a statement about genuine derivatives, and not about the value `0` that `∂ₜ` assigns to a curve where it is not differentiable. Global existence, which the global Lipschitz bound of section A makes true, is not proved here.

E.1. Smoothness of the phase-space vector field

E.2. Local existence of solutions

10 declarations

definition

Phase-space vector field (θ,θ˙)↦(θ˙,−ω2sin⁡θ)(\theta, \dot{\theta}) \mapsto (\dot{\theta}, -\omega^2 \sin \theta) of the simple pendulum

The phase-space vector field for a simple pendulum maps a point p=(θ,θ˙)p = (\theta, \dot{\theta}) in the phase space R×R\mathbb{R} \times \mathbb{R} to the vector (θ˙,−ω2sin⁡θ)(\dot{\theta}, -\omega^2 \sin \theta). Here, θ\theta represents the angular displacement, θ˙\dot{\theta} represents the angular velocity, and ω\omega is the angular frequency of the pendulum. This vector field defines the right-hand side of the first-order system of ordinary differential equations: {dθdt=θ˙dθ˙dt=−ω2sin⁡θ\begin{cases} \frac{d\theta}{dt} = \dot{\theta} \\ \frac{d\dot{\theta}}{dt} = -\omega^2 \sin \theta \end{cases} which is equivalent to the second-order nonlinear equation of motion θ¨+ω2sin⁡θ=0\ddot{\theta} + \omega^2 \sin \theta = 0.

theorem

The phase-space vector field of the simple pendulum is Lipschitz with constant 1+ω21 + \omega^2

The phase-space vector field V:R×R→R×RV: \mathbb{R} \times \mathbb{R} \to \mathbb{R} \times \mathbb{R} of the simple pendulum, which maps the state (θ,θ˙)(\theta, \dot{\theta}) to (θ˙,−ω2sin⁡θ)(\dot{\theta}, -\omega^2 \sin \theta), is Lipschitz continuous with Lipschitz constant 1+ω21 + \omega^2. Here, θ\theta denotes the angular displacement, θ˙\dot{\theta} denotes the angular velocity, and ω\omega is the angular frequency of the pendulum.

theorem

Angular acceleration of a simple pendulum solution satisfies θ¨=−ω2sin⁡θ\ddot{\theta} = -\omega^2 \sin \theta

Let θ:Time→R1\theta : \text{Time} \to \mathbb{R}^1 be a function that satisfies the equation of motion of a simple pendulum. For any t∈Timet \in \text{Time}, the second time derivative of the angle θ\theta, denoted as θ¨(t)\ddot{\theta}(t), is given by θ¨(t)=−(ω2sin⁡θ(t)0)e0 \ddot{\theta}(t) = -(\omega^2 \sin \theta(t)_0) \mathbf{e}_0 where θ(t)0\theta(t)_0 is the scalar value of the angle at time tt, ω\omega is the angular frequency of the pendulum, and e0\mathbf{e}_0 is the unit basis vector of the one-dimensional Euclidean space.

theorem

Relationship between Moment of Inertia, Angular Frequency, and Torque: I(−ω2sin⁡θ)=τ(θ)I(-\omega^2 \sin \theta) = \tau(\theta)

For a simple pendulum with moment of inertia II and angular frequency ω\omega, let xx be an angular position in a one-dimensional Euclidean space (where x0x_0 denotes the angle θ\theta). The product of the moment of inertia and the vector −(ω2sin⁡θ)e0-( \omega^2 \sin \theta ) \mathbf{e}_0 is equal to the torque τ(x)\tau(x) at that position, where e0\mathbf{e}_0 is the standard basis vector for the one-dimensional space. That is, I⋅(−ω2sin⁡(x0)e0)=τ(x). I \cdot \left( -\omega^2 \sin(x_0) \mathbf{e}_0 \right) = \tau(x). This identity expresses the rotational analogue of Newton's second law (Iα=τI \alpha = \tau) by relating the torque to the angular acceleration term −ω2sin⁡θ-\omega^2 \sin \theta derived from the pendulum's equation of motion.

theorem

The Phase Curve of a Simple Pendulum Solution is an Integral Curve of the Phase Vector Field

Let θ:Time→R1\theta: \text{Time} \to \mathbb{R}^1 be an infinitely differentiable (C∞C^\infty) function satisfying the equation of motion for a simple pendulum SS. For any real number τ\tau, let tt be the corresponding point in Time\text{Time} (under the continuous linear equivalence between R\mathbb{R} and Time\text{Time}). Then the phase-space curve f(τ)=(θ(t),θ˙(t))f(\tau) = (\theta(t), \dot{\theta}(t)), where θ˙=∂tθ\dot{\theta} = \partial_t \theta is the angular velocity, has a derivative at τ\tau given by the value of the phase-space vector field at that point: ddτ(θ(t),θ˙(t))=(θ˙(t),−ω2sin⁡θ(t)0) \frac{d}{d\tau} (\theta(t), \dot{\theta}(t)) = (\dot{\theta}(t), -\omega^2 \sin \theta(t)_0) where ω\omega is the angular frequency and θ(t)0\theta(t)_0 is the angular displacement.

theorem

Uniqueness of Smooth Solutions for the Simple Pendulum Equation

Consider a simple pendulum SS. Let x,y:Time→R1x, y : \text{Time} \to \mathbb{R}^1 be two smooth (C∞C^\infty) functions representing the angular position over time. If both xx and yy satisfy the equation of motion for the simple pendulum, and they have the same initial angular position x(0)=y(0)x(0) = y(0) and the same initial angular velocity x˙(0)=y˙(0)\dot{x}(0) = \dot{y}(0), then the two solutions are identical, i.e., x=yx = y.

theorem

Time reversal of a solution θ(t)\theta(t) is a solution for the simple pendulum

Let SS be a simple pendulum and θ:Time→R1\theta : \text{Time} \to \mathbb{R}^1 be a smooth function representing its angular position over time. If θ\theta is a solution to the equation of motion for SS, then the time-reversed function t↦θ(−t)t \mapsto \theta(-t) is also a solution. This holds because the equation of motion for the simple pendulum contains no velocity-dependent (damping) terms, ensuring that the angular acceleration is invariant under time reversal.

theorem

θ(−t)=θ(t)\theta(-t) = \theta(t) for a simple pendulum released from rest

Consider a simple pendulum SS and a smooth solution θ:Time→R1\theta: \text{Time} \to \mathbb{R}^1 to its equation of motion. If the pendulum is released from rest at time t=0t = 0, such that its initial angular velocity is zero (i.e., dθdt∣t=0=0\left. \frac{d\theta}{dt} \right|_{t=0} = 0), then the angular displacement θ\theta is an even function of time, satisfying θ(−t)=θ(t)\theta(-t) = \theta(t) for all t∈Timet \in \text{Time}.

theorem

The phase-space vector field of the simple pendulum is C∞C^\infty

For any n∈N∪{∞}n \in \mathbb{N} \cup \{\infty\}, the phase-space vector field V:R×R→R×RV: \mathbb{R} \times \mathbb{R} \to \mathbb{R} \times \mathbb{R} of the simple pendulum, defined by V(θ,θ˙)=(θ˙,−ω2sin⁡θ)V(\theta, \dot{\theta}) = (\dot{\theta}, -\omega^2 \sin \theta), is nn-times continuously differentiable (CnC^n) over R\mathbb{R}.

theorem

Local Existence of Solutions for the Simple Pendulum

For any initial angle x0x_0 and initial angular velocity v0v_0 (represented as elements of a one-dimensional Euclidean space), there exists a time interval ϵ>0\epsilon > 0 and a curve θ:Time→R\theta: \text{Time} \to \mathbb{R} such that the initial angle θ(0)=x0\theta(0) = x_0 and the initial angular velocity θ˙(0)=v0\dot{\theta}(0) = v_0. Furthermore, for all times tt within the interval ∣t∣≤ϵ|t| \le \epsilon, the curve θ\theta and its time derivative θ˙\dot{\theta} are differentiable, and they satisfy the equation of motion I⋅θ¨(t)=τ(θ(t))I \cdot \ddot{\theta}(t) = \tau(\theta(t)), where II is the moment of inertia and τ\tau is the torque of the pendulum.