The area–energy inequality for closed plane curves #
For a plane curve γ = x + i y : ℝ → ℂ on [a, b], its signed area is the boundary integral
½ ∫ₐᵇ (x y' - y x') (TauCeti.signedArea, defined in
TauCeti.Analysis.Green.Examples.CurveArea.SignedArea).
The main result is the sharp area–energy inequality for absolutely continuous closed curves with square-integrable derivative,
4π |signedArea γ a b| ≤ (b - a) ∫ₐᵇ ‖γ'‖²
(TauCeti.four_pi_mul_abs_signedArea_le),
with its complete equality analysis: equality holds exactly when γ is constant or traces a
circle once at constant angular speed, in one of the two orientations
(TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff). The Wirtinger inequality
for the mean-zero part of γ admits every ellipse as an equality case; the area–energy
inequality does not.
Equality also holds exactly when, for some center c and sign s = ±1, the a.e. velocity is
(2πis / (b - a)) * (γ - c)
(TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff_ae_hasDerivAt).
The AC integrating-factor theorem in TauCeti.Analysis.ODE.ScalarLinear recovers the pointwise
exponential parametrization from this a.e. equation.
For a closed curve of constant speed on [a, b], in particular an arclength parametrization,
(b - a) ∫ₐᵇ ‖γ'‖² is the square of its length L, so the inequality becomes the isoperimetric
inequality 4π |signedArea γ a b| ≤ L²
(HasConstantSpeedOnWith.four_pi_mul_abs_signedArea_le_eVariationOn_toReal_sq), with equality
exactly for constant curves and circles traversed once
(HasConstantSpeedOnWith.eVariationOn_toReal_sq_eq_four_pi_mul_abs_signedArea_iff).
Passing to the natural parameterization gives the isoperimetric inequality
4π |rectifiableSignedArea γ a b| ≤ L² for every continuous closed plane curve, where
L = (eVariationOn γ (Icc a b)).toReal is its total variation and
TauCeti.rectifiableSignedArea is the geometric signed area
(TauCeti.four_pi_mul_abs_rectifiableSignedArea_le). No absolute continuity of the parameter is
assumed. For a curve of infinite variation both sides are zero by convention, so the inequality
has content only for curves of bounded variation. For a continuous closed curve of bounded
variation, equality holds exactly when the curve traverses a circle once, uniformly in arclength,
or is constant (TauCeti.eVariationOn_toReal_sq_eq_four_pi_mul_abs_rectifiableSignedArea_iff).
The proof is Fourier-analytic and works directly at absolutely continuous regularity. Writing
c n for the Fourier coefficients of γ on [a, b], Parseval's identity applied to γ, to
γ' and to γ' - (2πi / (b - a)) γ gives the classical formula
signedArea γ a b = π ∑ n ‖c n‖² (TauCeti.hasSum_mul_sq_fourierCoeffOn_signedArea), while
(b - a) ∫ ‖γ'‖² = 4π² ∑ n² ‖c n‖². Since n² ≥ ± n for integers, with equality only at 0
and ± 1, both the inequality and its equality cases follow, since a continuous function on
[a, b] is determined by its Fourier coefficients.
Main results #
TauCeti.hasSum_mul_sq_fourierCoeffOn_signedArea: the Fourier series of the signed area.TauCeti.four_pi_mul_abs_signedArea_le: the area–energy inequality.TauCeti.mul_integral_norm_sq_eq_four_pi_mul_signedArea_iff,TauCeti.mul_integral_norm_sq_eq_neg_four_pi_mul_signedArea_iff,TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff: its equality cases.TauCeti.mul_integral_norm_sq_eq_intCast_mul_four_pi_mul_signedArea_iff_ae_hasDerivAt,TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff_ae_hasDerivAt: equality characterized by the a.e. velocity equation.HasConstantSpeedOnWith.four_pi_mul_abs_signedArea_le_eVariationOn_toReal_sq,HasConstantSpeedOnWith.eVariationOn_toReal_sq_eq_four_pi_mul_abs_signedArea_iff: the isoperimetric inequality in terms of length for constant-speed closed curves, and its equality case.TauCeti.four_pi_mul_abs_rectifiableSignedArea_le,TauCeti.eVariationOn_toReal_sq_eq_four_pi_mul_abs_rectifiableSignedArea_iff: the isoperimetric inequality for continuous closed curves of bounded variation, and its equality case.
References #
- A. Hurwitz, Sur le problème des isopérimètres, C. R. Acad. Sci. Paris 132 (1901), 401–403 (the Fourier-series proof of the isoperimetric inequality).
- A. Hurwitz, Sur quelques applications géométriques des séries de Fourier, Ann. Sci. École Norm. Sup. (3) 19 (1902), 357–408.
The Fourier series of the signed area. For an absolutely continuous closed curve with
square-integrable derivative, the signed area is π ∑ n ‖c n‖², where c n are the Fourier
coefficients of the curve on [a, b].
The area–energy inequality. For an absolutely continuous closed plane curve on [a, b]
with square-integrable derivative, 4π |signedArea γ a b| ≤ (b - a) ∫ₐᵇ ‖γ'‖². For a curve
parametrized proportionally to arclength the right side is the square of its length.
Equality in the area–energy inequality, positive orientation. For an absolutely
continuous closed plane curve with square-integrable derivative, (b - a) ∫ₐᵇ ‖γ'‖² equals
4π signedArea γ a b exactly when γ is constant or traverses a circle once counterclockwise
at constant angular speed.
Equality in the area–energy inequality, negative orientation. For an absolutely
continuous closed plane curve with square-integrable derivative, (b - a) ∫ₐᵇ ‖γ'‖² equals
-4π signedArea γ a b exactly when γ is constant or traverses a circle once clockwise at
constant angular speed.
Equality in the area–energy inequality. For an absolutely continuous closed plane curve
with square-integrable derivative, (b - a) ∫ₐᵇ ‖γ'‖² = 4π |signedArea γ a b| exactly when γ
is constant or traverses a circle once at constant angular speed, in either orientation.
Equality in the oriented area–energy inequality is equivalent to a uniform angular
velocity about a center, almost everywhere. The sign s = ±1 specifies the orientation;
constant curves are included.
Equality in the area–energy inequality is equivalent to the a.e. equation for one
counterclockwise or clockwise traversal at constant angular speed about some center.
Constant curves are included. See AbsolutelyContinuousOnInterval.ae_hasDerivAt_smul_sub_iff
for the corresponding pointwise exponential parametrization.
The isoperimetric inequality for constant-speed closed curves. A closed plane curve
traversed at constant speed on [a, b] has signed area at most L² / (4π) in absolute value,
where L is its length. This applies in particular to arclength parametrizations.
Equality in the isoperimetric inequality for constant-speed closed curves. For a closed
plane curve traversed at constant speed on [a, b], the square of its length equals
4π |signedArea γ a b| exactly when the curve is constant or traverses a circle once, in either
orientation.
The isoperimetric inequality for rectifiable closed curves. A continuous closed plane
curve on [a, b] has geometric signed area at most L² / (4π) in absolute value, where L is
its length, the total variation of the curve on [a, b]. The parameter need not be absolutely
continuous; for a curve of infinite length both sides are zero by convention.
Equality in the isoperimetric inequality for rectifiable closed curves. For a continuous
closed plane curve of bounded variation on [a, b] with length L, the equality
L² = 4π |rectifiableSignedArea γ a b| holds exactly when, for some center c and some w, the
curve is c + w exp(± 2π i s(t) / L), where s(t) is the length of the curve on [a, t]. That
is, the curve traverses a circle once, uniformly in arclength and in either orientation, or is
constant. The parameter itself need not be absolutely continuous or of constant speed.