:: Gauge Integral
::  by Roland Coghetto
:: 
:: Received September 3, 2017
:: Copyright (c) 2017-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 VALUED_1, MEMBERED, PARTFUN1, SEQ_4, INTEGRA1, MEASURE7, COUSIN,
      RELAT_1, NUMBERS, SUBSET_1, NAT_1, FUNCT_1, ARYTM_3, FINSEQ_2, ZFMISC_1,
      COMPLEX1, XBOOLE_0, REAL_1, CARD_1, XXREAL_0, ARYTM_1, FINSEQ_1, CARD_3,
      ORDINAL4, TARSKI, ORDINAL2, XXREAL_2, XXREAL_1, MEASURE5, RFINSEQ,
      PARTFUN3, VALUED_0, COUSIN2, FUNCT_7, FUNCT_3;
 notations ORDINAL1, VALUED_1, MEMBERED, PARTFUN1, XXREAL_2, FUNCT_1, XBOOLE_0,
      TARSKI, XCMPLX_0, XXREAL_0, FINSEQ_1, ZFMISC_1, SUBSET_1, NAT_1,
      FINSEQ_2, FUNCT_2, NUMBERS, XREAL_0, COMPLEX1, SEQ_2, RVSUM_1, RELSET_1,
      RCOMP_1, MEASURE5, SEQ_4, INTEGRA1, PARTFUN3, COUSIN, VALUED_0, FUNCT_3,
      INTEGRA3, RFINSEQ;
 constructors NEWTON, RCOMP_3, RVSUM_1, COMSEQ_2, SEQ_4, MEASURE6, RFINSEQ,
      MATRPROB, COUSIN, INTEGRA3;
 registrations SEQ_2, VALUED_1, XXREAL_2, COMPLEX1, SUBSET_1, FUNCT_1,
      RELSET_1, XXREAL_0, XREAL_0, MEMBERED, VALUED_0, FUNCT_2, FINSEQ_1,
      CARD_1, NAT_1, MEASURE5, INTEGRA1, SEQM_3, RELAT_1, ORDINAL1, XCMPLX_0,
      NUMBERS, SEQ_4, PARTFUN3, COUSIN, FINSET_1, NEWTON03, XBOOLE_0, RCOMP_3;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Preliminaries

reserve a,b,c,d,e for Real;

theorem :: COUSIN2:1
  a - b <= c & b <= a implies |. b - a .| <= c;

theorem :: COUSIN2:2
  b - a <= c & a <= b implies |. b - a .| <= c;

theorem :: COUSIN2:3
  a <= b <= c & |.a - d.| <= e & |.c - d.| <= e implies |. b - d .| <= e;

theorem :: COUSIN2:4
  (for c st 0 < c holds |.a - b.| <= c) implies a = b;

theorem :: COUSIN2:5
  for b,c,d being non negative Real st
  d < e / (2 * b * |. c .|) holds
  b is positive & c is positive;

theorem :: COUSIN2:6
  a <> 0 implies a * (b / (2 * a)) = b / 2;

theorem :: COUSIN2:7
  for b,c,d being non negative Real st a <= b * c * d &
  d < e / (2 * b * |. c .|) holds a <= e / 2;

begin :: Vector lattice / Riesz Space

definition
  let X be non empty set;
  let f,g be Function of X,REAL;
  func min(f,g) -> Function of X,REAL means
:: COUSIN2:def 1
  for x be Element of X holds it.x = min(f.x,g.x);
  commutativity;
  func max(f,g) -> Function of X,REAL means
:: COUSIN2:def 2
  for x be Element of X holds it.x = max(f.x,g.x);
  commutativity;
end;

registration
  let X be non empty set;
  let f,g be positive-yielding Function of X,REAL;
  cluster min(f,g) -> positive-yielding;
end;

registration
  let X be non empty set;
  let f,g be positive-yielding Function of X,REAL;
  cluster max(f,g) -> positive-yielding;
end;

definition
  let X be non empty set;
  let f,g be Function of X,REAL;
  pred f <= g means
