:: Symmetrical Piecewise Linear Functions Composed by Absolute Value Function
:: by Takashi Mitsuishi
::
:: Received December 18, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

theorem Lmbcd: :: FUZZY_8:1

for b, c, d being Real st b > 0 & c > 0 & d > 0 holds
(b - d) / (b / c) < c

proof end;

theorem :: FUZZY_8:2

for a, x being Real holds a - |.(a * x).| <= a

proof end;

theorem L724x: :: FUZZY_8:3

for a, x being Real holds a - |.x.| <= a

proof end;

theorem :: FUZZY_8:4

for a, b, c, x being Real holds |.((b * ((a - x) - a)) / c).| = |.((b * ((a + x) - a)) / c).|

proof end;

theorem F51max: :: FUZZY_8:5

for a, b, c being Real holds |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|

proof end;

theorem F51min: :: FUZZY_8:6

for a, b, c being Real holds |.((min (c,a)) - (min (c,b))).| <= |.(a - b).|

proof end;

theorem F51: :: FUZZY_8:7

for a, b, c, d being Real holds |.((min (c,(max (d,a)))) - (min (c,(max (d,b))))).| <= |.(a - b).|

proof end;

theorem :: FUZZY_8:8

for c being Real
for f, g being PartFunc of REAL,REAL st ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g holds
(f | ].-infty,c.[) +* (g | [.c,+infty.[) = (f | ].-infty,c.]) +* (g | [.c,+infty.[)

proof end;

theorem Th1: :: FUZZY_8:9

for c being Real
for f, g being PartFunc of REAL,REAL st f is continuous & g is continuous & f . c = g . c & ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g holds
(f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous

proof end;

theorem :: FUZZY_8:10

for c being Real
for f, g being Function of REAL,REAL st f is continuous & g is continuous & f . c = g . c holds
(f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous Function of REAL,REAL

proof end;

theorem F633: :: FUZZY_8:11

for a, b, c being Real
for f, g, h being Function of REAL,REAL st a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b holds
integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))

proof end;

theorem INTEGR241: :: FUZZY_8:12

for f being Function of REAL,REAL
for a, b, c being Real st a <= b & b <= c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] holds
( f is_integrable_on ['a,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )

proof end;

theorem INTEGRA617: :: FUZZY_8:13

for a, b, c being Real
for f being Function of REAL,REAL st a <= c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & ['a,c'] c= dom f & b in ['a,c'] holds
( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )

proof end;

theorem Th39: :: FUZZY_8:14

for A being non empty closed_interval Subset of REAL
for a being Real
for f, g, h being Function of REAL,REAL st f | A is bounded & f is_integrable_on A & g | A is bounded & g is_integrable_on A & a in A & h = (f | ].-infty,a.]) +* (g | [.a,+infty.[) & f . a = g . a holds
h is_integrable_on A

proof end;

theorem FUZZY711: :: FUZZY_8:15

for a, b, c being Real
for f, g being Function of REAL,REAL st a <= b & b <= c holds
((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.])

proof end;

theorem :: FUZZY_8:16

for a, b, c being Real
for f, g, h being Function of REAL,REAL st a <= b & b <= c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & g is_integrable_on ['a,c'] & g | ['a,c'] is bounded & h = (f | ].-infty,b.]) +* (g | [.b,+infty.[) & f . b = g . b holds
integral (h,['a,c']) = (integral (f,['a,b'])) + (integral (g,['b,c']))

proof end;

::area and centroid of continuous function

theorem :: FUZZY_8:17

for f, g, h being Function of REAL,REAL
for a, b, c being Real st a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & integral (f,['a,b']) <> 0 & integral (g,['b,c']) <> 0 & f . b = g . b holds
centroid (h,['a,c']) = (1 / (integral (h,['a,c']))) * (((centroid (f,['a,b'])) * (integral (f,['a,b']))) + ((centroid (g,['b,c'])) * (integral (g,['b,c']))))

proof end;

::b _________
:: /\
:: / \
::d ---------
:: / \
::- --
::a-c a a+c
::
:: Symmetric membership functions by absolute value function

theorem :: FUZZY_8:18

for f being Function of REAL,REAL
for a, b, c being Real st ( for x being Real holds f . x = b - |.((b * (x - a)) / c).| ) holds
for y being Real holds f . (a - y) = f . (a + y)

proof end;

theorem :: FUZZY_8:19

for f being Function of REAL,REAL
for a, b, c, d, e being Real st ( for x being Real holds f . x = min (d,(max (e,(b - |.((b * (x - a)) / c).|)))) ) holds
for y being Real holds f . (a - y) = f . (a + y)

proof end;

theorem LmCri2: :: FUZZY_8:20

for a, b, c, d being Real st b > 0 & c > 0 & d > 0 & d < b holds
for x being Real holds (d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))) . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|))))

proof end;

theorem Lm223: :: FUZZY_8:21

for a, b, c, d being Real st b > 0 & c > 0 & d > 0 & d < b holds
centroid ((d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))),['(a - c),(a + c)']) = a

proof end;

theorem Lm220: :: FUZZY_8:22

for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f = d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))

proof end;

theorem Lm221: :: FUZZY_8:23

for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,['(a - c),(a + c)']) = a

proof end;

theorem L724p: :: FUZZY_8:24

for a, b, c, d, e being Real
for f being Function of REAL,REAL st b <> 0 & c <> 0 & ( for x being Real holds f . x = min (d,(max (e,(b - |.((b * (x - a)) / c).|)))) ) holds
f is Lipschitzian

proof end;

theorem L724: :: FUZZY_8:25

for a, b, c, d, e being Real
for f being Function of REAL,REAL st c <> 0 & ( for x being Real holds f . x = min (d,(max (e,(b - |.((b * (x - a)) / c).|)))) ) holds
f is Lipschitzian

