@MISC{PDLAX.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Shidama, Yasunari},
  TITLE = {Classical Isoperimetric Theorem},
  SECTION1 = {Foundations of Continuity and Integration},
  SECTION2 = {Differentiation Rules and Properties},
  SECTION3 = {Properties of Parametric Curves and Area Calculations},
  SECTION4 = {Formalization of the Isoperimetric Theorem},
  DAY = {14},
  MONTH = {December},
  YEAR = {2024},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS2 = {Karuizawa Hotch 244-1\\Nagano, Japan},
  MSC2020 = {26B15 49Q20 68V20},
  KEYWORDS = {isoperimetric theorem; calculus of variations, parametric curves},
  SUMMARY = {This article presents a formalization of the isoperimetric theorem, inspired by Peter D. Lax's "A Short Path to the Shortest Path"~\cite{PeterLax:1995}. Notably, Lax's proof is remarkably concise, spanning just one page, demonstrating the elegance of his approach.\par
Our formalization begins by establishing fundamental properties of continuous and differentiable functions, including theorems on integrals and differentiation rules. Building upon these, it progresses to the proof of the isoperimetric theorem, addressing the following question: Among all curves of fixed length connecting two points on the x-axis, which curve maximizes the area between the curve and the x-axis? The formalization proves that for parametric curves $(x(t), y(t))$ with fixed length and endpoints on the x-axis, the integral $\int_0^\pi y(t) x'(t)\,dt$ is maximized when the curve is a semicircle.
\par
This work represents the 99th problem solved in Freek Wiedijk's "Formalizing 100 Theorems" project, underscoring the significance of this effort in the context of formalization of mathematics. The historical background on the isoperimetric theorem is detailed in \cite{Hehl:2013} and \cite{Viktor:2005}.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI Grant Number 24K14897.}}

@article{PeterLax:1995,
    author = {Lax, Peter D.},
    title = {A Short Path to the Shortest Path},
    journal = {The American Mathematical Monthly},
    volume = {102},
    number = {2},
    pages = {158-159},
    year  = {1995},
    publisher = {Taylor \& Francis}
}

@article{Hehl:2013,
  title={The Isoperimetric Inequality},
  author={Hehl, Andreas},
  journal={Proseminar Curves and Surfaces, Universitaet Tuebingen, Tuebingen},
  year={2013}
}

@article{Viktor:2005,
    author = {Blåsjö, Viktor},
    title = {The Isoperimetric Problem},
    journal = {The American Mathematical Monthly},
    volume = {112},
    number = {6},
    pages = {526-566},
    year  = {2005},
    publisher = {Taylor \& Francis}
}
