B.10 ANAL_1


ANAL_1.ABS (Digest)
Some Properties of Functions Modul and Signum, by Jan Popio{1}ek.


reserve x, y, z, s, t for Real;

def 1 func |.x.| -> Real means it = x if 0 x otherwise it = -x;

1 0x implies |.x.| = x; 2 0 < x implies |.x.| = x; 3 not 0 x implies |.x.| = -x; 5 0 |.x.|; 6 x < > 0 implies 0 < |.x.|; 7 x = 0 iff |.x.| = 0; 9 |.x.| = -x & x < > 0 implies x < 0; 10 for x , y holds |.x y.| = |.x.| |.y.|; 11 -|.x.| x & x |.x.|; 12 -y x & x y iff |.x.| y; 13 |.x + y.| |.x.| + |.y.|; 14 for x st x < > 0 holds |.x.| |.1/x.|=1; 15 for x st x < > 0 holds |.1/x.| = 1/|.x.|; 16 for x , y st y < > 0 holds |.x/y.| = |.x.|/|.y.|; 17 |.x.| = |.-x.|; 18 for x , y holds |.x.| - |.y.| |.x - y.|; 19 for x , y holds |.x - y.| |.x.| + |.y.|; 20 for x holds |.|.x.|.| = |.x.|; 21 |.x.| z & |.y.| t implies |.x + y.| z + t; 22 |.|.x.| - |.y.|.||.x - y.|; 24 0xy implies |.x + y.| = |.x.| + |.y.|; 25 |.x + y.| = |.x.| + |.y.| implies 0 xy; 26 |.x + y.|/(1 + |.x + y.|) |.x.|/(1 + |.x.|) + |.y.|/(1 + |.y.|);

def 2 func sgn x -> Real means it = 1 if (0 < x) , it = -1 if x < 0 otherwise it = 0;

27 0 < x implies sgn x = 1; 28 x < 0 implies sgn x = -1; 29 not (0 < x) & not (x < 0) implies sgn x = 0; 30 x = 0 implies sgn x = 0; 31 sgn x = 1 implies 0 < x; 32 sgn x = -1 implies x < 0; 33 sgn x = 0 implies x = 0; 34 x = |.x.| sgn x; 35 sgn (xy) = sgn x sgn y; 36 sgn sgn x = sgn x; 37 sgn (x + y) sgn x + sgn y + 1; 38 x < > 0 implies sgn x sgn (1/x) = 1; 39 x < > 0 implies 1/(sgn x) = sgn (1/x); 40 sgn x + sgn y - 1 sgn (x + y); 41 x < > 0 implies sgn x = sgn (1/x); 42 y < > 0 implies sgn (x/y) = (sgn x)/(sgn y);