:: Implicit Function Theorem -- Part {II}
::  by Kazuhisa Nakasho and Yasunari Shidama
:: 
:: Received May 27, 2019
:: Copyright (c) 2019-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, RCOMP_1, SQUARE_1, TARSKI,
      ARYTM_3, VALUED_1, ALGSTR_0, PRALG_1, PREPOWER, FUNCT_2, ARYTM_1, SEQ_2,
      ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, XXREAL_0, XBOOLE_0,
      FINSEQ_1, RLVECT_1, CFCONT_1, NDIFF_7, MCART_1, CARD_3, METRIC_1,
      LOPBAN_2, LOPBAN_3, SEQ_4, LOPBAN_8, LOPBAN13;
 notations TARSKI, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1,
      FUNCT_2, BINOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1,
      FINSEQ_1, SEQ_4, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1,
      VFUNCT_1, LOPBAN_1, LOPBAN_2, LOPBAN_3, LOPBAN_5, LOPBAN_8, NFCONT_1,
      PRVECT_2, NDIFF_1, NDIFF_2, PRVECT_3, NDIFF_7, NDIFF_8, LOPBAN13;
 constructors SQUARE_1, VFUNCT_1, NDIFF_1, RELSET_1, NAT_D, RSSPACE3, LOPBAN_3,
      NDIFF_5, NDIFF_2, DOMAIN_1, LOPBAN_8, NDIFF_7, NDIFF_8, SEQ_4, LOPBAN_5,
      LOPBAN13;
 registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, FUNCT_2,
      XBOOLE_0, ORDINAL1, LOPBAN_1, LOPBAN_2, PRVECT_2, PRVECT_3, XXREAL_0,
      XTUPLE_0, NDIFF_7, NDIFF_8, NORMSP_1, SQUARE_1, FINSEQ_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Properties of Lipschitz continuous linear operators

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

theorem :: NDIFF_9:1
  for E,F be RealNormSpace,
      f be PartFunc of E,F,
      Z be Subset of E,
      z be Point of E
  st Z is open
   & z in Z
   & Z c= dom f
   & f is_differentiable_in z
  holds
     f|Z is_differentiable_in z
   & diff(f,z) = diff(f|Z,z);

theorem :: NDIFF_9:2
  for E,F,G be RealNormSpace,
      f be PartFunc of [:E,F:],G,
      Z be Subset of [:E,F:],
      z be Point of [:E,F:]
  st Z is open & z in Z & Z c= dom f
  holds
  ( f is_partial_differentiable_in`1 z
    implies
      ( f|Z is_partial_differentiable_in`1 z
      & partdiff`1(f,z) = partdiff`1(f|Z,z) ) )
  &
  ( f is_partial_differentiable_in`2 z
    implies
      ( f|Z is_partial_differentiable_in`2 z
      & partdiff`2(f,z) = partdiff`2(f|Z,z) ) );

theorem :: NDIFF_9:3
  for X,E,G,F be RealNormSpace,
      BL be BilinearOperator of E,F,G,
      f be PartFunc of X,E,
      g be PartFunc of X,F,
      S be Subset of X
  st BL is_continuous_on the carrier of [:E,F:]
   & S c= dom f & S c= dom g
   & ( for s be Point of X st s in S holds f is_continuous_in s )
   & ( for s be Point of X st s in S holds g is_continuous_in s )
  holds
    ex H be PartFunc of X,G
    st dom H = S
     & ( for s be Point of X st s in S holds H.s = BL. (f.s,g.s) )
     & H is_continuous_on S;

theorem :: NDIFF_9:4
  for E,F be RealNormSpace,
        g be PartFunc of E,F,
        A be Subset of E
  st g is_continuous_on A
   & dom g = A
  holds
    ex xg be PartFunc of E,[:E,F:]
    st dom xg = A
     & ( for x be Point of E st x in A
         holds xg.x = [x,g.x] )
     & xg is_continuous_on A;

theorem :: NDIFF_9:5
  for S, T, V being RealNormSpace
  for x0 being Point of V
  for f1 being PartFunc of the carrier of V, the carrier of S
  for f2 being PartFunc of the carrier of S, the carrier of T
  st x0 in dom (f2 * f1)
   & f1 is_continuous_in x0
   & f2 is_continuous_in f1 /. x0
  holds f2 * f1 is_continuous_in x0;