proof end;

theorem Lm22a: :: FUZZY_8:26

for A being non empty closed_interval Subset of REAL
for a, b, c, d being Real
for f being Function of REAL,REAL st c > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
( f is_integrable_on A & f | A is bounded )

proof end;

theorem Lm22b: :: FUZZY_8:27

for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 )

proof end;

theorem FU710a: :: FUZZY_8:28

for a, b, c being Real st b > 0 & c > 0 holds
for x being Real st not x in ['(a - c),(a + c)'] holds
max (0,(b - |.((b * (x - a)) / c).|)) = 0

proof end;

theorem FU710b: :: FUZZY_8:29

for a, b, c, d being Real st b > 0 & c > 0 & d > 0 holds
for x being Real st not x in ['(a - c),(a + c)'] holds
min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = 0

proof end;

theorem FU710: :: FUZZY_8:30

for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
for x being Real st not x in ['(a - c),(a + c)'] holds
f . x = 0

proof end;

theorem Lm22B3: :: FUZZY_8:31

for A being non empty closed_interval Subset of REAL
for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
for x being Real st x in A \ ['(a - c),(a + c)'] holds
f . x = 0

proof end;

theorem Lm22: :: FUZZY_8:32

for A being non empty closed_interval Subset of REAL
for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,A) = a

proof end;

theorem :: FUZZY_8:33

for A being non empty closed_interval Subset of REAL
for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ['(a - c),(a + c)'] c= A & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,A) = centroid (f,['(a - c),(a + c)'])

proof end;

theorem :: FUZZY_8:34

for a, b, c, d being Real
for f, F being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) & ( for x being Real holds F . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)'])

proof end;

theorem :: FUZZY_8:35

for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f | [.(a - c),(a + c).] = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])

proof end;

:: (c,s)
:: (b,r) __ -- s
:: r __ -- | \
:: /| | \
:: / | | \
:: ------------------------
:: a b c d
:: (a,0) (d,0)
:: square with vertices (a,0),(b,r),(c,s) and (d,0)

theorem Th23a: :: FUZZY_8:36

for a, b, c, d, r, s being Real st a < b & b < c & c < d holds
( (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . a = 0 & (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . d = 0 )

proof end;

theorem Th23: :: FUZZY_8:37

for a, b, c, d, r, s being Real
for f being Function of REAL,REAL st a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) holds
integral (((id REAL) (#) f),['a,d']) = ((integral (((id REAL) (#) (AffineMap ((r / (b - a)),(- ((a * r) / (b - a)))))),['a,b'])) + (integral (((id REAL) (#) (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b)))))),['b,c']))) + (integral (((id REAL) (#) (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c)))))),['c,d']))

proof end;

theorem Th24: :: FUZZY_8:38

for a, b, c, d, r, s being Real
for f being Function of REAL,REAL st a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) holds
integral (f,['a,d']) = ((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d']))

proof end;

theorem Lm1: :: FUZZY_8:39

for a, b, c, d, r, s, x being Real st a < b & b < c & c < d & r >= 0 & s >= 0 & ( x < a or d < x ) holds
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x <= 0

proof end;

theorem Lm2: :: FUZZY_8:40

for a, b, c, d, r, s, x being Real st a < b & b < c & c < d & r >= 0 & s >= 0 & x in [.a,d.] holds
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0

proof end;

theorem :: FUZZY_8:41

for a, b, c, d, r, s being Real st a < b & b < c & c < d & r >= 0 & s >= 0 & r = s holds
for x being Real holds (r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)

proof end;

theorem Th4: :: FUZZY_8:42

for a, b, c, d being Real st c <= d holds
( integral (((id REAL) (#) (AffineMap (a,b))),['c,d']) = (d - c) * (((a * (((d * d) + (d * c)) + (c * c))) / 3) + ((b * (d + c)) / 2)) & integral ((AffineMap (a,b)),['c,d']) = (d - c) * (((a * (d + c)) / 2) + b) )

proof end;

theorem :: FUZZY_8:43

for a, b, c, d, r, s being Real
for f being Function of REAL,REAL st a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) holds
centroid (f,['a,d']) = ((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + ((c - b) * (((((s - r) / (c - b)) * (c + b)) / 2) + (s - ((c * (s - r)) / (c - b)))))) + ((d - c) * (((((- s) / (d - c)) * (d + c)) / 2) + (- ((d * (- s)) / (d - c))))))

proof end;

::d _________ AffineMap (0,d)
:: \ /
:: \ /
:: \
:: / \
:: / \
:: -----------
:: b c
::
:: sum of functions

theorem :: FUZZY_8:44

for b, c, d being Real st b < c holds
(AffineMap ((d * (1 / (c - b))),(d * (- (b / (c - b)))))) + (AffineMap ((d * (- (1 / (c - b)))),(d * (c / (c - b))))) = AffineMap (0,d)

proof end;

theorem :: FUZZY_8:45

for a, b, c, p, q being Real st a < b & b < c holds
((AffineMap (p,q)) | [.a,b.]) +* ((AffineMap (p,q)) | [.b,c.]) = (AffineMap (p,q)) | [.a,c.]

proof end;

theorem :: FUZZY_8:46

for a, b, c being Real st a < b & b < c holds
for x being Real st x in [.a,b.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x

proof end;

theorem :: FUZZY_8:47

for a, b, c being Real st a < b & b < c holds
for x being Real st x in [.b,c.] holds
(TriangularFS (a,b,c)) . x = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . x

proof end;

theorem :: FUZZY_8:48

for a, b, c being Real st a < b & b < c holds
for x being Real st not x in ].a,c.[ holds
(TriangularFS (a,b,c)) . x = (AffineMap (0,0)) . x

proof end;