let r be Real; for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2))) ) )
let Z be open Subset of REAL; for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2))) ) )
let f, f1, f2 be PartFunc of REAL,REAL; ( Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) implies ( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2))) ) ) )
assume that
A1:
Z c= dom ((r / 2) (#) (ln * (f1 + f2)))
and
A2:
for x being Real st x in Z holds
f1 . x = 1
and
A3:
r <> 0
and
A4:
f2 = (#Z 2) * f
and
A5:
for x being Real st x in Z holds
f . x = x / r
; ( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2))) ) )
A6:
Z c= dom (ln * (f1 + f2))
by A1, VALUED_1:def 5;
then
for y being object st y in Z holds
y in dom (f1 + f2)
by FUNCT_1:11;
then A7:
Z c= dom (f1 + f2)
;
then A8:
f1 + f2 is_differentiable_on Z
by A2, A4, A5, Th107;
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VALUED_1:def 1;
then A9:
Z c= dom f2
by A7, XBOOLE_1:18;
for x being Real st x in Z holds
ln * (f1 + f2) is_differentiable_in x
proof
let x be
Real;
( x in Z implies ln * (f1 + f2) is_differentiable_in x )
set g =
#Z 2;
assume A10:
x in Z
;
ln * (f1 + f2) is_differentiable_in x
then (f1 + f2) . x =
(f1 . x) + (f2 . x)
by A7, VALUED_1:def 1
.=
1
+ (((#Z 2) * f) . x)
by A2, A4, A10
.=
1
+ ((#Z 2) . (f . x))
by A4, A9, A10, FUNCT_1:12
.=
1
+ ((#Z 2) . (x / r))
by A5, A10
.=
1
+ ((x / r) #Z (1 + 1))
by TAYLOR_1:def 1
.=
1
+ (((x / r) #Z 1) * ((x / r) #Z 1))
by TAYLOR_1:1
.=
1
+ ((x / r) * ((x / r) #Z 1))
by PREPOWER:35
.=
1
+ ((x / r) * (x / r))
by PREPOWER:35
;
then A11:
(f1 + f2) . x > 0
by XREAL_1:34, XREAL_1:63;
f1 + f2 is_differentiable_in x
by A8, A10, FDIFF_1:9;
hence
ln * (f1 + f2) is_differentiable_in x
by A11, TAYLOR_1:20;
verum
end;
then A12:
ln * (f1 + f2) is_differentiable_on Z
by A6, FDIFF_1:9;
for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2)))
proof
let x be
Real;
( x in Z implies (((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2))) )
set g =
#Z 2;
assume A13:
x in Z
;
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2)))
then A14:
f1 + f2 is_differentiable_in x
by A8, FDIFF_1:9;
A15:
(f1 + f2) . x =
(f1 . x) + (f2 . x)
by A7, A13, VALUED_1:def 1
.=
1
+ (((#Z 2) * f) . x)
by A2, A4, A13
.=
1
+ ((#Z 2) . (f . x))
by A4, A9, A13, FUNCT_1:12
.=
1
+ ((#Z 2) . (x / r))
by A5, A13
.=
1
+ ((x / r) #Z (1 + 1))
by TAYLOR_1:def 1
.=
1
+ (((x / r) #Z 1) * ((x / r) #Z 1))
by TAYLOR_1:1
.=
1
+ ((x / r) * ((x / r) #Z 1))
by PREPOWER:35
.=
1
+ ((x / r) * (x / r))
by PREPOWER:35
;
then
(f1 + f2) . x > 0
by XREAL_1:34, XREAL_1:63;
then A16:
diff (
(ln * (f1 + f2)),
x) =
(diff ((f1 + f2),x)) / ((f1 + f2) . x)
by A14, TAYLOR_1:20
.=
(((f1 + f2) `| Z) . x) / ((f1 + f2) . x)
by A8, A13, FDIFF_1:def 7
.=
((2 * x) / (r ^2)) / (1 + ((x / r) ^2))
by A2, A4, A5, A7, A13, A15, Th107
;
thus (((r / 2) (#) (ln * (f1 + f2))) `| Z) . x =
(r / 2) * (diff ((ln * (f1 + f2)),x))
by A1, A12, A13, FDIFF_1:20
.=
((r * x) / (r ^2)) / (1 + ((x / r) ^2))
by A16
.=
((r / r) * (x / r)) / (1 + ((x / r) ^2))
by XCMPLX_1:76
.=
(1 * (x / r)) / (1 + ((x / r) ^2))
by A3, XCMPLX_1:60
.=
x / (r * (1 + ((x / r) ^2)))
by XCMPLX_1:78
;
verum
end;
hence
( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2))) ) )
by A1, A12, FDIFF_1:20; verum