:: Isometric Differentiable Functions on Real Normed Space
:: by Yuichi Futa , Noboru Endou and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-2017 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, MAZURULM,
LOPBAN_1, PRVECT_3, FUNCOP_1, VALUED_1, XTUPLE_0, FUNCT_7;
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;