Physlib.ClassicalMechanics.Pendulum.SimplePendulum.PeriodFormula

The period formula of the simple gravity pendulum

i. Overview

Beyond the small-angle approximation the period of the simple gravity pendulum depends on the amplitude of the swing. Released from rest at the angle `θ₀`, with `0 < θ₀ < π`, the pendulum librates about the bottom of its swing, and the classical calculation (Landau & Lifshitz, §11, Problem 1) integrates the energy first integral by quadrature: the quarter period is the time of descent from `θ₀` to the bottom, the substitution `sin (θ/2) = sin (θ₀/2) sin φ` turns the resulting integral into a complete elliptic integral of the first kind, and the period is

`T = 4 √(ℓ/g) K(sin ½θ₀)`,

with `K` Legendre's complete elliptic integral of the first kind in the modulus convention. In the parameter convention of `Real.completeEllipticK`, where the parameter is the square `m = k²` of the modulus, the same formula reads `4 √(ℓ/g) completeEllipticK (sin² (θ₀/2))`.

This module records that formula as `SimplePendulum.periodFormula` and proves what follows for it from the theory of `completeEllipticK` alone: it is even in the amplitude, at zero amplitude it is the small-angle period `2π √(ℓ/g)`, it is continuous on `(-π, π)` and tends to the small-angle period as the amplitude tends to zero, it is never below the small-angle period, it is strictly increasing in the amplitude on `[0, π)`, and it is at most `2π √(ℓ/g) / cos (θ₀/2)`. The formula is therefore not constant in the amplitude — the classical statement that the pendulum is not isochronous, once the identification below is proved — and the upper bound quantifies how it grows as the amplitude approaches the inverted position.

What this module does not do is identify `periodFormula θ₀` with the period of a solution of the nonlinear equation of motion released from rest at `θ₀`. That identification is the theorem the formula is named for, and its formalization — the quarter period as a first hitting time, the quadrature of the energy first integral, the substitution, and their assembly, on top of the uniqueness of solutions and the time-reversal symmetry of the equation of motion (formalized in the companion module `SimplePendulum/Solution.lean`) — is not yet carried out; the `TODO` after the definition lists the milestones. Until then `periodFormula` is a definition, and the statements about it are statements about the elliptic integral.

ii. Key results

- `SimplePendulum.periodFormula` is the classical formula `4 √(ℓ/g) K(sin² (θ₀/2))` for the period of libration with amplitude `θ₀`; for `|θ₀| < π` its parameter `sin² (θ₀/2)` lies below `1` (`Real.sin_half_sq_lt_one`), so it is evaluated on the domain of `completeEllipticK`. - `SimplePendulum.periodFormula_neg`: the formula is even in the amplitude. - `SimplePendulum.periodFormula_zero`: at zero amplitude the formula is the small-angle period, `periodFormula 0 = smallAnglePeriod`. - `SimplePendulum.continuousOn_periodFormula` and `SimplePendulum.continuousAt_periodFormula_zero`: the formula is continuous on `(-π, π)`, in particular at `0`. - `SimplePendulum.periodFormula_tendsto_smallAnglePeriod`: the formula tends to the small-angle period as the amplitude tends to zero. - `SimplePendulum.periodFormula_mono` and `SimplePendulum.periodFormula_strictMono`, with the bundled `SimplePendulum.monotoneOn_periodFormula` and `SimplePendulum.strictMonoOn_periodFormula`: on `[0, π)` the formula is increasing, and strictly increasing, in the amplitude. - `SimplePendulum.smallAnglePeriod_le_periodFormula` and `SimplePendulum.periodFormula_pos`: the formula is at least the small-angle period, in particular positive, whenever `sin² (θ₀/2) < 1`. - `SimplePendulum.periodFormula_le` and `SimplePendulum.periodFormula_le'`: for `|θ₀| < π` the formula is at most `2π √(ℓ/g) / cos (θ₀/2) = smallAnglePeriod / cos (θ₀/2)`.

iii. Table of contents

- A. The period formula, its continuity and its small-angle limit - A.1. The formula, its domain and its evenness - A.2. Continuity and the small-angle limit - B. Monotonicity and bounds in the amplitude - B.1. Monotonicity in the amplitude - B.2. Bounds

iv. References

- Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1: `T = 4 √(l/g) K(sin ½φ₀)`, in the modulus convention `K(k) = ∫ φ in 0..π/2, (1 - k² sin² φ)^(-1/2)`. - M. Abramowitz, I. A. Stegun, Handbook of Mathematical Functions, 17.3.1 (the parameter convention `K(m)`, `m = k²`, used by `Real.completeEllipticK`). - The module `Physlib.Mathematics.SpecialFunctions.EllipticIntegral`, for `completeEllipticK` and its theory on the domain `m < 1`. - The module `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.SmallAngle`, for the small-angle period `smallAnglePeriod = 2π √(ℓ/g)`.