theorem :: NDIFF_9:6
  for E,F be RealNormSpace,
      z be Point of [:E,F:],
      x be Point of E,
      y be Point of F
  st z = [x,y]
  holds ||.z.|| <= ||.x.|| + ||.y.||;

theorem :: NDIFF_9:7
  for E,F,G be RealNormSpace,
      L be LinearOperator of [:E,F:],G
  holds
    ex L1 be LinearOperator of E,G,
       L2 be LinearOperator of F,G
    st ( for x be Point of E,
             y be Point of F
         holds L. [x,y] = L1.x + L2.y )
     & ( for x be Point of E holds L1.x = L/. [x,0.F] )
     & ( for y be Point of F holds L2.y = L/. [0.E,y] );

theorem :: NDIFF_9:8
  for E,F,G be RealNormSpace,
      L be LinearOperator of [:E,F:],G,
      L11 be LinearOperator of E,G,
      L12 be LinearOperator of F,G,
      L21 be LinearOperator of E,G,
      L22 be LinearOperator of F,G
  st ( for x be Point of E,
           y be Point of F
       holds L. [x,y] = L11.x + L12.y )
   & ( for x be Point of E,
           y be Point of F
       holds L. [x,y] = L21.x + L22.y )
  holds L11 = L21 & L12 = L22;

theorem :: NDIFF_9:9
  for E,F,G be RealNormSpace,
      L1 be LinearOperator of E,G,
      L2 be LinearOperator of F,G
  holds
    ex L be LinearOperator of [:E,F:],G
    st ( for x be Point of E,
             y be Point of F
         holds L. [x,y] = L1.x + L2.y )
     & ( for x be Point of E holds L1.x = L/. [x,0.F] )
     & ( for y be Point of F holds L2.y = L/. [0.E,y] );

theorem :: NDIFF_9:10
  for E,F,G be RealNormSpace,
      L be Lipschitzian LinearOperator of [:E,F:],G
  holds
    ex L1 be Lipschitzian LinearOperator of E,G,
       L2 be Lipschitzian LinearOperator of F,G
    st ( for x be Point of E,
             y be Point of F
         holds L. [x,y] = L1.x + L2.y )
     & ( for x be Point of E holds L1.x = L/. [x,0.F] )
     & ( for y be Point of F holds L2.y = L/. [0.E,y] );

theorem :: NDIFF_9:11
  for E,F,G be RealNormSpace,
      L1 be Lipschitzian LinearOperator of E,G,
      L2 be Lipschitzian LinearOperator of F,G
  holds
    ex L be Lipschitzian LinearOperator of [:E,F:],G
    st ( for x be Point of E,
             y be Point of F
         holds L. [x,y] = L1.x + L2.y )
     & ( for x be Point of E holds L1.x = L/. [x,0.F] )
     & ( for y be Point of F holds L2.y = L/. [0.E,y] );

theorem :: NDIFF_9:12
  for E,F,G be RealNormSpace,
      L be Point of R_NormSpace_of_BoundedLinearOperators([:E,F:],G)
  holds
    ex L1 be Point of R_NormSpace_of_BoundedLinearOperators(E,G),
       L2 be Point of R_NormSpace_of_BoundedLinearOperators(F,G)
    st ( for x be Point of E,
             y be Point of F
         holds L. [x,y] = L1.x + L2.y )
     & ( for x be Point of E holds L1.x = L. [x,0.F] )
     & ( for y be Point of F holds L2.y = L. [0.E,y] )
      & ||.L.|| <= ||.L1.|| + ||.L2.||
      & ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.||;

theorem :: NDIFF_9:13
  for E,F,G be RealNormSpace,
      L be Point of R_NormSpace_of_BoundedLinearOperators([:E,F:],G),
      L11,L12 be Point of R_NormSpace_of_BoundedLinearOperators(E,G),
      L21,L22 be Point of R_NormSpace_of_BoundedLinearOperators(F,G)
  st ( for x be Point of E,
           y be Point of F
       holds L. [x,y] = L11.x + L21.y )
   & ( for x be Point of E,
           y be Point of F
       holds L. [x,y] = L12.x + L22.y )
  holds L11 = L12 & L21 = L22;

