:: Differentiation in Normed Spaces
::  by Noboru Endou and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
      NAT_1, FDIFF_1, SUBSET_1, RELAT_1, LOPBAN_1, ORDINAL4, RCOMP_1, TARSKI,
      ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, CARD_1, XXREAL_0, XBOOLE_0, CARD_3,
      FINSEQ_1, NDIFF_6;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_3, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, FINSEQ_1, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_1,
      VFUNCT_1, LOPBAN_1, NFCONT_1, NDIFF_1;
 constructors NFCONT_1, VFUNCT_1, NDIFF_1, RELSET_1, PRVECT_2;
 registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, FUNCT_1, INT_1, FUNCT_2,
      XBOOLE_0, SUBSET_1, FINSEQ_1, CARD_3, LOPBAN_1, PRVECT_3, NAT_1,
      AOFA_A00;
 requirements SUBSET, REAL, NUMERALS, ARITHM;


begin :: Preliminaries

theorem :: NDIFF_6:1
for D,E,F be non empty set holds
 ex I be Function of Funcs(D,Funcs(E,F)), Funcs([:D,E:],F)
  st I is bijective
   & for f be Function of D,Funcs(E,F), d,e be object st d in D & e in E
      holds (I.f).(d,e) = (f.d).e;

theorem :: NDIFF_6:2
for D,E,F be non empty set holds
 ex I be Function of Funcs(D,Funcs(E,F)), Funcs([:E,D:],F)
  st I is bijective
   & for f be Function of D,Funcs(E,F), e,d be object
     st e in E & d in D holds (I.f).(e,d) = (f.d).e;

theorem :: NDIFF_6:3
for D,E be non-empty non empty FinSequence, F be non empty set holds
 ex L being Function of Funcs(product D,Funcs(product E,F)),
                     Funcs(product(E^D),F)
 st L is bijective
  & for f be Function of product D,Funcs(product E,F),
        e,d be FinSequence
    st e in product E & d in product D holds (L.f).(e^d) = (f.d).e;

theorem :: NDIFF_6:4
for X,Y be non empty set holds
 ex I be Function of [:X,Y:],[:X,product <*Y*>:]
  st I is bijective
   & for x,y be object st x in X & y in Y holds I.(x,y) = [x,<*y*>];

theorem :: NDIFF_6:5
for X be non-empty non empty FinSequence, Y be non empty set holds
 ex K be Function of [:product X,Y:],product(X^<*Y*>)
  st K is bijective
   & for x be FinSequence, y be object
       st x in product X & y in Y holds K.(x,y) = x^<*y*>;

theorem :: NDIFF_6:6
for D be non empty set,
    E be non-empty non empty FinSequence,
    F be non empty set holds
 ex L being Function of Funcs(D,Funcs(product E,F)),
                     Funcs(product(E^<*D*>),F)
  st L is bijective
   & for f be Function of D,Funcs(product E,F),
         e be FinSequence, d be object
      st e in product E & d in D holds (L.f).(e^<*d*>) = (f.d).e;

reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve Z for Subset of S;
reserve i,n for Nat;

definition let S be set;
  assume  S is RealNormSpace;
  func modetrans(S) -> RealNormSpace equals
:: NDIFF_6:def 1
  S;
end;

definition let S,T be RealNormSpace;
  func diff_SP(S,T) -> Function means
:: NDIFF_6:def 2
  dom it = NAT & it.0 = T &
  for i be Nat holds
  it.(i+1) = R_NormSpace_of_BoundedLinearOperators(S,modetrans(it.i));
end;

theorem :: NDIFF_6:7
(diff_SP(S,T)).0 = T &
(diff_SP(S,T)).1 = R_NormSpace_of_BoundedLinearOperators(S,T) &
(diff_SP(S,T)).2
   = R_NormSpace_of_BoundedLinearOperators( S,
        R_NormSpace_of_BoundedLinearOperators(S,T) );

theorem :: NDIFF_6:8
for i be Nat holds (diff_SP(S,T)).i is RealNormSpace;

theorem :: NDIFF_6:9
for i be Nat holds
 ex H be RealNormSpace st H = (diff_SP(S,T)).i
 & (diff_SP(S,T)).(i+1) = R_NormSpace_of_BoundedLinearOperators(S,H);

definition
  let S,T be RealNormSpace, i be Nat;
  func diff_SP(i,S,T) -> RealNormSpace equals
:: NDIFF_6:def 3
  diff_SP(S,T).i;
end;

theorem :: NDIFF_6:10
for i be Nat holds
  diff_SP(i+1,S,T) = R_NormSpace_of_BoundedLinearOperators(S,diff_SP(i,S,T));

