:: Properties of Partial Functions from a Domain to the Set of Real Numbers
::  by Jaros{\l}aw Kotowicz and Yuji Sakai
::
:: Received March 15, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, REAL_1, XXREAL_0, CARD_1, ARYTM_1, ARYTM_3,
      COMPLEX1, RELAT_1, XBOOLE_0, FINSEQ_1, TARSKI, FUNCT_1, PARTFUN1,
      VALUED_1, CLASSES1, FUNCOP_1, MEMBERED, VALUED_0, ORDINAL4, BINOP_1,
      SETWISEO, CARD_3, NAT_1, RFINSEQ, FUNCT_3, PBOOLE, LIMFUNC1, FINSET_1,
      XXREAL_1, FINSEQ_2, RFUNCT_3, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
      XREAL_0, COMPLEX1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, BINOP_1, XXREAL_0, REAL_1, NAT_1, FUNCOP_1, SETWISEO, FINSEQ_2,
      FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, RFUNCT_1, FINSEQ_4, SETWOP_2,
      FINSET_1, RVSUM_1, RCOMP_1, PARTFUN2, LIMFUNC1, CLASSES1, RFINSEQ;
 constructors PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, BINOP_2, COMPLEX1,
      SEQM_3, PROB_1, SEQ_4, FINSEQOP, RCOMP_1, FINSEQ_4, FINSOP_1, PARTFUN2,
      RFUNCT_1, RVSUM_1, LIMFUNC1, RFINSEQ, CLASSES1, RELSET_1, SETFAM_1,
      VALUED_0, SQUARE_1;
 registrations XBOOLE_0, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0,
      XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, VALUED_0, FUNCT_1, CARD_1,
      RVSUM_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin ::  Nonnegative and Nonpositive Part of a Real Number

reserve n,m for Nat,
  r,r1,r2,s,t for Real,
  x,y for set;

definition
  let r be Real;
  func max+ (r) -> Real equals
:: RFUNCT_3:def 1
  max(r,0);
  func max- (r) -> Real equals
:: RFUNCT_3:def 2
  max(-r,0);
end;

theorem :: RFUNCT_3:1
  for r be Real holds r = max+(r) - max-(r);

theorem :: RFUNCT_3:2
  for r be Real holds |.r.| = max+(r) + max-(r);

theorem :: RFUNCT_3:3
  for r be Real holds 2*max+(r) = r + |.r.|;

theorem :: RFUNCT_3:4
  for r,s be Real st 0<=r holds max+(r*s) = r*(max+ s);

theorem :: RFUNCT_3:5
  for r,s be Real holds max+(r+s) <= max+(r) + max+(s);

begin

::
:: Partial Functions from a Domain to the Set of Real Numbers
::

theorem :: RFUNCT_3:6
  for D be non empty set, F be PartFunc of D,REAL, r,s be Real
 st r <> 0 holds F"{s/r} = (r(#)F)"{s};