A. The period formula, its continuity and its small-angle limit

The classical formula for the period of libration as a function of the amplitude, its evenness and its domain, and its behaviour at small amplitudes: it is continuous on the libration range `(-π, π)`, at zero amplitude it is exactly the small-angle period, and it tends to the small-angle period as the amplitude tends to zero. These are facts about the elliptic integral on its domain and at the parameter `0`, where `K 0 = π/2`.

A.1. The formula, its domain and its evenness

The formula `4 √(ℓ/g) K(sin² (θ₀/2))` is defined for every real `θ₀`, and is even in `θ₀`; for libration amplitudes `|θ₀| < π` the parameter `sin² (θ₀/2)` is below `1` (`Real.sin_half_sq_lt_one`), so the elliptic integral is evaluated on its domain. At `θ₀ = ±π` the parameter is `1`, where Legendre's `K` diverges — the pendulum released from rest at the inverted position never returns — while the Lean value of `completeEllipticK` at `m = 1` is a junk value (see the module docstring of `Physlib.Mathematics.SpecialFunctions.EllipticIntegral`), so nothing is claimed there.

A.2. Continuity and the small-angle limit

At zero amplitude the parameter of the elliptic integral is `0`, where `K 0 = π/2`, and the formula collapses to `4 √(ℓ/g) · π/2 = 2π √(ℓ/g)`: the small-angle period. Since `K` is continuous on its domain and the parameter `sin² (θ₀/2)` is continuous in the amplitude and stays below `1` for `|θ₀| < π`, the formula is continuous on `(-π, π)`; in particular it tends to the small-angle period as the amplitude tends to zero — the sense in which the small-angle theory of `SimplePendulum.SmallAngle` is the limit of the classical formula.

B. Monotonicity and bounds in the amplitude

The dependence of the period formula on the amplitude is inherited from the dependence of `completeEllipticK` on its parameter: on `[0, π)` the parameter `sin² (θ₀/2)` is strictly increasing in `θ₀` and stays below `1`, and `K` is strictly increasing on `(-∞, 1)`, so the formula is strictly increasing in the amplitude. The bounds `π/2 ≤ K m ≤ (π/2) (1 - m)^(-1/2)` on `[0, 1)` sandwich the formula between the small-angle period and `2π √(ℓ/g) / cos (θ₀/2)`.

B.1. Monotonicity in the amplitude

For `0 ≤ θ₁ ≤ θ₂ < π` the half-angles lie in `[0, π/2)`, where the sine is nonnegative and increasing, so `sin² (θ₁/2) ≤ sin² (θ₂/2) < 1`, and the monotonicity of `K` on its domain does the rest. The strict version uses the strict monotonicity of the sine on the same interval and of `K`. Both are restated as bundled `MonotoneOn` and `StrictMonoOn` facts on `[0, π)`.

B.2. Bounds

The lower bound `π/2 ≤ K m` on `[0, 1)` says that the period formula is never below the small-angle period: the formula is least at zero amplitude, and in particular positive. The upper bound `K m ≤ (π/2) (1 - m)^(-1/2)`, with `1 - sin² (θ₀/2) = cos² (θ₀/2)`, bounds the formula by `2π √(ℓ/g) / cos (θ₀/2)` for `|θ₀| < π`: the formula is at most the small-angle period divided by the cosine of the half-amplitude, a quantity that grows without bound as the amplitude approaches the inverted position.

14 declarations

definition

Period formula for a simple pendulum

#periodFormula

For a simple gravity pendulum with length $\ell$ and gravitational acceleration $g$ , the period $T$ as a function of the release amplitude $\theta_0$ is defined by the formula: $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ where $K(m)$ is the complete elliptic integral of the first kind evaluated with parameter $m = \sin^2 \frac{\theta_0}{2}$ .

theorem

The Period Formula $T(\theta_0)$ is Even in the Amplitude $\theta_0$

#periodFormula_neg

For any release amplitude $\theta_0 \in \mathbb{R}$ , the period formula of the simple gravity pendulum $T(\theta_0)$ is even in the amplitude, satisfying $T(-\theta_0) = T(\theta_0)$ .

theorem

At zero amplitude, $T(0)$ equals the small-angle period $2\pi \sqrt{\ell/g}$

#periodFormula_zero

For a simple gravity pendulum with length $\ell$ and gravitational acceleration $g$ , the period formula $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ evaluated at zero release amplitude $\theta_0 = 0$ is equal to the small-angle period $2\pi \sqrt{\frac{\ell}{g}}$ . Here, $K(m)$ denotes the complete elliptic integral of the first kind with parameter $m$ .

theorem

$T(\theta_0)$ is continuous on $(-\pi, \pi)$

