:: Scalar Multiple of Riemann Definite Integral
::  by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-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, REAL_1, SUBSET_1, FINSEQ_1, INTEGRA1, SEQ_4, XXREAL_0,
      XXREAL_1, VALUED_0, RELAT_1, ARYTM_3, FUNCT_1, CARD_1, NAT_1, CLASSES1,
      FINSEQ_5, ARYTM_1, ORDINAL4, XBOOLE_0, JORDAN3, MEMBERED, MEMBER_1,
      TARSKI, PARTFUN1, XXREAL_2, VALUED_1, MEASURE7, CARD_3, SEQ_1, INTEGRA2,
      MEASURE5, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0,
      XREAL_0, XXREAL_2, XXREAL_3, MEMBERED, MEMBER_1, XCMPLX_0, REAL_1, NAT_1,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, RFUNCT_1,
      RVSUM_1, INTEGRA1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4,
      FINSEQ_6, RCOMP_1, FINSEQ_5, CLASSES1, RFINSEQ, MEASURE5, MEASURE6;
 constructors PARTFUN1, REAL_1, NAT_1, SEQM_3, VALUED_0, RFUNCT_1, RFINSEQ,
      BINARITH, FINSEQ_5, FINSEQ_6, INTEGRA1, XXREAL_2, NAT_D, RVSUM_1, SEQ_4,
      CLASSES1, RELSET_1, SEQ_2, MEMBER_1, MEASURE6, COMSEQ_2;
 registrations RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED,
      FINSEQ_1, INTEGRA1, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SEQ_2,
      RELSET_1, XXREAL_3, MEMBER_1, MEASURE5, NAT_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Lemmas of Finite Sequence

reserve a,b,r,x,y for Real,
  i,j,k,n for Nat,
  x1 for set,
  p for FinSequence of REAL;

theorem :: INTEGRA2:1
  for A be non empty closed_interval Subset of REAL, x being Real holds
  x in A iff lower_bound A <= x & x <= upper_bound A;

definition
  let IT be FinSequence of REAL;
  redefine attr IT is non-decreasing means
:: INTEGRA2:def 1
  for n be Nat st n in dom IT & n+1 in dom IT holds IT.n <= IT.(n+1);
end;

registration
  cluster non-decreasing for FinSequence of REAL;
end;

theorem :: INTEGRA2:2
  for p be non-decreasing FinSequence of REAL, i,j st i in dom p & j in
  dom p & i <= j holds p.i <= p.j;

theorem :: INTEGRA2:3
  for p ex q be non-decreasing FinSequence of REAL st
    p,q are_fiberwise_equipotent;

theorem :: INTEGRA2:4
  for D be non empty set, f be FinSequence of D, k1,k2,k3 be Nat
    st 1<=k1 & k3<=len f & k1<=k2 & k2<k3
  holds mid(f,k1,k2)^mid(f,k2+1,k3)=mid(f,k1,k3);

begin :: Scalar Product of Real Subset

definition
  let A be real-membered set;
  let x be Real;
  redefine func x ** A -> Subset of REAL;
end;

theorem :: INTEGRA2:5
  for X,Y be non empty set, f be PartFunc of X,REAL st
    f|X is bounded_above & Y c= X holds f|Y|Y is bounded_above;

theorem :: INTEGRA2:6
  for X,Y be non empty set, f be PartFunc of X,REAL st
    f|X is bounded_below & Y c= X holds f|Y|Y is bounded_below;

theorem :: INTEGRA2:7
  for X being real-membered set, a being Real holds
    X is empty iff a ** X is empty;

theorem :: INTEGRA2:8
  for X be Subset of REAL holds r**X = {r*x : x in X};

theorem :: INTEGRA2:9
  for X be non empty Subset of REAL st X is bounded_above & 0<=r holds
    r**X is bounded_above;

theorem :: INTEGRA2:10
  for X be non empty Subset of REAL st X is bounded_above & r<=0 holds
    r**X is bounded_below;

theorem :: INTEGRA2:11
  for X be non empty Subset of REAL st X is bounded_below & 0<=r holds
    r**X is bounded_below;

theorem :: INTEGRA2:12
  for X be non empty Subset of REAL st X is bounded_below & r<=0 holds
    r**X is bounded_above;

theorem :: INTEGRA2:13
  for X be non empty Subset of REAL st X is bounded_above & 0<=r
  holds upper_bound(r**X) = r*(upper_bound X);

theorem :: INTEGRA2:14
  for X be non empty Subset of REAL st X is bounded_above & r<=0
  holds lower_bound(r**X) = r*(upper_bound X);

theorem :: INTEGRA2:15
  for X be non empty Subset of REAL st X is bounded_below & 0<=r
  holds lower_bound(r**X) = r*(lower_bound X);