theorem :: RFUNCT_3:7
  for D be non empty set, F be PartFunc of D,REAL holds (0(#)F)"{0} = dom F;

theorem :: RFUNCT_3:8
  for D be non empty set, F be PartFunc of D,REAL, r st 0<
  r holds abs(F)"{r} = F"{-r,r};

theorem :: RFUNCT_3:9
  for D be non empty set, F be PartFunc of D,REAL holds abs(F)"{0} = F"{0};

theorem :: RFUNCT_3:10
  for D be non empty set, F be PartFunc of D,REAL, r st r<
  0 holds abs(F)"{r} = {};

theorem :: RFUNCT_3:11
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc
of C,REAL, r st r <> 0 holds F,G are_fiberwise_equipotent iff r(#)F, r
  (#)G are_fiberwise_equipotent;

theorem :: RFUNCT_3:12
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
  REAL holds F,G are_fiberwise_equipotent iff -F, -G are_fiberwise_equipotent;

theorem :: RFUNCT_3:13
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
  REAL st F,G are_fiberwise_equipotent holds abs(F), abs(G)
  are_fiberwise_equipotent;

definition
  let X,Y be set;
  mode PartFunc-set of X,Y -> set means
:: RFUNCT_3:def 3

    for x being Element of it holds x is PartFunc of X,Y;
end;

registration
  let X,Y be set;
  cluster non empty for PartFunc-set of X,Y;
end;

definition
  let X,Y be set;
  mode PFUNC_DOMAIN of X,Y is non empty PartFunc-set of X,Y;
end;

definition
  let X,Y be set;
  redefine func PFuncs(X,Y) -> PartFunc-set of X,Y;
  let P be non empty PartFunc-set of X,Y;
  redefine mode Element of P -> PartFunc of X,Y;
end;

definition
  let D,C be non empty set, X be Subset of D, c be Element of C;
  redefine func X --> c -> Element of PFuncs(D,C);
end;

:: awaryjne, A.T.

registration
  let D be non empty set, E be real-membered set;
  cluster -> real-valued for Element of PFuncs(D,E);
end;

definition
  let D be non empty set, E be real-membered set, F1,F2 be Element of PFuncs(D
  ,E);
  redefine func F1+F2 -> Element of PFuncs(D,REAL);
  redefine func F1-F2 -> Element of PFuncs(D,REAL);
  redefine func F1(#)F2 -> Element of PFuncs(D,REAL);
  redefine func F1/F2 -> Element of PFuncs(D,REAL);
end;

definition
  let D be non empty set, E be real-membered set, F be Element of PFuncs(D,E);
  redefine func abs(F) -> Element of PFuncs(D,REAL);
  redefine func - F -> Element of PFuncs(D,REAL);
  redefine func F^ -> Element of PFuncs(D,REAL);
end;

definition
  let D be non empty set, E be real-membered set, F be Element of PFuncs(D,E),
  r be Real;
  redefine func r(#)F -> Element of PFuncs(D,REAL);
end;

definition
  let D be non empty set;
  func addpfunc(D) -> BinOp of PFuncs(D,REAL) means
:: RFUNCT_3:def 4

  for F1,F2 be Element of PFuncs(D,REAL) holds it.(F1,F2) = F1 + F2;
end;

theorem :: RFUNCT_3:14
  for D be non empty set holds addpfunc(D) is commutative;

theorem :: RFUNCT_3:15
  for D be non empty set holds addpfunc(D) is associative;

theorem :: RFUNCT_3:16
  for D be non empty set holds [#](D) --> (0 qua Real)
  is_a_unity_wrt addpfunc(D);

theorem :: RFUNCT_3:17
  for D be non empty set holds the_unity_wrt addpfunc(D) = [#](D)
  --> (0 qua Real);

theorem :: RFUNCT_3:18
  for D be non empty set holds addpfunc(D) is having_a_unity;

definition
  let D be non empty set, f be FinSequence of PFuncs(D,REAL);
  func Sum(f) -> Element of PFuncs(D,REAL) equals
:: RFUNCT_3:def 5
  (addpfunc(D)) $$ f;
end;

theorem :: RFUNCT_3:19
  for D be non empty set holds Sum(<*> PFuncs(D,REAL) ) = [#](D)
  -->(0 qua Real);

theorem :: RFUNCT_3:20
  for D be non empty set, f be FinSequence of PFuncs(D,REAL), G be
  Element of PFuncs(D,REAL) holds Sum(f^<*G*>) = Sum f + G;

theorem :: RFUNCT_3:21
  for D be non empty set, f1,f2 be FinSequence of PFuncs(D,REAL)
  holds Sum(f1^f2) = Sum f1 + Sum f2;

theorem :: RFUNCT_3:22
  for D be non empty set, f be FinSequence of PFuncs(D,REAL), G be
  Element of PFuncs(D,REAL) holds Sum(<*G*>^f) = G + Sum f;

theorem :: RFUNCT_3:23
  for D be non empty set, G1,G2 be Element of PFuncs(D,REAL) holds
  Sum<*G1,G2*> = G1 + G2;

theorem :: RFUNCT_3:24
  for D be non empty set, G1,G2,G3 be Element of PFuncs(D,REAL) holds
  Sum<*G1,G2,G3*> = G1 + G2 + G3;

theorem :: RFUNCT_3:25
  for D be non empty set, f,g be FinSequence of PFuncs(D,REAL) st f,g
  are_fiberwise_equipotent holds Sum f = Sum g;

definition
  let D be non empty set, f be FinSequence;
  func CHI(f,D) -> FinSequence of PFuncs(D,REAL) means
:: RFUNCT_3:def 6

  len it = len f & for n st n in dom it holds it.n = chi(f.n,D);
end;

definition
  let D be non empty set, f be FinSequence of PFuncs(D,REAL), R be FinSequence
  of REAL;
  func R (#) f -> FinSequence of PFuncs(D,REAL) means
:: RFUNCT_3:def 7

  len it = min(len R,len f) &
  for n st n in dom it for F be PartFunc of D,REAL, r st r = R.n &
  F = f.n holds it.n = r(#)F;
end;

definition
  let D be non empty set, f be FinSequence of PFuncs(D,REAL),
      d be Element of D;
  func f#d -> FinSequence of REAL means
:: RFUNCT_3:def 8

  len it = len f & for n be Element of NAT st n in dom it holds it.n = f.n.d;
end;

definition
  let D,C be non empty set, f be FinSequence of PFuncs(D,C), d be Element of D;
  pred d is_common_for_dom f means
:: RFUNCT_3:def 9

  for n be Nat st n in dom f holds d in dom (f.n);
end;

theorem :: RFUNCT_3:26
  for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be
  Element of D, n be Nat st d is_common_for_dom f & n <> 0 holds
  d is_common_for_dom f|n;

theorem :: RFUNCT_3:27
  for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be
  Element of D, n be Nat st d is_common_for_dom f holds d
  is_common_for_dom f /^ n;

theorem :: RFUNCT_3:28
  for D be non empty set, d be Element of D, f be FinSequence of
  PFuncs(D,REAL) st len f <> 0 holds d is_common_for_dom f iff d in dom Sum(f);

theorem :: RFUNCT_3:29
  for D be non empty set, f be FinSequence of PFuncs(D,REAL), d be
  Element of D, n be Nat holds (f|n)#d = (f#d)|n;

theorem :: RFUNCT_3:30
  for D be non empty set, f be FinSequence, d be Element of D
  holds d is_common_for_dom CHI(f,D);

theorem :: RFUNCT_3:31
  for D be non empty set, d be Element of D, f be FinSequence of
  PFuncs(D,REAL), R be FinSequence of REAL st d is_common_for_dom f holds d
  is_common_for_dom R(#)f;

theorem :: RFUNCT_3:32
  for D be non empty set, f be FinSequence, R be FinSequence of REAL, d
  be Element of D holds d is_common_for_dom R(#)CHI(f,D);

theorem :: RFUNCT_3:33
  for D be non empty set, d be Element of D, f be FinSequence of PFuncs(
  D, REAL ) st d is_common_for_dom f holds (Sum(f)).d = Sum (f#d);

definition
  let D be non empty set, F be PartFunc of D,REAL;
  func max+(F) -> PartFunc of D,REAL means
:: RFUNCT_3:def 10

  dom it = dom F & for d be Element of D st d in dom it holds it.d = max+(F.d);
  func max-(F) -> PartFunc of D,REAL means
:: RFUNCT_3:def 11

  dom it = dom F & for d be Element of D st d in dom it holds it.d = max-(F.d);
end;

theorem :: RFUNCT_3:34
  for D be non empty set, F be PartFunc of D,REAL holds F = max+(F) -
  max-(F) & abs(F) = max+(F) + max-(F) & 2 (#) max+(F) = F + abs(F);

theorem :: RFUNCT_3:35
  for D be non empty set, F be PartFunc of D,REAL, r st 0<
  r holds F"{r} = max+(F)"{r};

theorem :: RFUNCT_3:36
  for D be non empty set, F be PartFunc of D,REAL holds F"(
  left_closed_halfline(0)) = max+(F)"{0};

theorem :: RFUNCT_3:37
  for D be non empty set, F be PartFunc of D,REAL, d be Element of
  D holds 0<=(max+ F).d;

theorem :: RFUNCT_3:38
  for D be non empty set, F be PartFunc of D,REAL, r st 0<
  r holds F"{-r} = max-(F)"{r};

theorem :: RFUNCT_3:39
  for D be non empty set, F be PartFunc of D,REAL holds F"(
  right_closed_halfline(0)) = max-(F)"{0};

theorem :: RFUNCT_3:40
  for D be non empty set, F be PartFunc of D,REAL, d be Element of
  D holds 0<=(max- F).d;

theorem :: RFUNCT_3:41
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
  REAL st F,G are_fiberwise_equipotent holds max+(F), max+(G)
  are_fiberwise_equipotent;

theorem :: RFUNCT_3:42
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
  REAL st F,G are_fiberwise_equipotent holds max-(F), max-(G)
  are_fiberwise_equipotent;

registration
  let D be non empty set, F be finite PartFunc of D,REAL;
  cluster max+(F) -> finite;
  cluster max-(F) -> finite;
end;

theorem :: RFUNCT_3:43
  for D,C be non empty set, F be finite PartFunc of D,REAL, G be finite
PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G
  are_fiberwise_equipotent holds F, G are_fiberwise_equipotent;

theorem :: RFUNCT_3:44
  for D be non empty set, F be PartFunc of D,REAL, X be set holds
  (max+ F)|X = max+ (F|X);

theorem :: RFUNCT_3:45
  for D be non empty set, F be PartFunc of D,REAL, X be set holds (max-
  F)|X = max- (F|X);

theorem :: RFUNCT_3:46
  for D be non empty set, F be PartFunc of D,REAL st (for d be
  Element of D st d in dom F holds F.d>=0) holds max+ F = F;

theorem :: RFUNCT_3:47
  for D be non empty set, F be PartFunc of D,REAL st (for d be Element
  of D st d in dom F holds F.d<=0) holds max- F = -F;

theorem :: RFUNCT_3:48
  for D be non empty set, F be PartFunc of D,REAL holds F - 0 = F;

theorem :: RFUNCT_3:49
  for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set
  holds (F|X) - r = (F-r)| X;

theorem :: RFUNCT_3:50
  for D be non empty set, F be PartFunc of D,REAL, r,s
  holds F"{s+r} = (F-r)"{s};

theorem :: RFUNCT_3:51
  for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,
  REAL , r be Real holds F, G are_fiberwise_equipotent iff F-r,G-r
  are_fiberwise_equipotent;

definition

  let F be PartFunc of REAL,REAL, X be set;
  pred F is_convex_on X means
:: RFUNCT_3:def 12

  X c= dom F & for p be Real st 0<=p & p<=1
  for r,s be Real st r in X & s in X & p*r + (1-p)*s in X
   holds F.(p*r +(1-p)*s) <= p*F.r + (1-p)*F.s;
end;

theorem :: RFUNCT_3:52
  for a,b be Real, F be PartFunc of REAL,REAL holds F is_convex_on
  [.a,b.] iff [.a,b.] c= dom F &
   for p be Real st 0<=p & p<=1
  for r,s be Real st r in [.a,b.] & s in [.a,b.]
   holds F.(p*r + (1-p)*s) <= p*F.r + (1-p)*F.s;

theorem :: RFUNCT_3:53
  for a,b be Real,
      F be PartFunc of REAL,REAL holds F is_convex_on [.a,b
.] iff [.a,b.] c= dom F &
 for x1,x2,x3 be Real st x1 in [.a,b.] & x2 in [.a,b.]
& x3 in [.a,b.] & x1<x2 & x2<x3 holds (F.x1-F.x2)/(x1-x2)<=(F.x2-F.x3)/(x2-x3);

theorem :: RFUNCT_3:54
  for F be PartFunc of REAL,REAL, X,Y be set st F is_convex_on X & Y c=
  X holds F is_convex_on Y;

theorem :: RFUNCT_3:55
  for F be PartFunc of REAL,REAL, X be set, r holds F
  is_convex_on X iff F-r is_convex_on X;

theorem :: RFUNCT_3:56
  for F be PartFunc of REAL,REAL, X be set, r st 0<r holds F
  is_convex_on X iff r(#)F is_convex_on X;

theorem :: RFUNCT_3:57
  for F be PartFunc of REAL,REAL, X be set st X c= dom F holds 0(#) F
  is_convex_on X;

theorem :: RFUNCT_3:58
  for F,G be PartFunc of REAL,REAL, X be set st F is_convex_on X & G
  is_convex_on X holds F+G is_convex_on X;

theorem :: RFUNCT_3:59
  for F be PartFunc of REAL,REAL, X be set, r st F
  is_convex_on X holds max+(F-r) is_convex_on X;

theorem :: RFUNCT_3:60
  for F be PartFunc of REAL,REAL, X be set st F is_convex_on X holds
  max+ F is_convex_on X;

theorem :: RFUNCT_3:61
  id [#](REAL) is_convex_on REAL;

theorem :: RFUNCT_3:62
  for r be Real holds max+(id [#](REAL) - r) is_convex_on REAL;

definition
  let D be non empty set, F be PartFunc of D,REAL, X be set;
  assume
 dom(F|X) is finite;
  func FinS(F,X) -> non-increasing FinSequence of REAL means
:: RFUNCT_3:def 13

  F|X, it are_fiberwise_equipotent;
end;

theorem :: RFUNCT_3:63
  for D be non empty set, F be PartFunc of D,REAL, X be set st dom
  (F|X) is finite holds FinS(F,dom(F|X)) = FinS(F,X);

theorem :: RFUNCT_3:64
  for D be non empty set, F be PartFunc of D,REAL, X be set st dom
  (F|X) is finite holds FinS(F|X,X) = FinS(F,X);

theorem :: RFUNCT_3:65
  for D be non empty set, d be Element of D, X be set,
      F be PartFunc of D,REAL st
    X is finite & d in dom(F|X) holds
    FinS(F,X\{d})^<*F.d*>, F|X are_fiberwise_equipotent;

theorem :: RFUNCT_3:66
  for D be non empty set, d be Element of D, X be set,
      F be PartFunc of D,REAL st
      dom(F|X) is finite & d in dom(F|X) holds
    FinS(F,X\{d})^<*F.d*>, F|X are_fiberwise_equipotent;

theorem :: RFUNCT_3:67
  for D be non empty set, F be PartFunc of D,REAL, X be set,
      Y being finite set st Y = dom(F|X) holds len FinS(F,X) = card Y;

theorem :: RFUNCT_3:68
  for D be non empty set, F be PartFunc of D,REAL holds FinS(F,{}) = <*>REAL;

theorem :: RFUNCT_3:69
  for D be non empty set, F be PartFunc of D,REAL, d be Element of
  D st d in dom F holds FinS(F,{d}) = <* F.d *>;

theorem :: RFUNCT_3:70
  for D be non empty set, F be PartFunc of D,REAL, X be set, d be
Element of D st dom(F|X) is finite & d in dom(F|X) & FinS(F,X).(len FinS(F,X))
  = F.d holds FinS(F,X) = FinS(F,X\{d}) ^ <*F.d*>;

theorem :: RFUNCT_3:71
  for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|X
) is finite & Y c= X & (for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom
  (F|(X\Y)) holds F.d1>=F.d2) holds FinS(F,X) = FinS(F,Y) ^ FinS(F,X \ Y);

theorem :: RFUNCT_3:72
  for D be non empty set, F be PartFunc of D,REAL, r be Real, X be
set, d be Element of D st dom(F|X) is finite & d in dom(F|X) holds FinS(F-r,X).
  (len FinS(F-r,X)) = (F-r).d iff FinS(F,X).(len FinS(F,X)) = F.d;

theorem :: RFUNCT_3:73
  for D be non empty set, F be PartFunc of D,REAL, r be Real, X be
set, Z being finite set st Z = dom(F|X) holds FinS(F-r, X) = FinS(F,X) - (card
  Z |->r);

theorem :: RFUNCT_3:74
  for D be non empty set, F be PartFunc of D,REAL, X be set st dom(F|X)
  is finite & (for d be Element of D st d in dom(F|X) holds F.d>=0) holds FinS(
  max+ F, X) = FinS(F, X);

theorem :: RFUNCT_3:75
  for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real,
Z be finite set st Z = dom(F|X) & rng(F|X) = {r} holds FinS(F, X) = card(Z) |->
  r;

theorem :: RFUNCT_3:76
  for D be non empty set, F be PartFunc of D,REAL, X,Y be set st
dom(F|(X \/ Y)) is finite & X misses Y holds FinS(F,X \/ Y), FinS(F,X) ^ FinS(F
  ,Y) are_fiberwise_equipotent;

definition
  let D be non empty set, F be PartFunc of D,REAL, X be set;
  func Sum(F,X) -> Real equals
:: RFUNCT_3:def 14
  Sum FinS(F,X);
end;

theorem :: RFUNCT_3:77
  for D be non empty set, F be PartFunc of D,REAL, X be set, r
    st dom(F|X) is finite holds Sum(r(#)F,X) = r * Sum(F,X);

theorem :: RFUNCT_3:78
  for D be non empty set, F,G be PartFunc of D,REAL, X be set, Y
being finite set st Y = dom(F|X) & dom(F|X) = dom(G|X) holds Sum(F+G,X) = Sum(F
  ,X) + Sum(G,X);

theorem :: RFUNCT_3:79
  for D be non empty set, F,G be PartFunc of D,REAL, X be set st dom(F|X
  ) is finite & dom(F|X) = dom(G|X) holds Sum(F-G,X) = Sum(F,X) - Sum (G,X);

theorem :: RFUNCT_3:80
  for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real,
  Y being finite set st Y = dom(F|X) holds Sum(F-r,X) = Sum(F,X) - r*card(Y);

theorem :: RFUNCT_3:81
  for D be non empty set, F be PartFunc of D,REAL holds Sum(F,{}) = 0;

theorem :: RFUNCT_3:82
  for D be non empty set, F be PartFunc of D,REAL, d be Element of D st
  d in dom F holds Sum(F,{d}) = F.d;

theorem :: RFUNCT_3:83
  for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|(
  X \/ Y)) is finite & X misses Y holds Sum(F, X \/ Y) = Sum(F,X) + Sum (F,Y);

theorem :: RFUNCT_3:84
  for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|(
X \/ Y)) is finite & dom(F|X) misses dom(F|Y) holds Sum(F, X \/ Y) = Sum(F,X) +
  Sum(F,Y);