#continuousOn_periodFormula

The period formula $T(\theta_0)$ for a simple gravity pendulum, defined as $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ (where $K(m)$ is the complete elliptic integral of the first kind with parameter $m$ , $\ell$ is the pendulum length, and $g$ is the gravitational acceleration), is continuous on the open interval $(-\pi, \pi)$ of release amplitudes $\theta_0$ .

theorem

The period formula $T(\theta_0)$ is continuous at $\theta_0 = 0$

#continuousAt_periodFormula_zero

For a simple gravity pendulum, the period formula $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ , where $\theta_0$ is the release amplitude and $K$ is the complete elliptic integral of the first kind, is continuous at $\theta_0 = 0$ .

theorem

$T(\theta_0) \to 2\pi \sqrt{\ell/g}$ as $\theta_0 \to 0$

#periodFormula_tendsto_smallAnglePeriod

As the release amplitude $\theta_0$ approaches $0$ , the period formula for a simple gravity pendulum $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ tends to the small-angle period $2\pi \sqrt{\frac{\ell}{g}}$ . Here, $\ell$ is the length of the pendulum, $g$ is the gravitational acceleration, and $K(m)$ is the complete elliptic integral of the first kind with parameter $m$ .

theorem

The period formula $T(\theta_0)$ is non-decreasing for $0 \le \theta_0 < \pi$

#periodFormula_mono

For any real numbers $\theta_1$ and $\theta_2$ such that $0 \le \theta_1 \le \theta_2 < \pi$ , the period formula for a simple gravity pendulum $T(\theta_0)$ satisfies $T(\theta_1) \le T(\theta_2)$ . Here, the period formula is defined as $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ , where $\ell$ is the length of the pendulum, $g$ is the gravitational acceleration, and $K(m)$ is Legendre's complete elliptic integral of the first kind with parameter $m$ .

theorem

The pendulum period $T(\theta_0)$ is strictly increasing on $[0, \pi)$

#periodFormula_strictMono

Let $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ be the period formula for a simple gravity pendulum with length $\ell$ and gravitational acceleration $g$ , where $K(m)$ is the complete elliptic integral of the first kind. For any release amplitudes $\theta_1, \theta_2 \in \mathbb{R}$ such that $0 \le \theta_1 < \theta_2 < \pi$ , it holds that $T(\theta_1) < T(\theta_2)$ .

theorem

The period formula is monotone on $[0, \pi)$

#monotoneOn_periodFormula

The period formula for a simple gravity pendulum, $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ , is monotonically non-decreasing as a function of the release amplitude $\theta_0$ on the interval $[0, \pi)$ .

theorem

The period formula $T(\theta_0)$ is strictly increasing on $[0, \pi)$

#strictMonoOn_periodFormula

The period formula for a simple gravity pendulum, $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ , is strictly increasing on the interval $[0, \pi)$ . Here, $\theta_0$ is the release amplitude, $\ell$ is the pendulum length, $g$ is the gravitational acceleration, and $K(m)$ is the complete elliptic integral of the first kind with parameter $m$ .

theorem

The small-angle period is a lower bound for the period formula: $T_{\text{small}} \le T(\theta_0)$

#smallAnglePeriod_le_periodFormula

For a simple gravity pendulum with release amplitude $\theta_0 \in \mathbb{R}$ such that $\sin^2 \frac{\theta_0}{2} < 1$ , the period $T(\theta_0)$ is greater than or equal to the small-angle period $T_{\text{small}}$ . That is, $T_{\text{small}} \le T(\theta_0)$ where $T_{\text{small}} = 2\pi \sqrt{\frac{\ell}{g}}$ is the small-angle period and $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ is the period formula calculated using Legendre's complete elliptic integral of the first kind $K$ .

theorem

The simple pendulum period $T(\theta_0)$ is strictly positive for $\sin^2(\frac{\theta_0}{2}) < 1$

#periodFormula_pos

For a simple gravity pendulum with release amplitude $\theta_0$ such that $\sin^2\left(\frac{\theta_0}{2}\right) < 1$ , the period $T(\theta_0)$ given by the formula $T(\theta_0) = 4 \sqrt{\frac{\ell}{g}} K\left(\sin^2 \frac{\theta_0}{2}\right)$ is strictly positive, where $K$ is Legendre's complete elliptic integral of the first kind.

theorem

Upper Bound for the Simple Pendulum Period: $T(\theta_0) \le \frac{2\pi \sqrt{\ell/g}}{\cos(\theta_0/2)}$

#periodFormula_le

Let $\theta_0$ be the release amplitude of a simple gravity pendulum with length $\ell$ and gravitational acceleration $g$ . If $|\theta_0| < \pi$ , then the period of the pendulum, given by the formula $T(\theta_0) = 4 \sqrt{\ell/g} K(\sin^2(\theta_0/2))$ , satisfies the inequality: $T(\theta_0) \le \frac{2\pi \sqrt{\ell/g}}{\cos(\theta_0/2)}$ where $K$ is Legendre's complete elliptic integral of the first kind.