theorem :: INTEGRA2:16
  for X be non empty Subset of REAL st X is bounded_below & r<=0
  holds upper_bound(r**X) = r*(lower_bound X);

begin :: Scalar Multiple of Integral

theorem :: INTEGRA2:17
  for X be non empty set, f be Function of X,REAL holds rng(r(#)f)
  = r**rng f;

theorem :: INTEGRA2:18
  for X,Z be non empty set, f be PartFunc of X,REAL holds rng(r(#)
  (f|Z)) = r**rng(f|Z);

reserve A, B for non empty closed_interval Subset of REAL;
reserve f, g for Function of A,REAL;
reserve D, D1, D2 for Division of A;

theorem :: INTEGRA2:19
  f|A is bounded & r >= 0 implies (upper_sum_set(r(#)f)).D >= r*(
  lower_bound rng f)*vol(A);

theorem :: INTEGRA2:20
  f|A is bounded & r <= 0 implies (upper_sum_set(r(#)f)).D >= r*(
  upper_bound rng f)*vol(A);

theorem :: INTEGRA2:21
  f|A is bounded & r >= 0 implies (lower_sum_set(r(#)f)).D <= r*(
  upper_bound rng f)*vol(A);

theorem :: INTEGRA2:22
  f|A is bounded & r <= 0 implies (lower_sum_set(r(#)f)).D <= r*(
  lower_bound rng f)*vol(A);

theorem :: INTEGRA2:23
  i in dom D & f|A is bounded_above & r >= 0 implies upper_volume(
  r(#)f,D).i = r*upper_volume(f,D).i;

theorem :: INTEGRA2:24
  i in dom D & f|A is bounded_above & r <= 0 implies lower_volume(
  r(#)f,D).i = r*upper_volume(f,D).i;

theorem :: INTEGRA2:25
  i in dom D & f|A is bounded_below & r >= 0 implies lower_volume(
  r(#)f,D).i = r*lower_volume(f,D).i;

theorem :: INTEGRA2:26
  i in dom D & f|A is bounded_below & r <= 0 implies upper_volume(
  r(#)f,D).i = r*lower_volume(f,D).i;

theorem :: INTEGRA2:27
  f|A is bounded_above & r >= 0 implies upper_sum(r(#)f,D) = r*
  upper_sum(f,D);

theorem :: INTEGRA2:28
  f|A is bounded_above & r <= 0 implies lower_sum(r(#)f,D) = r*
  upper_sum(f,D);

theorem :: INTEGRA2:29
  f|A is bounded_below & r >= 0 implies lower_sum(r(#)f,D) = r*
  lower_sum(f,D);

theorem :: INTEGRA2:30
  f|A is bounded_below & r <= 0 implies upper_sum(r(#)f,D) = r*
  lower_sum(f,D);

theorem :: INTEGRA2:31
  f|A is bounded & f is integrable implies r(#)f is integrable &
  integral(r(#)f) = r*integral(f);

begin :: Monotonicity of Integral

theorem :: INTEGRA2:32
  f|A is bounded & (for x st x in A holds f.x >= 0) implies
  integral(f) >= 0;

theorem :: INTEGRA2:33
  f|A is bounded & f is integrable & g|A is bounded & g is
integrable implies f-g is integrable & integral(f-g) = integral(f)-integral(g);

theorem :: INTEGRA2:34
  f|A is bounded & f is integrable & g|A is bounded & g is integrable &
  (for x st x in A holds f.x >= g.x) implies integral(f) >= integral(g);

begin :: Definition of Division Sequence

theorem :: INTEGRA2:35
  f|A is bounded implies rng upper_sum_set(f) is bounded_below;

theorem :: INTEGRA2:36
  f|A is bounded implies rng lower_sum_set(f) is bounded_above;

definition
  let A be non empty closed_interval Subset of REAL;
  mode DivSequence of A is sequence of divs A;
end;

definition
  let A;
  let T be DivSequence of A;
  let i;
  redefine func T.i -> Division of A;

end;

definition
  let A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
      T be DivSequence of A;
  func upper_sum(f,T) -> Real_Sequence means
:: INTEGRA2:def 2
  for i holds it.i = upper_sum(f,T.i);
  func lower_sum(f,T) -> Real_Sequence means
:: INTEGRA2:def 3
  for i holds it.i = lower_sum(f,T.
  i);
end;

theorem :: INTEGRA2:37
  D1 <= D2 implies for j st j in dom D2 holds ex i st i in dom D1
  & divset(D2,j) c= divset(D1,i);

theorem :: INTEGRA2:38
  A c= B implies vol(A) <= vol(B);

theorem :: INTEGRA2:39
  for A being Subset of REAL,
      a,x being Real st x in a ** A holds
   ex b being Real st b in A & x = a * b;

begin :: Addenda
:: missing, 2008.06.10

theorem :: INTEGRA2:40
  for A being non empty ext-real-membered set holds 0 ** A = {0};