set f = Eval p;
set L = RealVectSpace REAL;
defpred S1[ Nat, object ] means c2 = FPower ((p . (p -' 1)),(p -' 1));
consider G being FinSequence of (RealVectSpace REAL) such that
A2:
dom G = Seg (len p)
and
A3:
for n being Nat st n in Seg (len p) holds
S1[n,G . n]
from FINSEQ_1:sch 5(A1);
A4:
G | (len G) = G
by FINSEQ_1:58;
reconsider SF = Sum G as Function of REAL,REAL by FUNCT_2:66;
A5:
now for x being Element of REAL holds (Eval p) . x = SF . xlet x be
Element of
REAL ;
(Eval p) . x = SF . xreconsider x1 =
x as
Element of
F_Real ;
consider H being
FinSequence of
F_Real such that A6:
eval (
p,
x1)
= Sum H
and A7:
len H = len p
and A8:
for
n being
Element of
NAT st
n in dom H holds
H . n = (p . (n -' 1)) * ((power F_Real) . (x1,(n -' 1)))
by POLYNOM4:def 2;
defpred S2[
Nat]
means for
SFk being
Function of
REAL,
REAL st
SFk = Sum (G | p) holds
Sum (H | p) = SFk . x;
A9:
len G = len p
by A2, FINSEQ_1:def 3;
A10:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
assume A11:
for
SFk being
Function of
REAL,
REAL st
SFk = Sum (G | k) holds
Sum (H | k) = SFk . x
;
S2[k + 1]
reconsider SFk1 =
Sum (G | k) as
Function of
REAL,
REAL by FUNCT_2:66;
let SFk be
Function of
REAL,
REAL;
( SFk = Sum (G | (k + 1)) implies Sum (H | (k + 1)) = SFk . x )
assume A12:
SFk = Sum (G | (k + 1))
;
Sum (H | (k + 1)) = SFk . x
per cases
( len G > k or len G <= k )
;
suppose A13:
len G > k
;
Sum (H | (k + 1)) = SFk . xreconsider g2 =
FPower (
(p . kk),
k) as
Function of
REAL,
REAL ;
A14:
k + 1
>= 1
by NAT_1:11;
A15:
k + 1
<= len G
by A13, NAT_1:13;
then A16:
k + 1
in dom G
by NAT_1:11, FINSEQ_3:25;
then A17:
G /. (k + 1) =
G . (k + 1)
by PARTFUN1:def 6
.=
FPower (
(p . ((k + 1) -' 1)),
((k + 1) -' 1))
by A2, A3, A14, A15, FINSEQ_3:25
.=
FPower (
(p . kk),
((k + 1) -' 1))
by NAT_D:34
.=
FPower (
(p . kk),
k)
by NAT_D:34
;
G | (k + 1) =
(G | k) ^ <*(G . (k + 1))*>
by A13, FINSEQ_5:83
.=
(G | k) ^ <*(G /. (k + 1))*>
by A16, PARTFUN1:def 6
;
then A18:
SFk =
(Sum (G | k)) + (G /. (k + 1))
by A12, FVSUM_1:71
.=
SFk1 + g2
by A17, FUNCSDOM:28
;
A19:
Sum (H | k) = SFk1 . x
by A11;
A20:
dom G = dom H
by A2, A7, FINSEQ_1:def 3;
then A21:
H /. (k + 1) =
H . (k + 1)
by A16, PARTFUN1:def 6
.=
(p . ((k + 1) -' 1)) * ((power F_Real) . (x1,((k + 1) -' 1)))
by A8, A20, A16
.=
(p . kk) * ((power F_Real) . (x1,((k + 1) -' 1)))
by NAT_D:34
.=
(p . kk) * (power (x1,k))
by NAT_D:34
.=
(FPower ((p . kk),k)) . x
by POLYNOM5:def 12
;
H | (k + 1) =
(H | k) ^ <*(H . (k + 1))*>
by A7, A9, A13, FINSEQ_5:83
.=
(H | k) ^ <*(H /. (k + 1))*>
by A20, A16, PARTFUN1:def 6
;
hence Sum (H | (k + 1)) =
(Sum (H | k)) + (H /. (k + 1))
by FVSUM_1:71
.=
SFk . x
by A21, A18, A19, VALUED_1:1
;
verum end;
end; A24:
S2[
0 ]
A27:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A24, A10);
A28:
Sum (G | (len G)) = SF
by FINSEQ_1:58;
thus (Eval p) . x =
Sum H
by A6, POLYNOM5:def 13
.=
Sum (H | (len H))
by FINSEQ_1:58
.=
SF . x
by A7, A9, A27, A28
;
verum end;
defpred S2[ Nat] means for g being PartFunc of REAL,REAL st g = Sum (G | p) holds
g is differentiable ;
A29:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
reconsider g1 =
Sum (G | k) as
Function of
REAL,
REAL by FUNCT_2:66;
assume A30:
for
g being
PartFunc of
REAL,
REAL st
g = Sum (G | k) holds
g is
differentiable
;
S2[k + 1]
then A31:
g1 is
differentiable
;
let g be
PartFunc of
REAL,
REAL;
( g = Sum (G | (k + 1)) implies g is differentiable )
assume A32:
g = Sum (G | (k + 1))
;
g is differentiable
per cases
( len G > k or len G <= k )
;
suppose A33:
len G > k
;
g is differentiable
k + 1
<= len G
by A33, NAT_1:13;
then A34:
k + 1
in dom G
by NAT_1:11, FINSEQ_3:25;
then A35:
G /. (k + 1) =
G . (k + 1)
by PARTFUN1:def 6
.=
FPower (
(p . ((k + 1) -' 1)),
((k + 1) -' 1))
by A2, A3, A34
.=
FPower (
(p . kk),
((k + 1) -' 1))
by NAT_D:34
.=
FPower (
(p . kk),
k)
by NAT_D:34
;
A36:
FPower (
(p . kk),
k) is
differentiable Function of
REAL,
REAL
by Th42;
G | (k + 1) =
(G | k) ^ <*(G . (k + 1))*>
by A33, FINSEQ_5:83
.=
(G | k) ^ <*(G /. (k + 1))*>
by A34, PARTFUN1:def 6
;
then g =
(Sum (G | k)) + (G /. (k + 1))
by A32, FVSUM_1:71
.=
g1 + (FPower ((p . kk),k))
by A35, FUNCSDOM:28
;
hence
g is
differentiable
by A31, A36;
verum end;
end;
A38:
S2[ 0 ]
for k being Nat holds S2[k]
from NAT_1:sch 2(A38, A29);
hence
Eval p is differentiable
by A4, A5, FUNCT_2:63; verum