:: Differentiable Functions into Real Normed Spaces
:: by Hiroyuki Okazaki , Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received October 13, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users
begin
reconsider
cs
=
NAT
-->
0
as
Real_Sequence
by
FUNCOP_1:45
;
theorem
Th1
:
:: NDIFF_3:1
for
G
being
RealNormSpace
for
s1
being
Real_Sequence
for
seq
being
sequence
of
G
st ( for
n
being
Element
of
NAT
holds
||.
(
seq
.
n
)
.||
<=
s1
.
n
) &
s1
is
convergent
&
lim
s1
=
0
holds
(
seq
is
convergent
&
lim
seq
=
0.
G
)
proof
end;
theorem
Th2
:
:: NDIFF_3:2
for
G
being
RealNormSpace
for
k
being
Element
of
NAT
for
s1
being
Real_Sequence
for
seq
being
sequence
of
G
holds
(
s1
^\
k
)
(#)
(
seq
^\
k
)
=
(
s1
(#)
seq
)
^\
k
proof
end;
definition
let
F
be non
trivial
RealNormSpace
;
let
IT
be
PartFunc
of
REAL
, the
carrier
of
F
;
attr
IT
is
RestFunc-like
means
:
Def1
:
:: NDIFF_3:def 1
(
IT
is
total
& ( for
h
being
non-zero
0
-convergent
Real_Sequence
holds
(
(
h
"
)
(#)
(
IT
/*
h
)
is
convergent
&
lim
(
(
h
"
)
(#)
(
IT
/*
h
)
)
=
0.
F
) ) );
end;
::
deftheorem
Def1
defines
RestFunc-like
NDIFF_3:def 1 :
for
F
being non
trivial
RealNormSpace
for
IT
being
PartFunc
of
REAL
, the
carrier
of
F
holds
(
IT
is
RestFunc-like
iff (
IT
is
total
& ( for
h
being
non-zero
0
-convergent
Real_Sequence
holds
(
(
h
"
)
(#)
(
IT
/*
h
)
is
convergent
&
lim
(
(
h
"
)
(#)
(
IT
/*
h
)
)
=
0.
F
) ) ) );
registration
let
F
be non
trivial
RealNormSpace
;
cluster
V13
()
V16
(
REAL
)
V17
( the
carrier
of
F
)
Function-like
RestFunc-like
for
Element
of
K6
(
K7
(
REAL
, the
carrier
of
F
));
existence
ex
b
1
being
PartFunc
of
REAL
, the
carrier
of
F
st
b
1
is
RestFunc-like
proof
end;
end;
definition
let
F
be non
trivial
RealNormSpace
;
mode
RestFunc of
F
is
RestFunc-like
PartFunc
of
REAL
, the
carrier
of
F
;
end;
definition
let
F
be non
trivial
RealNormSpace
;
let
IT
be
Function
of
REAL
, the
carrier
of
F
;
attr
IT
is
linear
means
:
Def2
:
:: NDIFF_3:def 2
ex
r
being
Point
of
F
st
for
p
being
Real
holds
IT
.
p
=
p
*
r
;
end;
::
deftheorem
Def2
defines
linear
NDIFF_3:def 2 :
for
F
being non
trivial
RealNormSpace
for
IT
being
Function
of
REAL
, the
carrier
of
F
holds
(
IT
is
linear
iff ex
r
being
Point
of
F
st
for
p
being
Real
holds
IT
.
p
=
p
*
r
);
registration
let
F
be non
trivial
RealNormSpace
;
cluster
V1
()
V13
()
V16
(
REAL
)
V17
( the
carrier
of
F
)
Function-like
total
quasi_total
linear
for
Element
of
K6
(
K7
(
REAL
, the
carrier
of
F
));
existence
ex
b
1
being
Function
of
REAL
, the
carrier
of
F
st
b
1
is
linear
proof
end;
end;
definition
let
F
be non
trivial
RealNormSpace
;
mode
LinearFunc of
F
is
linear
Function
of
REAL
, the
carrier
of
F
;
end;
theorem
Th3
:
:: NDIFF_3:3
for
F
being non
trivial
RealNormSpace
for
L1
,
L2
being
LinearFunc
of
F
holds
(
L1
+
L2
is
LinearFunc
of
F
&
L1
-
L2
is
LinearFunc
of
F
)
proof
end;
theorem
Th4
:
:: NDIFF_3:4
for
F
being non
trivial
RealNormSpace
for
r
being
Real
for
L
being
LinearFunc
of
F
holds
r
(#)
L
is
LinearFunc
of
F
proof
end;
theorem
Th5
:
:: NDIFF_3:5
for
F
being non
trivial
RealNormSpace
for
h1
,
h2
being
PartFunc
of
REAL
, the
carrier
of
F
for
seq
being
Real_Sequence
st
rng
seq
c=
(
dom
h1
)
/\
(
dom
h2
)
holds
(
(
h1
+
h2
)
/*
seq
=
(
h1
/*
seq
)
+
(
h2
/*
seq
)
&
(
h1
-
h2
)
/*
seq
=
(
h1
/*
seq
)
-
(
h2
/*
seq
)
)
proof
end;
theorem
Th6
:
:: NDIFF_3:6
for
F
being non
trivial
RealNormSpace
for
h1
,
h2
being
PartFunc
of
REAL
, the
carrier
of
F
for
seq
being
Real_Sequence
st
h1
is
total
&
h2
is
total
holds
(
(
h1
+
h2
)
/*
seq
=
(
h1
/*
seq
)
+
(
h2
/*
seq
)
&
(
h1
-
h2
)
/*
seq
=
(
h1
/*
seq
)
-
(
h2
/*
seq
)
)
proof
end;
theorem
Th7
:
:: NDIFF_3:7
for
F
being non
trivial
RealNormSpace
for
R1
,
R2
being
RestFunc
of
F
holds
(
R1
+
R2
is
RestFunc
of
F
&
R1
-
R2
is
RestFunc
of
F
)
proof
end;
theorem
Th8
:
:: NDIFF_3:8
for
F
being non
trivial
RealNormSpace
for
r
being
Real
for
R
being
RestFunc
of
F
holds
r
(#)
R
is
RestFunc
of
F
proof
end;
definition
let
F
be non
trivial
RealNormSpace
;
let
f
be
PartFunc
of
REAL
, the
carrier
of
F
;
let
x0
be
real
number
;
pred
f
is_differentiable_in
x0
means
:
Def3
:
:: NDIFF_3:def 3
ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
of
F
ex
R
being
RestFunc
of
F
st
for
x
being
Real
st
x
in
N
holds
(
f
/.
x
)
-
(
f
/.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
/.
(
x
-
x0
)
)
);
end;
::
deftheorem
Def3
defines
is_differentiable_in
NDIFF_3:def 3 :
for
F
being non
trivial
RealNormSpace
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
for
x0
being
real
number
holds
(
f
is_differentiable_in
x0
iff ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
of
F
ex
R
being
RestFunc
of
F
st
for
x
being
Real
st
x
in
N
holds
(
f
/.
x
)
-
(
f
/.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
/.
(
x
-
x0
)
)
) );
definition
let
F
be non
trivial
RealNormSpace
;
let
f
be
PartFunc
of
REAL
, the
carrier
of
F
;
let
x0
be
real
number
;
assume
A1
:
f
is_differentiable_in
x0
;
func
diff
(
f
,
x0
)
->
Point
of
F
means
:
Def4
:
:: NDIFF_3:def 4
ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
of
F
ex
R
being
RestFunc
of
F
st
(
it
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
/.
x
)
-
(
f
/.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
/.
(
x
-
x0
)
)
) ) );
existence
ex
b
1
being
Point
of
F
ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
of
F
ex
R
being
RestFunc
of
F
st
(
b
1
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
/.
x
)
-
(
f
/.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
/.
(
x
-
x0
)
)
) ) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Point
of
F
st ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
of
F
ex
R
being
RestFunc
of
F
st
(
b
1
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
/.
x
)
-
(
f
/.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
/.
(
x
-
x0
)
)
) ) ) & ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
of
F
ex
R
being
RestFunc
of
F
st
(
b
2
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
/.
x
)
-
(
f
/.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
/.
(
x
-
x0
)
)
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def4
defines
diff
NDIFF_3:def 4 :
for
F
being non
trivial
RealNormSpace
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
for
x0
being
real
number
st
f
is_differentiable_in
x0
holds
for
b
4
being
Point
of
F
holds
(
b
4
=
diff
(
f
,
x0
) iff ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
of
F
ex
R
being
RestFunc
of
F
st
(
b
4
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
/.
x
)
-
(
f
/.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
/.
(
x
-
x0
)
)
) ) ) );
definition
let
F
be non
trivial
RealNormSpace
;
let
f
be
PartFunc
of
REAL
, the
carrier
of
F
;
let
X
be
set
;
pred
f
is_differentiable_on
X
means
:
Def5
:
:: NDIFF_3:def 5
(
X
c=
dom
f
& ( for
x
being
Real
st
x
in
X
holds
f
|
X
is_differentiable_in
x
) );
end;
::
deftheorem
Def5
defines
is_differentiable_on
NDIFF_3:def 5 :
for
F
being non
trivial
RealNormSpace
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
for
X
being
set
holds
(
f
is_differentiable_on
X
iff (
X
c=
dom
f
& ( for
x
being
Real
st
x
in
X
holds
f
|
X
is_differentiable_in
x
) ) );
theorem
Th9
:
:: NDIFF_3:9
for
F
being non
trivial
RealNormSpace
for
X
being
set
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
f
is_differentiable_on
X
holds
X
is
Subset
of
REAL
proof
end;
theorem
Th10
:
:: NDIFF_3:10
for
F
being non
trivial
RealNormSpace
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
holds
(
f
is_differentiable_on
Z
iff (
Z
c=
dom
f
& ( for
x
being
Real
st
x
in
Z
holds
f
is_differentiable_in
x
) ) )
proof
end;
theorem
:: NDIFF_3:11
for
F
being non
trivial
RealNormSpace
for
Y
being
Subset
of
REAL
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
f
is_differentiable_on
Y
holds
Y
is
open
proof
end;
definition
let
F
be non
trivial
RealNormSpace
;
let
f
be
PartFunc
of
REAL
, the
carrier
of
F
;
let
X
be
set
;
assume
A1
:
f
is_differentiable_on
X
;
func
f
`|
X
->
PartFunc
of
REAL
, the
carrier
of
F
means
:
Def6
:
:: NDIFF_3:def 6
(
dom
it
=
X
& ( for
x
being
Real
st
x
in
X
holds
it
.
x
=
diff
(
f
,
x
) ) );
existence
ex
b
1
being
PartFunc
of
REAL
, the
carrier
of
F
st
(
dom
b
1
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
1
.
x
=
diff
(
f
,
x
) ) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of
REAL
, the
carrier
of
F
st
dom
b
1
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
1
.
x
=
diff
(
f
,
x
) ) &
dom
b
2
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
2
.
x
=
diff
(
f
,
x
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def6
defines
`|
NDIFF_3:def 6 :
for
F
being non
trivial
RealNormSpace
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
for
X
being
set
st
f
is_differentiable_on
X
holds
for
b
4
being
PartFunc
of
REAL
, the
carrier
of
F
holds
(
b
4
=
f
`|
X
iff (
dom
b
4
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
4
.
x
=
diff
(
f
,
x
) ) ) );
theorem
:: NDIFF_3:12
for
F
being non
trivial
RealNormSpace
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
Z
c=
dom
f
& ex
r
being
Point
of
F
st
rng
f
=
{
r
}
holds
(
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
f
`|
Z
)
/.
x
=
0.
F
) )
proof
end;
theorem
Th13
:
:: NDIFF_3:13
for
F
being non
trivial
RealNormSpace
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
for
x0
being
real
number
for
N
being
Neighbourhood
of
x0
st
f
is_differentiable_in
x0
&
N
c=
dom
f
holds
for
h
being
non-zero
0
-convergent
Real_Sequence
for
c
being
constant
Real_Sequence
st
rng
c
=
{
x0
}
&
rng
(
h
+
c
)
c=
N
holds
(
(
h
"
)
(#)
(
(
f
/*
(
h
+
c
)
)
-
(
f
/*
c
)
)
is
convergent
&
diff
(
f
,
x0
)
=
lim
(
(
h
"
)
(#)
(
(
f
/*
(
h
+
c
)
)
-
(
f
/*
c
)
)
)
)
proof
end;
theorem
Th14
:
:: NDIFF_3:14
for
F
being non
trivial
RealNormSpace
for
x0
being
Real
for
f1
,
f2
being
PartFunc
of
REAL
, the
carrier
of
F
st
f1
is_differentiable_in
x0
&
f2
is_differentiable_in
x0
holds
(
f1
+
f2
is_differentiable_in
x0
&
diff
(
(
f1
+
f2
)
,
x0
)
=
(
diff
(
f1
,
x0
)
)
+
(
diff
(
f2
,
x0
)
)
)
proof
end;
theorem
Th15
:
:: NDIFF_3:15
for
F
being non
trivial
RealNormSpace
for
x0
being
Real
for
f1
,
f2
being
PartFunc
of
REAL
, the
carrier
of
F
st
f1
is_differentiable_in
x0
&
f2
is_differentiable_in
x0
holds
(
f1
-
f2
is_differentiable_in
x0
&
diff
(
(
f1
-
f2
)
,
x0
)
=
(
diff
(
f1
,
x0
)
)
-
(
diff
(
f2
,
x0
)
)
)
proof
end;
theorem
Th16
:
:: NDIFF_3:16
for
F
being non
trivial
RealNormSpace
for
x0
being
Real
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
for
r
being
Real
st
f
is_differentiable_in
x0
holds
(
r
(#)
f
is_differentiable_in
x0
&
diff
(
(
r
(#)
f
)
,
x0
)
=
r
*
(
diff
(
f
,
x0
)
)
)
proof
end;
theorem
:: NDIFF_3:17
for
F
being non
trivial
RealNormSpace
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
, the
carrier
of
F
st
Z
c=
dom
(
f1
+
f2
)
&
f1
is_differentiable_on
Z
&
f2
is_differentiable_on
Z
holds
(
f1
+
f2
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
+
f2
)
`|
Z
)
.
x
=
(
diff
(
f1
,
x
)
)
+
(
diff
(
f2
,
x
)
)
) )
proof
end;
theorem
:: NDIFF_3:18
for
F
being non
trivial
RealNormSpace
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
, the
carrier
of
F
st
Z
c=
dom
(
f1
-
f2
)
&
f1
is_differentiable_on
Z
&
f2
is_differentiable_on
Z
holds
(
f1
-
f2
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
-
f2
)
`|
Z
)
.
x
=
(
diff
(
f1
,
x
)
)
-
(
diff
(
f2
,
x
)
)
) )
proof
end;
theorem
:: NDIFF_3:19
for
F
being non
trivial
RealNormSpace
for
r
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
Z
c=
dom
(
r
(#)
f
)
&
f
is_differentiable_on
Z
holds
(
r
(#)
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
r
(#)
f
)
`|
Z
)
.
x
=
r
*
(
diff
(
f
,
x
)
)
) )
proof
end;
theorem
:: NDIFF_3:20
for
F
being non
trivial
RealNormSpace
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
Z
c=
dom
f
&
f
|
Z
is
constant
holds
(
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
f
`|
Z
)
.
x
=
0.
F
) )
proof
end;
theorem
Th21
:
:: NDIFF_3:21
for
F
being non
trivial
RealNormSpace
for
r
,
p
being
Point
of
F
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
Z
c=
dom
f
& ( for
x
being
Real
st
x
in
Z
holds
f
/.
x
=
(
x
*
r
)
+
p
) holds
(
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
f
`|
Z
)
.
x
=
r
) )
proof
end;
theorem
Th22
:
:: NDIFF_3:22
for
F
being non
trivial
RealNormSpace
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
for
x0
being
Real
st
f
is_differentiable_in
x0
holds
f
is_continuous_in
x0
proof
end;
theorem
:: NDIFF_3:23
for
F
being non
trivial
RealNormSpace
for
X
being
set
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
f
is_differentiable_on
X
holds
f
|
X
is
continuous
proof
end;
theorem
Th24
:
:: NDIFF_3:24
for
F
being non
trivial
RealNormSpace
for
X
being
set
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
st
f
is_differentiable_on
X
&
Z
c=
X
holds
f
is_differentiable_on
Z
proof
end;
Lm1
:
{}
REAL
is
closed
proof
end;
theorem
:: NDIFF_3:25
for
F
being non
trivial
RealNormSpace
ex
R
being
RestFunc
of
F
st
(
R
/.
0
=
0.
F
&
R
is_continuous_in
0
)
proof
end;
definition
let
F
be non
trivial
RealNormSpace
;
let
f
be
PartFunc
of
REAL
, the
carrier
of
F
;
attr
f
is
differentiable
means
:
Def7
:
:: NDIFF_3:def 7
f
is_differentiable_on
dom
f
;
end;
::
deftheorem
Def7
defines
differentiable
NDIFF_3:def 7 :
for
F
being non
trivial
RealNormSpace
for
f
being
PartFunc
of
REAL
, the
carrier
of
F
holds
(
f
is
differentiable
iff
f
is_differentiable_on
dom
f
);
Lm2
:
[#]
REAL
is
open
proof
end;
registration
let
F
be non
trivial
RealNormSpace
;
cluster
V1
()
V13
()
V16
(
REAL
)
V17
( the
carrier
of
F
)
Function-like
total
quasi_total
differentiable
for
Element
of
K6
(
K7
(
REAL
, the
carrier
of
F
));
existence
ex
b
1
being
Function
of
REAL
, the
carrier
of
F
st
b
1
is
differentiable
proof
end;
end;
theorem
:: NDIFF_3:26
for
F
being non
trivial
RealNormSpace
for
Z
being
open
Subset
of
REAL
for
f
being
differentiable
PartFunc
of
REAL
, the
carrier
of
F
st
Z
c=
dom
f
holds
f
is_differentiable_on
Z
proof
end;