let n be Ordinal; for b being bag of n
for r being Real st r >= 1 holds
for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (b,x)).| <= r |^ (degree b)
let b be bag of n; for r being Real st r >= 1 holds
for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (b,x)).| <= r |^ (degree b)
let r be Real; ( r >= 1 implies for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (b,x)).| <= r |^ (degree b) )
assume A1:
r >= 1
; for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (b,x)).| <= r |^ (degree b)
let x be Function of n,F_Real; ( ( for i being object st i in dom x holds
|.(x . i).| <= r ) implies |.(eval (b,x)).| <= r |^ (degree b) )
assume A2:
for i being object st i in dom x holds
|.(x . i).| <= r
; |.(eval (b,x)).| <= r |^ (degree b)
reconsider FR = F_Real as Field ;
reconsider X = x as Function of n, the carrier of F_Real ;
set sgm = SgmX ((RelIncl n),(support b));
set B = b * (SgmX ((RelIncl n),(support b)));
A3:
( rng (SgmX ((RelIncl n),(support b))) c= n & n = dom b )
by PARTFUN1:def 2, RELAT_1:def 19;
then A4:
dom (b * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b)))
by RELAT_1:27;
then A5:
len (b * (SgmX ((RelIncl n),(support b)))) = len (SgmX ((RelIncl n),(support b)))
by FINSEQ_3:29;
dom x = n
by FUNCT_2:def 1;
then A6:
dom (x * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b)))
by A3, RELAT_1:27;
consider y being FinSequence of FR such that
A7:
( len y = len (SgmX ((RelIncl n),(support b))) & eval (b,x) = Product y )
and
A8:
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power F_Real) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i))
by POLYNOM2:def 2;
rng (b * (SgmX ((RelIncl n),(support b)))) c= NAT
by VALUED_0:def 6;
then reconsider B = b * (SgmX ((RelIncl n),(support b))) as FinSequence of NAT by FINSEQ_1:def 4;
reconsider Y = y as FinSequence of F_Real ;
defpred S1[ Nat] means ( $1 <= len y implies ( Product (y | $1) is Real & ( for P being Real st P = Product (y | $1) holds
|.P.| <= r |^ (Sum (B | $1)) ) ) );
reconsider ZERO = 0 as Nat ;
y | ZERO = <*> the carrier of F_Real
;
then
Product (y | ZERO) = 1_ F_Real
by GROUP_4:8;
then A9:
S1[ 0 ]
by NEWTON:4;
A10:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
set i1 =
i + 1;
assume that A11:
S1[
i]
and A12:
i + 1
<= len y
;
( Product (y | (i + 1)) is Real & ( for P being Real st P = Product (y | (i + 1)) holds
|.P.| <= r |^ (Sum (B | (i + 1))) ) )
reconsider yi1 =
y /. (i + 1),
Pi =
Product (y | i) as
Real ;
A13:
|.Pi.| <= r |^ (Sum (B | i))
by A12, A11, NAT_1:13;
i + 1
in dom y
by A12, NAT_1:11, FINSEQ_3:25;
then
(
y | (i + 1) = (y | i) ^ <*(y . (i + 1))*> &
y . (i + 1) = y /. (i + 1) )
by FINSEQ_5:10, PARTFUN1:def 6;
then A14:
Product (y | (i + 1)) =
(Product (y | i)) * (y /. (i + 1))
by GROUP_4:6
.=
Pi * yi1
by BINOP_2:def 11
;
thus
Product (y | (i + 1)) is
Real
;
for P being Real st P = Product (y | (i + 1)) holds
|.P.| <= r |^ (Sum (B | (i + 1)))
let P be
Real;
( P = Product (y | (i + 1)) implies |.P.| <= r |^ (Sum (B | (i + 1))) )
assume A15:
P = Product (y | (i + 1))
;
|.P.| <= r |^ (Sum (B | (i + 1)))
A16:
|.P.| = |.Pi.| * |.yi1.|
by A15, A14, COMPLEX1:65;
i + 1
in dom B
by A7, A12, A4, NAT_1:11, FINSEQ_3:25;
then A17:
(
B | (i + 1) = (B | i) ^ <*(B . (i + 1))*> &
B . (i + 1) = B /. (i + 1) &
B . (i + 1) = b . ((SgmX ((RelIncl n),(support b))) . (i + 1)) )
by FINSEQ_5:10, PARTFUN1:def 6, FUNCT_1:12;
then
Sum (B | (i + 1)) = (Sum (B | i)) + (B /. (i + 1))
by RVSUM_1:74;
then A18:
r |^ (Sum (B | (i + 1))) = (r |^ (Sum (B | i))) * (r |^ (B /. (i + 1)))
by NEWTON:8;
A19:
|.yi1.| <= r |^ (B /. (i + 1))
proof
y /. (i + 1) =
(power F_Real) . (
((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)),
(B /. (i + 1)))
by A8, A12, NAT_1:11
.=
((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)) |^ (B /. (i + 1))
by NIVEN:7
;
then A20:
|.yi1.| = |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| |^ (B /. (i + 1))
by TAYLOR_2:1;
i + 1
in dom (x * (SgmX ((RelIncl n),(support b))))
by A6, A7, A12, NAT_1:11, FINSEQ_3:25;
then A21:
(
(x * (SgmX ((RelIncl n),(support b)))) /. (i + 1) = (x * (SgmX ((RelIncl n),(support b)))) . (i + 1) &
(x * (SgmX ((RelIncl n),(support b)))) . (i + 1) = x . ((SgmX ((RelIncl n),(support b))) . (i + 1)) &
(SgmX ((RelIncl n),(support b))) . (i + 1) in dom x &
i + 1
in dom (SgmX ((RelIncl n),(support b))) )
by PARTFUN1:def 6, FUNCT_1:11, FUNCT_1:12;
RelIncl n linearly_orders support b
by PRE_POLY:82;
then
(
(SgmX ((RelIncl n),(support b))) . (i + 1) in rng (SgmX ((RelIncl n),(support b))) &
rng (SgmX ((RelIncl n),(support b))) = support b )
by A21, FUNCT_1:def 3, PRE_POLY:def 2;
then
B /. (i + 1) <> 0
by A17, PRE_POLY:def 7;
then A22:
B /. (i + 1) >= 1
+ 0
by NAT_1:13;
end;
A23:
|.Pi.| >= 0
by COMPLEX1:46;
|.yi1.| >= 0
by COMPLEX1:46;
hence
|.P.| <= r |^ (Sum (B | (i + 1)))
by A13, A18, A23, A16, A19, XREAL_1:66;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A9, A10);
then
S1[ len y]
;
then
|.(eval (b,x)).| <= r |^ (Sum (B | (len B)))
by A5, A7;
hence
|.(eval (b,x)).| <= r |^ (degree b)
by Th4; verum