@MISC{NDIFF12.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Shidama, Yasunari},
  TITLE = {Differentiability Properties of Lipschitzian Bilinear Operators in Real Normed Spaces},
  SECTION1 = {Fundamental Properties and Partial Differentiability},
  SECTION2 = {Total Differentiability and Continuity},
  SECTION3 = {Higher-Order Derivatives and Special Properties},
  DAY = {9},
  MONTH = {December},
  YEAR = {2024},
  ADDRESS1 = {Yamaguchi University\\Yamaguchi, Japan},
  ADDRESS1 = {Karuizawa Hotch 244-1\\Nagano, Japan},
  MSC2020 = {46G05 47A07 68V20},
  KEYWORDS = {functional analysis; bilinear operators; Lipschitz continuity; differentiability; normed spaces},
  SUMMARY = {This article formalizes various differentiability properties of Lipschitzian bilinear
    operators in real normed spaces.
    It covers topics such as partial differentiability, continuity, and total differentiability of these operators.
    The work extends results for linear operators to the bilinear case and provides theorems
    on the behavior of differential operators up to arbitrary order.
    Key results include the Lipschitz continuity of partial derivatives,
    the representation of the total derivative in terms of partial derivatives,
    and the continuous differentiability of Lipschitzian bilinear operators on open subsets of the product space.
    We referred to \cite{miyadera:1972}, \cite{yoshida:1980}, \cite{Schwartz1997a},
    \cite{Schwartz1997b} in this formalization.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI Grant Number 24K14897.}}

@BOOK{miyadera:1972,
 AUTHOR={Miyadera, Isao},
 TITLE={Functional Analysis},
 PUBLISHER={Riko-Gaku-Sya},
 YEAR=1972}

@BOOK{yoshida:1980,
 AUTHOR={Yoshida, Kosaku},
 TITLE={Functional Analysis},
 PUBLISHER={Springer},
 YEAR=1980}

@BOOK{Schwartz1997a,
  TITLE={Th\'{e}orie des ensembles et topologie, tome 1. {A}nalyse},
  AUTHOR={Schwartz, Laurent},
  PUBLISHER={Hermann},
  YEAR={1997}}

@BOOK{Schwartz1997b,
  TITLE = {Calcul diff\'{e}rentiel, tome 2. {A}nalyse},
  AUTHOR = {Schwartz, Laurent},
  PUBLISHER = {Hermann},
  YEAR = {1997}}
