@MISC{PDLAX.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Shidama, Yasunari},
  TITLE = {On the Properties of Curves and Parametrization-Independent Isoperimetric Inequality},
  SECTION1 = {Preliminaries and Basic Theorems},
  SECTION2 = {Arc Length Parametrization},
  SECTION3 = {Parametrization-Independent Isoperimetric Inequality},
  DAY = {14},
  MONTH = {December},
  YEAR = {2024},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS1 = {Karuizawa Hotch 244-1\\Nagano, Japan},
  MSC2020 = {26B15 49Q20 68V20},
  KEYWORDS = {isoperimetric theorem; differential geometry; parametric curves},
  SUMMARY = {This article formalizes several properties of curves and establishes a parametrization-independent isoperimetric inequality. The paper is structured into three main sections:
\begin{enumerate}
\item Preliminaries and Basic Theorems: Introduces fundamental definitions, notations, and initial theorems, including the definition of the ArcLenP function.
\item Arc Length Parametrization: Constructs arc length parametrization and explores its properties, including differentiability and characteristics of its inverse function.
\item Parametrization-Independent Isoperimetric Inequality: Proves an isoperimetric inequality that holds regardless of the curve's parametrization.
\end{enumerate}
    This formalization provides a rigorous foundation for further work in differential geometry and analysis. We referred to \cite{Pressley:2010}, \cite{PeterLax:1995} and \cite{Hehl:2013} in this formalization.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI Grant Number 24K14897.}}

@article{PeterLax:1995,
    author = {Peter D. Lax},
    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}
}

@book{Pressley:2010,
  title={Elementary Differential Geometry},
  author={Pressley, Andrew N.},
  year={2010},
  publisher={Springer Science \& Business Media}
}