:: COUSIN2:def 3
for x being Element of X holds f.x <= g.x;
end;

theorem :: COUSIN2:8
  for X being non empty set
  for f,g being Function of X,REAL holds
  min(f,g) <= f;

theorem :: COUSIN2:9
  for X being non empty real-membered set st
  (for r being Real st r in X holds upper_bound X = r) holds
  ex r being Real st X = {r};

theorem :: COUSIN2:10
  for X being non empty real-membered set st
  (for r being Real st r in X holds lower_bound X = r) holds
  ex r being Real st X = {r};

theorem :: COUSIN2:11
  for X be non empty bounded_below bounded_above real-membered set
  st upper_bound X = lower_bound X
  holds ex r be Real st X = {r};

begin :: chi

reserve X,Y for set,
          Z for non empty set,
          r for Real,
          s for ExtReal,
          A for Subset of REAL,
          f for real-valued Function;

theorem :: COUSIN2:12
  chi(X,Y) is Function of Y,REAL;

theorem :: COUSIN2:13
  A c= ].r,s.[ implies A is bounded_below;

theorem :: COUSIN2:14
  A c= ].s,r.[ implies A is bounded_above;

theorem :: COUSIN2:15
  rng f c= [.a,b.] implies f is bounded;

theorem :: COUSIN2:16
  a <= b implies {a,b} c= [.a,b.];

theorem :: COUSIN2:17
  chi(X,Y) is bounded;

theorem :: COUSIN2:18
  X misses Y implies (for x being Element of X holds (chi(Y,X)).x = 0);

theorem :: COUSIN2:19
  for f be Function of Z,REAL holds (f is constant iff
  (ex r be Real st f = r (#) chi(Z,Z)));

theorem :: COUSIN2:20
  chi(X,X) is positive-yielding;

begin

reserve I for non empty closed_interval Subset of REAL,
       TD for tagged_division of I,
        D for Division of I,
        T for Element of set_of_tagged_Division(D),
        f for PartFunc of I,REAL;

theorem :: COUSIN2:21
  f is lower_integrable implies lower_sum(f,D) <= lower_integral(f);

theorem :: COUSIN2:22
  f is upper_integrable implies upper_integral(f) <= upper_sum(f,D);

definition
  let A be non empty closed_interval Subset of REAL;
  func tagged_divs A -> set means
:: COUSIN2:def 4
    for x being set holds (x in it iff x is tagged_division of A);
end;

registration
  let A be non empty closed_interval Subset of REAL;
  cluster tagged_divs A -> non empty;
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let TD be tagged_division of A;
  func tagged_of TD -> non empty non-decreasing FinSequence of REAL means
:: COUSIN2:def 5

  ex D being Division of A, T being Element of set_of_tagged_Division(D) st
  it = T & TD = [D,T];
end;

theorem :: COUSIN2:23
  TD = [D,T] implies T = tagged_of TD &
  D = division_of TD;

theorem :: COUSIN2:24
  len tagged_of TD = len division_of TD;

definition
  let A be non empty closed_interval Subset of REAL;
  let TD be tagged_division of A;
  func len TD -> Element of NAT equals
:: COUSIN2:def 6
    len division_of TD;
  func dom TD -> set equals
:: COUSIN2:def 7
    dom division_of TD;
end;

theorem :: COUSIN2:25
  for I being non empty closed_interval Subset of REAL,
  D being Division of I, T being Element of set_of_tagged_Division(D) holds
  rng T c= I;

theorem :: COUSIN2:26
  for I being non empty closed_interval Subset of REAL
  for jauge1,jauge2 being positive-yielding Function of I,REAL
  for TD being jauge1-fine tagged_division of I st jauge1 <= jauge2 holds
  TD is jauge2-fine tagged_division of I;

begin :: Jauge integral: definition

definition
  let I be non empty closed_interval Subset of REAL;
  let f be PartFunc of I,REAL;
  let TD be tagged_division of I;
  func tagged_volume(f,TD) -> FinSequence of REAL means
:: COUSIN2:def 8
    len it = len TD &
    for i being Nat st i in dom TD holds it.i = f.((tagged_of TD).i) *
      vol(divset(division_of TD,i));
end;

definition
  let I be non empty closed_interval Subset of REAL;
  let f be PartFunc of I,REAL;
  let TD be tagged_division of I;
  func tagged_sum(f,TD) -> Real equals
:: COUSIN2:def 9
Sum tagged_volume(f,TD);
end;

theorem :: COUSIN2:27
  Y c= X implies chi(X,Y) = chi(Y,Y);

reserve f for Function of I,REAL;

theorem :: COUSIN2:28
  I is non empty trivial implies vol I = 0;

theorem :: COUSIN2:29
  for r being Real st I = {r} holds
  (for D being Division of I holds D = <* r *> );

definition
  let I be non empty closed_interval Subset of REAL;
  let f be Function of I,REAL;
  attr f is HK-integrable means
:: COUSIN2:def 10
  ex J being Real st
    for epsilon being Real st epsilon > 0 holds
      ex jauge being positive-yielding Function of I,REAL st
      for TD being tagged_division of I st TD is jauge-fine
        holds |.tagged_sum(f,TD) - J.| <= epsilon;
end;

definition
  let I be non empty closed_interval Subset of REAL;
  let f be Function of I,REAL;
  assume
 f is HK-integrable;
  func HK-integral f -> Real means
:: COUSIN2:def 11
  for epsilon being Real st epsilon > 0 holds
    ex jauge being positive-yielding Function of I,REAL st
      for TD being tagged_division of I st TD is jauge-fine
      holds |.tagged_sum(f,TD) - it.| <= epsilon;
end;

theorem :: COUSIN2:30
  for f being Function of I,REAL st I is trivial holds
  f is HK-integrable & HK-integral(f) = 0;

theorem :: COUSIN2:31
  A misses I & f = chi(A,I) implies tagged_sum(f,TD) = 0;

theorem :: COUSIN2:32
  A misses I & f = chi(A,I) implies f is HK-integrable & HK-integral(f) = 0;

theorem :: COUSIN2:33
  I c= A & f = chi(A,I) implies f is HK-integrable & HK-integral(f) = vol(I);

registration
  let I be non empty closed_interval Subset of REAL;
  cluster HK-integrable for Function of I,REAL;
end;

begin :: Linearity of jauge-integrale

reserve f,g for HK-integrable Function of I,REAL,
          r for Real;

theorem :: COUSIN2:34
  for i being Nat st i in dom TD holds
  (tagged_volume(r(#)f,TD)).i
    = r * f.((tagged_of TD).i) * vol(divset(division_of TD,i));

theorem :: COUSIN2:35
  tagged_volume(r(#)f,TD) = r * tagged_volume(f,TD);

theorem :: COUSIN2:36
  for i being Nat st i in dom TD holds
  (tagged_volume(f + g,TD)).i
    = f.((tagged_of TD).i) * vol(divset(division_of TD,i))
      + g.((tagged_of TD).i) * vol(divset(division_of TD,i));

theorem :: COUSIN2:37
  tagged_volume(f + g,TD) = tagged_volume(f,TD) + tagged_volume(g,TD);

theorem :: COUSIN2:38
  f is HK-integrable implies
  r (#) f is HK-integrable Function of I,REAL &
  HK-integral (r (#) f) = r * HK-integral f;

theorem :: COUSIN2:39
  f + g is HK-integrable Function of I,REAL &
  HK-integral (f + g) = HK-integral f + HK-integral g;

theorem :: COUSIN2:40
  for f being Function of I,REAL st f is constant holds
  (f is HK-integrable & ex r being Real st
  f = r (#) chi(I,I) & HK-integral f = r * vol(I));

begin :: integrable + bounded -> HK-integrable

registration
  let I being non empty closed_interval Subset of REAL;
  cluster integrable for Function of I,REAL;
end;

registration
  let X be non empty set;
  cluster bounded for Function of X,REAL;
end;

theorem :: COUSIN2:41
  for f being bounded Function of I,REAL holds
  |. upper_bound (rng f) - lower_bound (rng f) .| = 0 iff f is constant;

registration
  let I be non empty closed_interval Subset of REAL;
  cluster bounded for integrable Function of I,REAL;
end;

theorem :: COUSIN2:42
  for f being PartFunc of I,REAL st f is upper_integrable holds
  ex r being Real st for D being Division of I holds r < upper_sum(f,D);

theorem :: COUSIN2:43
  for f being PartFunc of I,REAL st f is lower_integrable holds
  ex r being Real st for D being Division of I holds lower_sum(f,D) < r;

theorem :: COUSIN2:44
  for f being Function of I,REAL
  for D,D1 being Division of I st D.1 = lower_bound I & D1 = D/^1
  holds upper_sum(f,D1) = (upper_sum(f,D)) & lower_sum(f,D1) = lower_sum(f,D);

reserve f for bounded integrable Function of I,REAL;

theorem :: COUSIN2:45
  for i being Nat st i in dom TD holds
  (lower_volume(f,division_of TD)).i <= (tagged_volume(f,TD)).i
    <= (upper_volume(f,division_of TD)).i;

theorem :: COUSIN2:46
  Sum lower_volume(f,division_of TD) <= Sum tagged_volume(f,TD)
    <= Sum upper_volume(f,division_of TD);

theorem :: COUSIN2:47
  for epsilon being Real st I is non trivial & 0 < epsilon holds
  ex D being Division of I st D.1 <> lower_bound I &
  upper_sum(f,D) < integral(f) + (epsilon / 2) &
  integral(f) - (epsilon / 2) < lower_sum(f,D) &
  upper_sum(f,D) - lower_sum(f,D) < epsilon;

reserve jauge for positive-yielding Function of I,REAL;

theorem :: COUSIN2:48
  jauge = r (#) chi(I,I) implies 0 < r;

reserve D for tagged_division of I;

theorem :: COUSIN2:49
  jauge = r (#) chi(I,I) & D is jauge-fine
  implies delta(division_of D) <= r;

reserve r1,r2,s for Real,
           D,D1 for Division of I,
             fc for Function of I,REAL;

theorem :: COUSIN2:50
  ex i being Nat st i in dom D &
  min rng upper_volume(fc,D) = (upper_volume(fc,D)).i;

theorem :: COUSIN2:51
  for f being Function of I,REAL
  for epsilon being Real st
  fc = chi(I,I) &
  r1 = min rng upper_volume(fc,D1) &
  r2 = epsilon / (2 * (len D1) *
    |. upper_bound (rng f) - lower_bound (rng f) .| ) &
  0 < r1 & 0 < r2 & s = min(r1,r2) / 2 &
  jauge = s (#) fc & TD is jauge-fine holds
  delta(division_of TD) < min rng upper_volume(fc,D1) &
  delta(division_of TD) < epsilon / (2 * (len D1) *
    |. upper_bound (rng f) - lower_bound (rng f) .| );

theorem :: COUSIN2:52
  for p being FinSequence of REAL st
  (for i being Nat st i in dom p holds r <= p.i) &
  ex i0 being Nat st i0 in dom p & p.i0 = r holds
  r = inf rng p;

theorem :: COUSIN2:53
   fc = chi(I,I) implies 0 <= min rng upper_volume(fc,D) &
   (0 = min rng upper_volume(fc,D) iff divset(D,1) = [.D.1,D.1.]);

theorem :: COUSIN2:54
  divset(D,1) = [.D.1,D.1.] implies D.1 = lower_bound I;

theorem :: COUSIN2:55
  for f being bounded integrable Function of I,REAL
  holds f is HK-integrable & HK-integral(f) = integral(f);

registration
  let I be non empty closed_interval Subset of REAL;
  cluster bounded integrable -> HK-integrable for Function of I,REAL;
end;