environ
vocabularies ARYTM, ARYTM_1, RELAT_1, ARYTM_3, FUNCT_1, ABSVALUE, SEQ_4,
SEQ_2;
notations SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, COMPLEX1, FUNCT_1,
RELSET_1, FUNCT_2, SEQ_4, XXREAL_0, PARTFUN3;
constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN3;
registrations RELSET_1, XREAL_0, MEMBERED, SEQ_1, RELAT_1, FUNCT_2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions SEQ_4;
theorems XREAL_1, COMPLEX1, SEQ_1, SEQ_4, FUNCT_1, FUNCT_2, XCMPLX_1,
ABSVALUE;
begin
reserve
x,y,z for Element of REAL,
f,g for Function of REAL,REAL;
Lm1: abs(f.x) in rng abs f
proof
dom abs f = REAL by FUNCT_2:def 1;
then (abs f).x = abs(f.x) by SEQ_1:def 10;
hence abs(f.x) in rng abs f by FUNCT_2:6;
end;
theorem
(for x,y holds f.(x+y)+f.(x-y)=2*f.x*g.y) &
(ex x st f.x<>0) & (for x holds abs(f.x)<=1)
implies for x holds abs(g.x)<=1
proof
assume that
A1: for x,y holds f.(x+y)+f.(x-y)=2*f.x*g.y;
given z such that
A2: f.z<>0;
assume
A3: for x being Element of REAL holds abs(f.x)<=1;
let y such that
A4: abs(g.y) > 1;
set X = rng abs f, k = upper_bound X, D = abs(g.y);
A5: abs(g.y) > 0 by A4,XREAL_1:2;
A6: X is bounded_above
proof
take 1;
let r be real number;
assume r in X;
then consider x being set such that
A7: x in dom abs f and
A8: (abs f).x = r by FUNCT_1:def 5;
abs(f.x) = r by A7,A8,SEQ_1:def 10;
hence r<=1 by A3,A7;
end;
A9: for s being real number st s in X holds s<=k/D
proof
let s be real number;
assume s in X;
then consider x being set such that
B1: x in dom abs f and
B2: s = (abs f).x by FUNCT_1:def 5;
B3: s = abs(f.x) by B1,B2,SEQ_1:def 10;
reconsider x as Element of REAL by B1;
set A = f.(x+y), B = f.(x-y), C = abs(f.x);
B4: abs(A+B)<=abs(A)+abs(B) by COMPLEX1:142;
abs(A) in X & abs(B) in X by Lm1;
then abs(A)<=k & abs(B)<=k by A6,SEQ_4:def 4;
then
B5: abs(A)+abs(B)<=k+k by XREAL_1:9;
abs(A+B) = abs(2*f.x*g.y) by A1
.= abs(2*f.x)*D by COMPLEX1:151
.= abs(2)*C*D by COMPLEX1:151
.= 2*C*D by ABSVALUE:def 1;
then 2*(C*D)<=2*k by B4,B5,XREAL_1:2;
then C*D<=k by XREAL_1:70;
then C*D/D<=k/D by A5,XREAL_1:74;
hence thesis by A5,B3,XCMPLX_1:90;
end;
abs(f.z) in X by Lm1;
then
B6: abs(f.z)<=k by A6,SEQ_4:def 4;
0