Miz-B10

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);