:: Isometric Differentiable Functions on Real Normed Space :: by Yuichi Futa , Noboru Endou and Yasunari Shidama :: :: Received December 31, 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, FUNCT_4, NAT_1, FDIFF_1, SUBSET_1, SEQ_4, RELAT_1, LOPBAN_1, RCOMP_1, TARSKI, ARYTM_3, FUNCT_7, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, VALUED_0, XXREAL_0, GROUP_2, FUNCOP_1, XBOOLE_0, CARD_3, FINSEQ_1, RLVECT_1, PDIFF_1, PRVECT_1, PRVECT_2, CFCONT_1, VECTMETR, NDIFF_7, MCART_1; notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_4, CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, MEMBERED, VALUED_0, COMPLEX1, NAT_D, XXREAL_2, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_2, RVSUM_1, RFINSEQ, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, RFINSEQ2, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, VFUNCT_1, MONOID_0, RLTOPSP1, EUCLID, LOPBAN_1, PRVECT_1, NFCONT_1, NDIFF_1, MAZURULM, NDIFF_2, PRVECT_2, NFCONT_3, PRVECT_3, NDIFF_3, FUNCT_7, NDIFF_5; constructors REAL_1, SQUARE_1, SEQ_2, FDIFF_1, NFCONT_1, RSSPACE, VFUNCT_1, NDIFF_1, RELSET_1, FINSEQ_7, NAT_D, RFINSEQ2, SEQ_4, FCONT_1, NFCONT_3, NDIFF_3, FUNCT_4, NDIFF_5, PRVECT_3, NDIFF_2, MAZURULM, LOPBAN_1, DOMAIN_1, RCOMP_1; registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, NDIFF_1, FUNCT_2, NUMBERS, XBOOLE_0, PRVECT_2, FINSEQ_1, RELAT_1, LOPBAN_1, PRVECT_3, FUNCOP_1, VALUED_1, XTUPLE_0, FUNCT_7, PRVECT_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Preliminaries 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_7:1 for X be set, I,f be Function holds (f|X)*I = (f*I) | I"X; theorem :: NDIFF_7:2 for S, T be RealNormSpace, L be LinearOperator of S, T, x, y be Point of S holds L.x - L.y = L.(x-y); theorem :: NDIFF_7:3 for X, Y, W be RealNormSpace, I be Function of X, Y, f1, f2 be PartFunc of Y, W holds (f1+f2)*I = f1*I+f2*I & (f1-f2)*I = f1*I-f2*I; theorem :: NDIFF_7:4 for X, Y, W be RealNormSpace, I be Function of X, Y, f be PartFunc of Y, W, r be Real holds r(#)(f*I) = (r(#)f)*I; theorem :: NDIFF_7:5 for f be PartFunc of T, W, g be Function of S, T, x be Point of S st x in dom g & g/.x in dom f & g is_continuous_in x & f is_continuous_in g/.x holds f*g is_continuous_in x; definition let X, Y be RealNormSpace; let x be Element of [:X,Y:]; func reproj1(x) -> Function of X,[:X,Y:] means :: NDIFF_7:def 1 for r being Element of X holds it . r = [r,x`2]; func reproj2(x) -> Function of Y,[:X,Y:] means :: NDIFF_7:def 2 for r being Element of Y holds it . r = [x`1,r]; end; begin :: Isometries theorem :: NDIFF_7:6 for I be LinearOperator of S,T, x be Point of S st I is isometric holds I is_continuous_in x; theorem :: NDIFF_7:7 for S, T be RealNormSpace, f be LinearOperator of S, T holds f is isometric iff for x being Element of S holds ||. f.x .|| = ||. x .||; theorem :: NDIFF_7:8 for I be LinearOperator of S,T, Z be Subset of S st I is isometric holds I is_continuous_on Z; theorem :: NDIFF_7:9 for I be LinearOperator of S, T st I is one-to-one onto isometric holds ex J be LinearOperator of T, S st J = I" & J is one-to-one onto isometric; theorem :: NDIFF_7:10 for I be LinearOperator of S, T, s1 being sequence of S st I is isometric & s1 is convergent holds I*s1 is convergent & lim (I*s1) = I.lim s1; theorem :: NDIFF_7:11 for I be LinearOperator of S, T, s1 being sequence of S st I is one-to-one onto isometric holds ( s1 is convergent iff I*s1 is convergent ); theorem :: NDIFF_7:12 for I be LinearOperator of S, T, Z be Subset of S st I is one-to-one onto isometric holds (Z is closed iff I.:Z is closed); theorem :: NDIFF_7:13 for I be LinearOperator of S, T, Z be Subset of S st I is one-to-one onto isometric holds (Z is open iff I.:Z is open); theorem :: NDIFF_7:14 for I be LinearOperator of S, T, Z be Subset of S st I is one-to-one onto isometric holds (Z is compact iff I.:Z is compact); theorem :: NDIFF_7:15 for f be PartFunc of T, W, I be LinearOperator of S, T st I is one-to-one onto isometric holds for x be Point of S st I.x in dom f holds f*I is_continuous_in x iff f is_continuous_in I.x; theorem :: NDIFF_7:16 for f be PartFunc of T, W, I be LinearOperator of S, T, X be set st X c= the carrier of T & I is one-to-one onto isometric holds f is_continuous_on X iff f*I is_continuous_on I"X; definition let X, Y be RealNormSpace; func IsoCPNrSP(X,Y) -> LinearOperator of [:X,Y:],product <*X,Y*> means :: NDIFF_7:def 3 for x be Point of X, y be Point of Y holds it.(x,y) = <*x,y*>; end; theorem :: NDIFF_7:17 for X, Y be RealNormSpace holds 0.product <*X,Y*> = IsoCPNrSP(X,Y).(0.[:X,Y:]); registration let X, Y be RealNormSpace; cluster IsoCPNrSP(X,Y) -> one-to-one onto isometric; end; registration let X, Y be RealNormSpace; cluster one-to-one onto isometric for LinearOperator of [:X,Y:],product <*X,Y*>; end; definition let X, Y be RealNormSpace; let f be one-to-one onto isometric LinearOperator of [:X,Y:],product <*X,Y*>; redefine func f" -> LinearOperator of product <*X,Y*>,[:X,Y:]; end; registration let X, Y be RealNormSpace; let f be one-to-one onto isometric LinearOperator of [:X,Y:],product <*X,Y*>; cluster f" -> one-to-one onto isometric for LinearOperator of product <*X,Y*>,[:X,Y:]; end; registration let X, Y be RealNormSpace; cluster one-to-one onto isometric for LinearOperator of product <*X,Y*>,[:X,Y:]; end; theorem :: NDIFF_7:18 for X, Y be RealNormSpace, x be Point of X, y be Point of Y holds (IsoCPNrSP(X,Y)").<*x,y*> = [x,y]; theorem :: NDIFF_7:19 for X, Y be RealNormSpace holds (IsoCPNrSP(X,Y)").(0. product <*X,Y*>) = 0.[:X,Y:]; theorem :: NDIFF_7:20 for X, Y be RealNormSpace, Z be Subset of [:X,Y:] holds IsoCPNrSP(X,Y) is_continuous_on Z; theorem :: NDIFF_7:21 for X, Y be RealNormSpace, Z be Subset of product <*X,Y*> holds IsoCPNrSP(X,Y)" is_continuous_on Z; theorem :: NDIFF_7:22 for S, T, W be RealNormSpace, f be Point of R_NormSpace_of_BoundedLinearOperators(S,W), g be Point of R_NormSpace_of_BoundedLinearOperators(T,W), I be LinearOperator of S, T st I is one-to-one onto isometric & f = g*I holds ||.f.|| = ||.g.||; registration let S, T; cluster isometric -> Lipschitzian for LinearOperator of S, T; end; begin :: Isometric Differentiable Functions on Real Normed Space theorem :: NDIFF_7:23 for G be RealNormSpace-Sequence, F be RealNormSpace, i be set, f,g be PartFunc of product G,F, X be Subset of product G st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds f+g is_partial_differentiable_on X,i & (f+g) `partial|(X,i) = f `partial|(X,i) + g `partial|(X,i); theorem :: NDIFF_7:24 for G be RealNormSpace-Sequence, F be RealNormSpace, i be set, f,g be PartFunc of product G,F, X be Subset of product G st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds f-g is_partial_differentiable_on X,i & (f-g) `partial|(X,i) = f `partial|(X,i)- g `partial|(X,i); theorem :: NDIFF_7:25 for G be RealNormSpace-Sequence, F be RealNormSpace, i be set, f be PartFunc of product G,F, r be Real, X be Subset of product G st X is open & i in dom G & f is_partial_differentiable_on X,i holds r(#)f is_partial_differentiable_on X,i & (r(#)f) `partial|(X,i) = r(#)(f `partial|(X,i)); theorem :: NDIFF_7:26 for S, T be RealNormSpace, L be Lipschitzian LinearOperator of S, T, x0 be Point of S holds L is_differentiable_in x0 & diff(L,x0) = L; theorem :: NDIFF_7:27 for f be PartFunc of T, W, I be Lipschitzian LinearOperator of S, T, I0 be Point of R_NormSpace_of_BoundedLinearOperators(S,T) st I0 = I holds for x be Point of S st f is_differentiable_in I.x holds f*I is_differentiable_in x & diff(f*I,x) = diff(f,I.x)*I0; theorem :: NDIFF_7:28 for f be PartFunc of T, W, I be LinearOperator of S, T st I is one-to-one onto & I is isometric holds for x be Point of S holds f*I is_differentiable_in x iff f is_differentiable_in I.x; theorem :: NDIFF_7:29 for f be PartFunc of T, W, I be LinearOperator of S, T, X be set st X c= the carrier of T & I is one-to-one onto & I is isometric holds f is_differentiable_on X iff f*I is_differentiable_on I"X; theorem :: NDIFF_7:30 for X, Y be RealNormSpace, f be PartFunc of product <*X,Y*>, W, D be Subset of product <*X,Y*> st f is_differentiable_on D holds for z be Point of product <*X,Y*> st z in dom (f`| D ) holds (f`| D ).z = ((f*IsoCPNrSP(X,Y) `| (IsoCPNrSP(X,Y))"D) /.((IsoCPNrSP(X,Y)").z)) *(IsoCPNrSP(X,Y)"); theorem :: NDIFF_7:31 for X, Y be RealNormSpace, f be PartFunc of [:X,Y:], W, D be Subset of [:X,Y:] st f is_differentiable_on D holds for z be Point of [:X,Y:] st z in dom (f`| D ) holds (f`| D ).z = ((f*(IsoCPNrSP(X,Y)") `| ((IsoCPNrSP(X,Y)"))"D) /.(IsoCPNrSP(X,Y).z)) *(IsoCPNrSP(X,Y)")"; theorem :: NDIFF_7:32 for X,Y be RealNormSpace, z be Point of [:X,Y:] holds reproj1(z) = (IsoCPNrSP(X,Y)") * reproj(In(1,dom <*X,Y*>),IsoCPNrSP(X,Y).z) & reproj2(z) = (IsoCPNrSP(X,Y)") * reproj(In(2,dom <*X,Y*>),IsoCPNrSP(X,Y).z); definition let X, Y be RealNormSpace, z be Point of [:X,Y:]; redefine func z`1 -> Point of X; redefine func z`2 -> Point of Y; end; definition let X, Y, W be RealNormSpace, z be Point of [:X,Y:], f be PartFunc of [:X,Y:], W; pred f is_partial_differentiable_in`1 z means :: NDIFF_7:def 4 f*reproj1(z) is_differentiable_in z`1; pred f is_partial_differentiable_in`2 z means :: NDIFF_7:def 5 f*reproj2(z) is_differentiable_in z`2; end; theorem :: NDIFF_7:33 for X, Y be RealNormSpace, z be Point of [:X,Y:] holds z`1 = proj(In(1,dom<*X,Y*>)).(IsoCPNrSP(X,Y).z) & z`2 = proj(In(2,dom<*X,Y*>)).(IsoCPNrSP(X,Y).z); theorem :: NDIFF_7:34 for X, Y, W be RealNormSpace, z be Point of [:X,Y:], f be PartFunc of [:X,Y:], W holds (f is_partial_differentiable_in`1 z iff f*(IsoCPNrSP(X,Y)") is_partial_differentiable_in IsoCPNrSP(X,Y).z,1 ) & (f is_partial_differentiable_in`2 z iff f*(IsoCPNrSP(X,Y)") is_partial_differentiable_in IsoCPNrSP(X,Y).z,2 ); definition let X, Y, W be RealNormSpace, z be Point of [:X,Y:], f be PartFunc of [:X,Y:], W; func partdiff`1(f,z) -> Point of R_NormSpace_of_BoundedLinearOperators(X,W) equals :: NDIFF_7:def 6 diff(f*reproj1(z),z`1); func partdiff`2(f,z) -> Point of R_NormSpace_of_BoundedLinearOperators(Y,W) equals :: NDIFF_7:def 7 diff(f*reproj2(z),z`2); end; theorem :: NDIFF_7:35 for X, Y, W be RealNormSpace, z be Point of [:X,Y:], f be PartFunc of [:X,Y:], W holds partdiff`1(f,z) = partdiff(f*(IsoCPNrSP(X,Y)"),IsoCPNrSP(X,Y).z,1) & partdiff`2(f,z) = partdiff(f*(IsoCPNrSP(X,Y)"),IsoCPNrSP(X,Y).z,2); theorem :: NDIFF_7:36 for X, Y, W be RealNormSpace, z be Point of [:X,Y:], f1, f2 be PartFunc of [:X,Y:], W st f1 is_partial_differentiable_in`1 z & f2 is_partial_differentiable_in`1 z holds (f1+f2) is_partial_differentiable_in`1 z & partdiff`1(f1+f2,z) = partdiff`1(f1,z)+partdiff`1(f2,z) & (f1-f2) is_partial_differentiable_in`1 z & partdiff`1(f1-f2,z) = partdiff`1(f1,z)-partdiff`1(f2,z); theorem :: NDIFF_7:37 for X, Y, W be RealNormSpace, z be Point of [:X,Y:], f1, f2 be PartFunc of [:X,Y:], W st f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z holds (f1+f2) is_partial_differentiable_in`2 z & partdiff`2(f1+f2,z) = partdiff`2(f1,z)+partdiff`2(f2,z) & (f1-f2) is_partial_differentiable_in`2 z & partdiff`2(f1-f2,z) = partdiff`2(f1,z)-partdiff`2(f2,z); theorem :: NDIFF_7:38 for X, Y, W be RealNormSpace, z be Point of [:X,Y:], r be Real, f be PartFunc of [:X,Y:], W st f is_partial_differentiable_in`1 z holds r(#)f is_partial_differentiable_in`1 z & partdiff`1(r(#)f,z) = r*partdiff`1(f,z); theorem :: NDIFF_7:39 for X, Y, W be RealNormSpace, z be Point of [:X,Y:], r be Real, f be PartFunc of [:X,Y:], W st f is_partial_differentiable_in`2 z holds r(#)f is_partial_differentiable_in`2 z & partdiff`2(r(#)f,z) = r*partdiff`2(f,z); definition let X, Y, W be RealNormSpace, Z be set, f be PartFunc of [:X,Y:], W; pred f is_partial_differentiable_on`1 Z means :: NDIFF_7:def 8 Z c= dom f & for z be Point of [:X,Y:] st z in Z holds f|Z is_partial_differentiable_in`1 z; pred f is_partial_differentiable_on`2 Z means :: NDIFF_7:def 9 Z c= dom f & for z be Point of [:X,Y:] st z in Z holds f|Z is_partial_differentiable_in`2 z; end; theorem :: NDIFF_7:40 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f be PartFunc of [:X,Y:],W holds (f is_partial_differentiable_on`1 Z iff f*(IsoCPNrSP(X,Y)") is_partial_differentiable_on ((IsoCPNrSP(X,Y)"))"Z,1) & (f is_partial_differentiable_on`2 Z iff f*(IsoCPNrSP(X,Y)") is_partial_differentiable_on ((IsoCPNrSP(X,Y)"))"Z,2); definition let X, Y, W be RealNormSpace, Z be set, f be PartFunc of [:X,Y:], W; assume f is_partial_differentiable_on`1 Z; func f `partial`1|Z -> PartFunc of [:X,Y:], R_NormSpace_of_BoundedLinearOperators (X,W) means :: NDIFF_7:def 10 dom it = Z & for z be Point of [:X,Y:] st z in Z holds it/.z =partdiff`1(f,z); end; definition let X, Y, W be RealNormSpace, Z be set, f be PartFunc of [:X,Y:], W; assume f is_partial_differentiable_on`2 Z; func f `partial`2|Z -> PartFunc of [:X,Y:], R_NormSpace_of_BoundedLinearOperators (Y,W) means :: NDIFF_7:def 11 dom it = Z & for z be Point of [:X,Y:] st z in Z holds it/.z =partdiff`2(f,z); end; theorem :: NDIFF_7:41 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f be PartFunc of [:X,Y:], W st f is_partial_differentiable_on`1 Z holds f `partial`1|Z = (f*(IsoCPNrSP(X,Y)"))`partial|(((IsoCPNrSP(X,Y)"))"Z,1) *IsoCPNrSP(X,Y); theorem :: NDIFF_7:42 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f be PartFunc of [:X,Y:], W st f is_partial_differentiable_on`2 Z holds f `partial`2|Z = (f*(IsoCPNrSP(X,Y)"))`partial|(((IsoCPNrSP(X,Y)"))"Z,2) *IsoCPNrSP(X,Y); theorem :: NDIFF_7:43 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f be PartFunc of [:X,Y:], W st Z is open holds f is_partial_differentiable_on`1 Z iff Z c= dom f & for x be Point of [:X,Y:] st x in Z holds f is_partial_differentiable_in`1 x; theorem :: NDIFF_7:44 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f be PartFunc of [:X,Y:], W st Z is open holds f is_partial_differentiable_on`2 Z iff Z c= dom f & for x be Point of [:X,Y:] st x in Z holds f is_partial_differentiable_in`2 x; theorem :: NDIFF_7:45 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f,g be PartFunc of [:X,Y:], W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds f+g is_partial_differentiable_on`1 Z & (f+g) `partial`1|Z = f `partial`1|Z+ g `partial`1|Z; theorem :: NDIFF_7:46 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f, g be PartFunc of [:X,Y:], W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds f-g is_partial_differentiable_on`1 Z & (f-g) `partial`1|Z = f `partial`1|Z- g `partial`1|Z; theorem :: NDIFF_7:47 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f, g be PartFunc of [:X,Y:], W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds f+g is_partial_differentiable_on`2 Z & (f+g) `partial`2|Z = f `partial`2|Z+ g `partial`2|Z; theorem :: NDIFF_7:48 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f, g be PartFunc of [:X,Y:], W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds f-g is_partial_differentiable_on`2 Z & (f-g) `partial`2|Z = f `partial`2|Z- g `partial`2|Z; theorem :: NDIFF_7:49 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], r be Real, f be PartFunc of [:X,Y:], W st Z is open & f is_partial_differentiable_on`1 Z holds r(#)f is_partial_differentiable_on`1 Z & (r(#)f) `partial`1|Z = r(#)(f `partial`1|Z); theorem :: NDIFF_7:50 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], r be Real, f be PartFunc of [:X,Y:], W st Z is open & f is_partial_differentiable_on`2 Z holds r(#)f is_partial_differentiable_on`2 Z & (r(#)f) `partial`2|Z = r(#)(f `partial`2|Z); theorem :: NDIFF_7:51 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f be PartFunc of [:X,Y:], W st f is_differentiable_on Z holds f`|Z is_continuous_on Z iff (f*(IsoCPNrSP(X,Y)")) `| ((IsoCPNrSP(X,Y)")"Z) is_continuous_on ((IsoCPNrSP(X,Y)")"Z); theorem :: NDIFF_7:52 for X, Y, W be RealNormSpace, Z be Subset of [:X,Y:], f be PartFunc of [:X,Y:], W st Z is open holds ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1|Z is_continuous_on Z & f `partial`2|Z is_continuous_on Z ) iff f is_differentiable_on Z & f`|Z is_continuous_on Z;