theorem

Upper Bound for Simple Pendulum Period: $T(\theta_0) \le T_{\text{small}} / \cos(\theta_0/2)$

#periodFormula_le'

Let $\theta_0$ be the release amplitude of a simple gravity pendulum. If $|\theta_0| < \pi$ , then the period of the pendulum $T(\theta_0)$ is at most the small-angle period $T_{\text{small}}$ divided by $\cos(\theta_0/2)$ : $T(\theta_0) \le \frac{T_{\text{small}}}{\cos(\theta_0/2)}$ where $T_{\text{small}} = 2\pi \sqrt{\ell/g}$ is the period predicted by the small-angle approximation.

Physlib.ClassicalMechanics.Pendulum.SimplePendulum.PeriodFormula

The period formula of the simple gravity pendulum

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The period formula, its continuity and its small-angle limit

A.1. The formula, its domain and its evenness

A.2. Continuity and the small-angle limit

B. Monotonicity and bounds in the amplitude

B.1. Monotonicity in the amplitude

B.2. Bounds

Period formula for a simple pendulum

The Period Formula T(θ0)T(\theta_0)T(θ0​) is Even in the Amplitude θ0\theta_0θ0​

At zero amplitude, T(0)T(0)T(0) equals the small-angle period 2πℓ/g2\pi \sqrt{\ell/g}2πℓ/g​

T(θ0)T(\theta_0)T(θ0​) is continuous on (−π,π)(-\pi, \pi)(−π,π)

The period formula T(θ0)T(\theta_0)T(θ0​) is continuous at θ0=0\theta_0 = 0θ0​=0

T(θ0)→2πℓ/gT(\theta_0) \to 2\pi \sqrt{\ell/g}T(θ0​)→2πℓ/g​ as θ0→0\theta_0 \to 0θ0​→0

The period formula T(θ0)T(\theta_0)T(θ0​) is non-decreasing for 0≤θ0<π0 \le \theta_0 < \pi0≤θ0​<π

The pendulum period T(θ0)T(\theta_0)T(θ0​) is strictly increasing on [0,π)[0, \pi)[0,π)

The period formula is monotone on [0,π)[0, \pi)[0,π)

The period formula T(θ0)T(\theta_0)T(θ0​) is strictly increasing on [0,π)[0, \pi)[0,π)

The small-angle period is a lower bound for the period formula: Tsmall≤T(θ0)T_{\text{small}} \le T(\theta_0)Tsmall​≤T(θ0​)

The simple pendulum period T(θ0)T(\theta_0)T(θ0​) is strictly positive for sin⁡2(θ02)<1\sin^2(\frac{\theta_0}{2}) < 1sin2(2θ0​​)<1

Upper Bound for the Simple Pendulum Period: T(θ0)≤2πℓ/gcos⁡(θ0/2)T(\theta_0) \le \frac{2\pi \sqrt{\ell/g}}{\cos(\theta_0/2)}T(θ0​)≤cos(θ0​/2)2πℓ/g​​

Upper Bound for Simple Pendulum Period: T(θ0)≤Tsmall/cos⁡(θ0/2)T(\theta_0) \le T_{\text{small}} / \cos(\theta_0/2)T(θ0​)≤Tsmall​/cos(θ0​/2)

The Period Formula $T(\theta_0)$ is Even in the Amplitude $\theta_0$

At zero amplitude, $T(0)$ equals the small-angle period $2\pi \sqrt{\ell/g}$

$T(\theta_0)$ is continuous on $(-\pi, \pi)$

The period formula $T(\theta_0)$ is continuous at $\theta_0 = 0$

$T(\theta_0) \to 2\pi \sqrt{\ell/g}$ as $\theta_0 \to 0$

The period formula $T(\theta_0)$ is non-decreasing for $0 \le \theta_0 < \pi$

The pendulum period $T(\theta_0)$ is strictly increasing on $[0, \pi)$

The period formula is monotone on $[0, \pi)$

The period formula $T(\theta_0)$ is strictly increasing on $[0, \pi)$

The small-angle period is a lower bound for the period formula: $T_{\text{small}} \le T(\theta_0)$

The simple pendulum period $T(\theta_0)$ is strictly positive for $\sin^2(\frac{\theta_0}{2}) < 1$

Upper Bound for the Simple Pendulum Period: $T(\theta_0) \le \frac{2\pi \sqrt{\ell/g}}{\cos(\theta_0/2)}$

Upper Bound for Simple Pendulum Period: $T(\theta_0) \le T_{\text{small}} / \cos(\theta_0/2)$