definition let S,T be RealNormSpace, f be set;
  assume  f is PartFunc of S,T;
  func modetrans(f,S,T) -> PartFunc of S,T equals
:: NDIFF_6:def 4
  f;
end;

definition let S,T be RealNormSpace, f be PartFunc of S,T,
               Z be Subset of S;
  func diff(f,Z) -> Function means
:: NDIFF_6:def 5
  dom it = NAT & it.0 = f|Z &
  for i be Nat holds
   it.(i+1) = modetrans(it.i,S,diff_SP(i,S,T)) `| Z;
end;

theorem :: NDIFF_6:11
diff(f,Z).0 = f|Z & diff(f,Z).1 = (f|Z)`| Z &
diff(f,Z).2 = ((f|Z)`| Z) `| Z;

theorem :: NDIFF_6:12
for i be Nat holds diff(f,Z).i is PartFunc of S,diff_SP(i,S,T);

definition
  let S,T be RealNormSpace, f be PartFunc of S,T,
      Z be Subset of S, i be Nat;
  func diff(f,i,Z) -> PartFunc of S,diff_SP(i,S,T) equals
:: NDIFF_6:def 6
  diff(f,Z).i;
end;

theorem :: NDIFF_6:13
diff(f,i+1,Z) = diff(f,i,Z) `|Z;

definition
  let S,T be RealNormSpace;
  let f be PartFunc of S,T;
  let Z be Subset of S;
  let n be Nat;
  pred f is_differentiable_on n,Z means
:: NDIFF_6:def 7
    Z c= dom f
  & for i be Nat st i <= n-1 holds
    modetrans(diff(f,Z).i,S,diff_SP(i,S,T)) is_differentiable_on Z;
end;

theorem :: NDIFF_6:14
f is_differentiable_on n,Z
  iff
Z c= dom f & for i be Nat st i <= n-1 holds diff(f,i,Z) is_differentiable_on Z;

theorem :: NDIFF_6:15
f is_differentiable_on 1,Z
  iff
Z c= dom f & f|Z is_differentiable_on Z;

theorem :: NDIFF_6:16
f is_differentiable_on 2,Z
  iff
Z c= dom f & f|Z is_differentiable_on Z &
(f|Z)`|Z is_differentiable_on Z;

theorem :: NDIFF_6:17
for S,T be RealNormSpace, f be PartFunc of S,T,
    Z be Subset of S, n be Nat st
 f is_differentiable_on n,Z for m be Nat st m <= n
  holds f is_differentiable_on m, Z;

theorem :: NDIFF_6:18
for n be Nat, f be PartFunc of S,T
  st 1 <= n & f is_differentiable_on n,Z holds Z is open;

theorem :: NDIFF_6:19
for n being Nat, f being PartFunc of S,T st 1<=n & f is_differentiable_on n,Z
 holds
  for i being Nat st i <= n holds
    diff_SP(S,T).i is RealNormSpace
  & diff(f,Z).i is PartFunc of S,diff_SP(i,S,T) & dom diff(f,i,Z) = Z;

theorem :: NDIFF_6:20
for n being Nat, f,g being PartFunc of S,T
 st 1<=n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
 holds
  for i being Nat st i<=n holds diff(f+g,i,Z) = diff(f,i,Z) + diff(g,i,Z);

theorem :: NDIFF_6:21
for n be Nat, f,g be PartFunc of S,T
 st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
 holds f+g is_differentiable_on n,Z;

theorem :: NDIFF_6:22
for n being Nat, f,g being PartFunc of S,T
 st 1<=n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
 holds
  for i being Nat st i<=n holds diff(f-g,i,Z) = diff(f,i,Z) - diff(g,i,Z);

theorem :: NDIFF_6:23
for n be Nat, f,g be PartFunc of S,T
 st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
 holds f-g is_differentiable_on n,Z;

theorem :: NDIFF_6:24
for n be Nat, r be Real, f be PartFunc of S,T
 st 1<= n & f is_differentiable_on n,Z
 holds
  for i be Nat st i <= n holds diff(r(#)f,i,Z) = r(#)diff(f,i,Z);

theorem :: NDIFF_6:25
for n be Nat, r be Real, f be PartFunc of S,T
 st 1 <= n & f is_differentiable_on n,Z
  holds r(#)f is_differentiable_on n,Z;

theorem :: NDIFF_6:26
for n be Nat, f be PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z
holds
 for i be Nat st i <= n holds diff(-f,i,Z) = -diff(f,i,Z);

theorem :: NDIFF_6:27
for n be Nat, f be PartFunc of S,T st 1<= n & f is_differentiable_on n,Z
 holds -f is_differentiable_on n,Z;