:: Implicit Function Theorem -- Part {I}
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: Received November 29, 2017
:: Copyright (c) 2017-2018 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, XXREAL_1, FINSEQ_2, RELAT_1, LOPBAN_1, RCOMP_1,
MSSUBFAM, SQUARE_1, TARSKI, ARYTM_3, VALUED_1, 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, NORMSP_2, METRIC_1,
POWER, COMPLEX1, LOPBAN_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, COMPLEX1, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_2, POWER,
STRUCT_0, PRE_TOPC, RLVECT_1, VECTSP_1, NORMSP_0, NORMSP_1, VFUNCT_1,
EUCLID, LOPBAN_1, LOPBAN_2, NFCONT_1, LOPBAN_5, NDIFF_1, NDIFF_2,
NORMSP_2, PRVECT_3, NDIFF_5, NDIFF_7;
constructors SQUARE_1, SEQ_2, NFCONT_1, VFUNCT_1, COMSEQ_2, NDIFF_1, RELSET_1,
NAT_D, SERIES_1, RSSPACE3, LOPBAN_3, NDIFF_5, NDIFF_2, DOMAIN_1,
LOPBAN_5, PCOMPS_1, NDIFF_7, NORMSP_2;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_0,
VALUED_1, FINSEQ_2, FUNCT_2, NUMBERS, XBOOLE_0, RELAT_1, ORDINAL1,
LOPBAN_1, PRVECT_3, XXREAL_0, NORMSP_0, NAT_1, NORMSP_1, SQUARE_1,
XTUPLE_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
begin :: 1. Properties of Lipschitz continuous linear function
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_8:1
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:]
st z = [x,y]
holds ||.z.|| = sqrt (||.x.|| ^2 + ||.y.|| ^2);
theorem :: NDIFF_8:2
for X,Y be RealNormSpace,
x be Point of X,
z be Point of [:X,Y:]
st z = [x,0.Y]
holds ||.z.|| = ||.x.||;
theorem :: NDIFF_8:3
for X,Y be RealNormSpace,
y be Point of Y,
z be Point of [:X,Y:]
st z = [0.X,y]
holds ||.z.|| = ||.y.||;
theorem :: NDIFF_8:4
for X,Y,Z,W be RealNormSpace
for f be Lipschitzian LinearOperator of Z,W,
g be Lipschitzian LinearOperator of Y,Z,
h be Lipschitzian LinearOperator of X,Y
holds f*(g*h) = (f*g)*h;
theorem :: NDIFF_8:5
for X,Y,Z be RealNormSpace
for g be Lipschitzian LinearOperator of X,Y,
f be Lipschitzian LinearOperator of Y,Z,
h be Lipschitzian LinearOperator of X,Z
holds h = f*g iff for x be VECTOR of X holds h.x = f.(g.x);
theorem :: NDIFF_8:6
for X,Y be RealNormSpace for f be Lipschitzian LinearOperator of X,Y
holds f * (id the carrier of X) = f & (id the carrier of Y) * f = f;
theorem :: NDIFF_8:7
for X,Y,Z,W be RealNormSpace
for f be Element of BoundedLinearOperators(Z,W),
g be Element of BoundedLinearOperators(Y,Z),
h be Element of BoundedLinearOperators(X,Y)
holds f*(g*h) = (f*g)*h;
theorem :: NDIFF_8:8
for X,Y be RealNormSpace for f be Element of BoundedLinearOperators
(X,Y) holds f * FuncUnit(X) = f & FuncUnit(Y) * f = f;
theorem :: NDIFF_8:9
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g,h be Element of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds f * (g + h) = f*g + f*h;
theorem :: NDIFF_8:10
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(X,Y),
g,h be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds (g + h) * f = g*f + h*f;
theorem :: NDIFF_8:11
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g be Element of R_NormSpace_of_BoundedLinearOperators(X,Y)
for a,b be Real holds (a*b) * (f*g) = (a*f) * (b*g);
theorem :: NDIFF_8:12
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g be Element of R_NormSpace_of_BoundedLinearOperators(X,Y)
for a be Real
holds a*(f*g) = (a*f)*g;
begin :: 2. Properties of open and closed sets in Banach space
definition
let M be RealNormSpace, p be Element of M, r be Real;
func cl_Ball(p,r) -> Subset of M equals
:: NDIFF_8:def 1
{q where q is Element of M : ||.p - q.|| <= r};
end;
theorem :: NDIFF_8:13
for p be Element of S, r be Real st 0 < r holds
p in Ball(p,r) & p in cl_Ball(p,r);
theorem :: NDIFF_8:14
for p be Element of S, r be Real st 0 < r holds
Ball(p,r) <> {} & cl_Ball(p,r) <> {};
theorem :: NDIFF_8:15
for M be RealNormSpace, p be Element of M, r1,r2 be Real
st r1 <= r2 holds
cl_Ball(p,r1) c= cl_Ball(p,r2)
& Ball(p,r1) c= cl_Ball(p,r2)
& Ball(p,r1) c= Ball(p,r2);
theorem :: NDIFF_8:16
for M be RealNormSpace, p be Element of M, r1,r2 be Real
st r1 < r2 holds
cl_Ball(p,r1) c= Ball(p,r2);
theorem :: NDIFF_8:17
for p be Element of S, r be Real holds
Ball(p,r) = {y where y is Point of S: ||.y - p.|| < r};
theorem :: NDIFF_8:18
for p be Element of S, r be Real holds
cl_Ball(p,r) = {y where y is Point of S: ||.y - p.|| <= r};
theorem :: NDIFF_8:19
for p be Element of S, r be Real st 0 < r
holds Ball(p,r) is Neighbourhood of p;
registration let X be RealNormSpace, x be Point of X, r be Real;
cluster Ball(x,r) -> open;
cluster cl_Ball(x,r) -> closed;
end;
theorem :: NDIFF_8:20
for X be RealNormSpace, V be Subset of X holds V is open
iff for x be Point of X st x in V ex r be Real st r>0 & Ball(x,r) c= V;
theorem :: NDIFF_8:21
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:]
st z = [x,y]
holds ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.||;
theorem :: NDIFF_8:22
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:],
r1 be Real
st 0 < r1 & z = [x,y]
holds
ex r2 be Real
st 0 < r2 & r2 < r1 & [:Ball(x,r2),Ball(y,r2):] c= Ball(z,r1);
theorem :: NDIFF_8:23
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
V be Subset of [:X,Y:]
st V is open & [x,y] in V
ex r be Real st 0 < r & [:Ball(x,r),Ball(y,r):] c= V;
theorem :: NDIFF_8:24
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
V be Subset of [:X,Y:],
r be Real
st V = [:Ball(x,r),Ball(y,r):]
holds V is open;
theorem :: NDIFF_8:25
for E,F be RealNormSpace,
Q be LinearOperator of E,F,
v be Point of E
st Q is one-to-one
holds Q.v = 0.F iff v = 0.E;
theorem :: NDIFF_8:26
for E be RealNormSpace,
X,Y be Subset of E,
v be Point of E
st X is open
& Y = {x+v where x is Point of E : x in X}
holds Y is open;
theorem :: NDIFF_8:27
for E be RealNormSpace,
X,Y be Subset of E,
v be Point of E
st X is open & Y = {x-v where x is Point of E : x in X}
holds Y is open;
begin :: 3. Existence and uniqueness of continuous implicit function
theorem :: NDIFF_8:28
for X be RealBanachSpace,
S be non empty Subset of X,
f be PartFunc of X,X
st S is closed & dom f = S & rng f c= S
& ex k be Real
st 0 < k < 1
& for x,y be Point of X st x in S & y in S
holds ||. f/.x - f/.y .|| <= k * ||.x-y.||
holds
(ex x0 be Point of X st x0 in S & f.x0 = x0)
&(for x0,y0 be Point of X st x0 in S & y0 in S & f.x0 = x0 & f.y0 = y0
holds x0 = y0);
theorem :: NDIFF_8:29
for E be RealNormSpace,
F be RealBanachSpace,
E0 be non empty Subset of E,
F0 be non empty Subset of F,
Fai be PartFunc of [:E,F:],F
st F0 is closed
& [:E0,F0:] c= dom Fai
& (for x be Point of E, y be Point of F
st x in E0 & y in F0
holds Fai.(x,y) in F0)
& (for y be Point of F st y in F0 holds
for x0 be Point of E st x0 in E0
for e be Real st 0 < e
ex d be Real
st 0 < d
& for x1 be Point of E
st x1 in E0
& ||.x1-x0.|| < d
holds ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e )
& ex k be Real
st 0 < k & k < 1
& (for x be Point of E st x in E0 holds
for y1,y2 be Point of F st y1 in F0 & y2 in F0
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= k * ||.y1-y2.||)
holds
(for x be Point of E st x in E0
holds
(ex y be Point of F st y in F0 & Fai.(x,y) = y)
& (for y1,y2 be Point of F
st y1 in F0 & y2 in F0 & Fai.(x,y1) = y1 & Fai.(x,y2) = y2
holds y1 = y2))
& (for x0 be Point of E, y0 be Point of F
st x0 in E0 & y0 in F0 & Fai.(x0,y0) = y0
holds
(for e be Real st 0 < e holds
ex d be Real
st 0 < d
& (for x1 be Point of E, y1 be Point of F
st x1 in E0 & y1 in F0 & Fai.(x1,y1) = y1
& ||.x1-x0.|| < d
holds ||.y1-y0.|| < e)));
theorem :: NDIFF_8:30
for E be RealNormSpace,
F be RealBanachSpace,
A be non empty Subset of E,
B be non empty Subset of F,
Fai be PartFunc of [:E,F:],F
st B is closed
& [:A,B:] c= dom Fai
& (for x be Point of E, y be Point of F
st x in A & y in B holds Fai.(x,y) in B )
& (for y be Point of F st y in B holds
for x0 be Point of E st x0 in A
for e be Real st 0 < e
ex d be Real
st 0 < d
& for x1 be Point of E
st x1 in A & ||.x1-x0.|| < d
holds ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e)
& ex k be Real
st 0 < k & k < 1
& (for x be Point of E st x in A holds
for y1,y2 be Point of F st y1 in B & y2 in B
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= k * ||.y1-y2.||)
holds
(ex g be PartFunc of E,F
st g is_continuous_on A
& dom g = A & rng g c= B
& for x be Point of E st x in A
holds Fai.(x,g.x) = g.x)
&(for g1,g2 be PartFunc of E,F
st dom g1 = A & rng g1 c= B
& dom g2 = A & rng g2 c= B
&(for x be Point of E st x in A holds Fai.(x,g1.x) = g1.x)
&(for x be Point of E st x in A holds Fai.(x,g2.x) = g2.x)
holds g1=g2);
theorem :: NDIFF_8:31
for E,F be RealNormSpace,
s1,s2 be Point of [:E,F:]
st s1`2 = s2`2
holds reproj1 s1 = reproj1 s2;
theorem :: NDIFF_8:32
for E,F be RealNormSpace,
s1,s2 be Point of [:E,F:]
st s1`1 = s2`1
holds reproj2 s1 = reproj2 s2;
theorem :: NDIFF_8:33
for E be RealNormSpace,
r be Real,
z,y1,y2 be Point of E
st y1 in cl_Ball(z,r) & y2 in cl_Ball(z,r)
holds [.y1,y2.] c= cl_Ball(z,r);
theorem :: NDIFF_8:34
for E be RealNormSpace,
x,b be Point of E,
N be Neighbourhood of x holds
{z-b where z is Point of E: z in N} is Neighbourhood of x-b &
{z+b where z is Point of E: z in N} is Neighbourhood of x+b;
theorem :: NDIFF_8:35
for E,G be RealNormSpace,
F be 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_continuous_on Z
& f is_partial_differentiable_on`2 Z
& f `partial`2|Z is_continuous_on Z
& z = [a,b] & z in Z
& f.(a,b) = c
& partdiff`2(f,z) is one-to-one
& partdiff`2(f,z)" is Lipschitzian LinearOperator of G,F
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 cl_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 cl_Ball(b,r2) & y2 in cl_Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c
holds y1 = y2))
& (ex g be PartFunc of E,F
st g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= cl_Ball(b,r2)
& g.a = b
& for x be Point of E st x in Ball(a,r1)
holds f.(x,g.x) = c )
& (for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= cl_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= cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g2.x) = c)
holds g1=g2);
theorem :: NDIFF_8:36
for E,G be RealNormSpace,
F be 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_continuous_on Z
& f is_partial_differentiable_on`2 Z
& f `partial`2|Z is_continuous_on Z
& z = [a,b] & z in Z
& f.(a,b) = c
& partdiff`2(f,z) is one-to-one
& partdiff`2(f,z)" is Lipschitzian LinearOperator of G,F
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 g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= Ball(b,r2)
& g.a = b
& for x be Point of E st x in Ball(a,r1) holds f.(x,g.x) = c )
& (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);