begin :: Differentiability of implicit function

theorem :: NDIFF_9:14
  for E,G,F be RealNormSpace,
      Z be Subset of [:E,F:],
      f be PartFunc of [:E,F:], G,
      z be Point of [:E,F:]
  st f is_differentiable_in z
  holds
    f is_partial_differentiable_in`1 z
  & f is_partial_differentiable_in`2 z
  & for dx be Point of E,dy be Point of F holds
    diff(f,z) . [dx,dy] = partdiff`1(f,z).dx + partdiff`2(f,z).dy;

theorem :: NDIFF_9:15
  for E,G,F be RealNormSpace,
      Z be Subset of [:E,F:],
      f be PartFunc of [:E,F:], G,
      a be Point of E,
      b be Point of F,
      c be Point of G,
      z be Point of [:E,F:],
      r1,r2 be Real,
      g be PartFunc of E,F,
      P be Lipschitzian LinearOperator of E,G,
      Q be Lipschitzian LinearOperator of G,F
  st Z is open & dom f = Z
   & z = [a,b] & z in Z
   & f.(a,b) = c
   & f is_differentiable_in z
   & 0 < r1 & 0 < r2
   & dom g = Ball(a,r1) & rng g c= Ball(b,r2)
   & g.a = b
   & g is_continuous_in a
   & ( for x be Point of E st x in Ball(a,r1) holds f.(x,g.x) = c )
   & partdiff`2(f,z) is one-to-one
   & Q = partdiff`2(f,z)"
   & P = partdiff`1(f,z)
  holds
     g is_differentiable_in a
   & diff(g,a) = - Q*P;

 reserve X,Y,Z for non trivial RealBanachSpace;

theorem :: NDIFF_9:16
  for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
  st u is invertible
  holds
    ex K,s be Real
    st 0 <= K & 0 < s
     & for du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
       st ||.du.|| < s
       holds
         u+du is invertible
       & ||.Inv(u+du) - Inv u - (- (Inv u)*du*(Inv u) ) .||
          <= K * (||.du.|| * ||.du.||);

theorem :: NDIFF_9:17
  for I be PartFunc of
         R_NormSpace_of_BoundedLinearOperators(X,Y),
         R_NormSpace_of_BoundedLinearOperators(Y,X)
  st dom I = InvertibleOperators(X,Y)
   & for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
      st u in InvertibleOperators(X,Y)
     holds I.u = Inv u
  holds
    for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
     st u in InvertibleOperators(X,Y)
    holds I is_differentiable_in u
        & for du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
          holds diff(I,u).du = - (Inv u) * du * (Inv u);

theorem :: NDIFF_9:18
  ex I be PartFunc of
         R_NormSpace_of_BoundedLinearOperators(X,Y),
         R_NormSpace_of_BoundedLinearOperators(Y,X)
  st dom I = InvertibleOperators(X,Y)
   & rng I = InvertibleOperators(Y,X)
   & I is one-to-one
   & I is_differentiable_on InvertibleOperators(X,Y)
   & ( ex J be PartFunc of
           R_NormSpace_of_BoundedLinearOperators(Y,X),
           R_NormSpace_of_BoundedLinearOperators(X,Y)
       st J = I"
        & J is one-to-one
        & dom J = InvertibleOperators(Y,X)
        & rng J = InvertibleOperators(X,Y)
        & J is_differentiable_on InvertibleOperators(Y,X))
   & ( for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
       st u in InvertibleOperators(X,Y)
       holds I.u = Inv u )
   & for u,du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
     st u in InvertibleOperators(X,Y)
     holds diff(I,u).du =- (Inv u) * du * (Inv u);

theorem :: NDIFF_9:19
  for E,G,F be RealNormSpace,
      Z be Subset of [:E,F:],
      f be PartFunc of [:E,F:], G,
      a be Point of E,
      b be Point of F,
      c be Point of G,
      z be Point of [:E,F:],
      A be Subset of E,
      B be Subset of F,
      g be PartFunc of E,F
  st Z is open & dom f = Z
   & A is open & B is open & [:A,B:] c= Z
   & z = [a,b] & f.(a,b) = c
   & f is_differentiable_in z
   & dom g = A & rng g c= B & a in A
   & g.a = b
   & g is_continuous_in a
   & ( for x be Point of E st x in A holds f.(x,g.x) = c )
   & partdiff`2(f,z) is invertible
  holds
     g is_differentiable_in a
   & diff(g,a) = - ( Inv partdiff`2(f,z)) * partdiff`1(f,z);

theorem :: NDIFF_9:20
  for E be RealNormSpace,
      G,F be non trivial RealBanachSpace,
      Z be Subset of [:E,F:],
      f be PartFunc of [:E,F:], G,
      c be Point of G,
      A be Subset of E,
      B be Subset of F,
      g be PartFunc of E,F
  st Z is open & dom f = Z
   & A is open & B is open & [:A,B:] c= Z
   & f is_differentiable_on Z
   & f `| Z is_continuous_on Z
   & dom g = A & rng g c= B
   & g is_continuous_on A
   & ( for x be Point of E st x in A holds f.(x,g.x) = c )
   & ( for x be Point of E, z be Point of [:E,F:]
        st x in A & z =[x,g.x]
       holds partdiff`2(f,z) is invertible )
  holds
     g is_differentiable_on A
   & g `| A is_continuous_on A
   & for x be Point of E,
         z be Point of [:E,F:]
      st x in A & z =[x,g.x]
     holds diff(g,x) = - (Inv partdiff`2(f,z)) * partdiff`1(f,z);

theorem :: NDIFF_9:21
  for E be RealNormSpace,
      G,F be non trivial RealBanachSpace,
      Z be Subset of [:E,F:],
      f be PartFunc of [:E,F:], G,
      a be Point of E,
      b be Point of F,
      c be Point of G,
      z be Point of [:E,F:]
  st Z is open & dom f = Z
   & f is_differentiable_on Z
   & f `| Z is_continuous_on Z
   & [a,b] in Z & f.(a,b) = c
   & z = [a,b]
   & partdiff`2(f,z) is invertible
  holds
    ex r1,r2 be Real
    st 0 < r1 & 0 < r2
     & [:Ball(a,r1),cl_Ball(b,r2):] c= Z
     & ( for x be Point of E st x in Ball(a,r1) holds
         ex y be Point of F
         st y in Ball(b,r2) & f.(x,y) = c )
     & ( for x be Point of E st x in Ball(a,r1) holds
         for y1,y2 be Point of F
         st y1 in Ball(b,r2) & y2 in Ball(b,r2)
          & f.(x,y1) =c & f.(x,y2)= c
         holds y1=y2 )
     & ( ex g be PartFunc of E,F
         st dom g = Ball(a,r1) & rng g c= Ball(b,r2)
          & g is_continuous_on Ball(a,r1)
          & g.a = b
          & ( for x be Point of E st x in Ball(a,r1)
              holds f.(x,g.x) = c )
          & g is_differentiable_on Ball(a,r1)
          & g `| Ball(a,r1) is_continuous_on Ball(a,r1)
          & ( for x be Point of E, z be Point of [:E,F:]
              st x in Ball(a,r1) & z = [x,g.x]
              holds diff(g,x) = - ( Inv partdiff`2(f,z)) * partdiff`1(f,z) )
          & ( for x be Point of E, z be Point of [:E,F:]
              st x in Ball(a,r1) & z =[x,g.x]
              holds partdiff`2(f,z) is invertible ) )
     & ( for g1,g2 be PartFunc of E,F
         st dom g1 = Ball(a,r1)
          & rng g1 c= Ball(b,r2)
          & ( for x be Point of E st x in Ball(a,r1)
              holds f.(x,g1.x) = c )
          & dom g2 = Ball(a,r1)
          & rng g2 c= Ball(b,r2)
          & ( for x be Point of E st x in Ball(a,r1)
              holds f.(x,g2.x) = c )
         holds g1 = g2);