let n be Ordinal; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: |.(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, RVSUM_1:72;
A10: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
set i1 = i + 1;
assume that
A11: S1[i] and
A12: i + 1 <= len y ; :: thesis: ( 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 ; :: thesis: for P being Real st P = Product (y | (i + 1)) holds
|.P.| <= r |^ (Sum (B | (i + 1)))
let P be Real; :: thesis: ( P = Product (y | (i + 1)) implies |.P.| <= r |^ (Sum (B | (i + 1))) )
assume A15: P = Product (y | (i + 1)) ; :: thesis: |.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;
per cases ( |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| > 0 or |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| = 0 ) by COMPLEX1:46;
suppose |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| > 0 ; :: thesis: |.yi1.| <= r |^ (B /. (i + 1))
hence |.yi1.| <= r |^ (B /. (i + 1)) by A20, A2, A21, PREPOWER:9; :: thesis: verum
end;
suppose |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| = 0 ; :: thesis: |.yi1.| <= r |^ (B /. (i + 1))
then |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| |^ (B /. (i + 1)) = 0 by A22, NEWTON:11;
hence |.yi1.| <= r |^ (B /. (i + 1)) by A1, A20; :: thesis: verum
end;
end;
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; :: thesis: 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; :: thesis: verum