:: Gauge Integral
:: by Roland Coghetto
::
:: Received September 3, 2017
:: Copyright (c) 2017-2026 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;
definitions TARSKI, XBOOLE_0;
expansions FUNCT_1, TARSKI, XBOOLE_0;
theorems CGAMES_1, NUMBERS, VALUED_1, FINSEQ_3, XXREAL_2, XTUPLE_0, PARTFUN1,
VALUED_0, JORDAN5A, INTEGRA1, XXREAL_1, ABSVALUE, FINSEQ_1, FINSEQ_2,
FUNCT_2, NAT_1, FUNCT_1, FINSEQ_5, XREAL_1, XXREAL_0, XBOOLE_0, TARSKI,
RFINSEQ, XCMPLX_1, INT_1, SEQ_4, PARTFUN3, SEQ_2, COUSIN, FUNCT_3,
ZFMISC_1, INTEGR23, PARTFUN2, RELAT_1, XREAL_0, COMPLEX1, RVSUM_1,
INTEGRA4, INTEGRA5, SPRECT_1, INTEGRA2, INTEGRA3, INTEGR20, IRRAT_1,
XBOOLE_1;
schemes FUNCT_2, FINSEQ_2, XFAMILY;
begin :: Preliminaries
reserve a,b,c,d,e for Real;
theorem Th01:
a - b <= c & b <= a implies |. b - a .| <= c
proof
assume that
A1: a - b <= c and
A2: b <= a;
b - b <= a - b by A2,XREAL_1:9; then
A3: 0 <= c by A1;
(-1) * c <= (-1) * (a - b) by A1,XREAL_1:65; then
A5: -c <= b - a;
b - a <= a - a by A2,XREAL_1:9;
hence thesis by ABSVALUE:5,A5,A3;
end;
theorem Th02:
b - a <= c & a <= b implies |. b - a .| <= c
proof
assume that
A1: b - a <= c and
A2: a <= b;
A3: a - a <= b - a by A2,XREAL_1:9;
then -c <= 0 by A1;
hence thesis by A3,A1,ABSVALUE:5;
end;
Lm01:
a <= b + c & b <= d implies a <= d + c
proof
assume
A1: a <= b + c & b <= d;
then b + c <= d + c by XREAL_1:7;
hence thesis by A1,XXREAL_0:2;
end;
Lm02:
a < b + c & b - c < d implies a - d < 2 * c
proof
assume that
A1: a < b + c and
A2: b - c < d;
a - d < (b + c) - (b - c) by A1,A2,XREAL_1:14;
hence thesis;
end;
theorem Th03:
a <= b <= c & |.a - d.| <= e & |.c - d.| <= e implies |. b - d .| <= e
proof
assume that
A1: a <= b <= c and
A2: |.a - d.| <= e and
A3: |.c - d.| <= e;
b in [.a,c.] & a <= c by A1,XXREAL_1:1,XXREAL_0:2;
then consider r be Real such that
A4: 0 <= r & r <= 1 and
A5: b = r * a + (1 - r) * c by SPRECT_1:51;
A6: |. r * (a - d) + (1 - r) * (c - d).| <= |. r * (a - d) .|
+ |.(1 - r) * (c - d).| by COMPLEX1:56;
|. r * (a - d) .| = |.r.| * |.a - d.| by COMPLEX1:65
.= r * |.a - d.| by A4,ABSVALUE:def 1;
then
A7: |. r * (a - d) .| <= r * e by A4,A2,XREAL_1:64;
A8: r - r <= 1 - r by A4,XREAL_1:9;
|. (1 - r) * (c - d) .| = |.1 - r.| * |.c - d.| by COMPLEX1:65
.= (1 - r) * |.c - d.| by A8,ABSVALUE:def 1;
then
A9: |. (1 - r) * (c - d) .| <= (1 - r) * e by A8,A3,XREAL_1:64;
|. b - d .| <= r * e + |.(1 - r) * (c - d).| by A5,A6,A7,Lm01;
then |. b - d .| <= r * e + (1 - r) * e by A9,Lm01;
hence thesis;
end;
theorem Th04:
(for c st 0 < c holds |.a - b.| <= c) implies a = b
proof
assume
A1: for c st 0 < c holds |.a - b.| <= c;
assume a <> b;
then
A2: a - b <> 0;
set e = |.a - b.| / 2;
2 * e <= e by A1;
then (2 * e) / e <= e / e by XREAL_1:72;
then 2 <= e / e by A2,XCMPLX_1:89;
then 2 <= 1 by A2,XCMPLX_1:60;
hence contradiction;
end;
theorem Th05:
for b,c,d being non negative Real st
d < e / (2 * b * |. c .|) holds
b is positive & c is positive
proof
let b,c,d be non negative Real;
assume
A1: d < e / (2 * b * |. c .|);
assume not (b is positive & c is positive);
then per cases;
suppose b <= 0;
then 2 * b * |.c.| = 0;
hence contradiction by A1,XCMPLX_1:49;
end;
suppose c <= 0;
then |. c .| = 0;
hence contradiction by A1,XCMPLX_1:49;
end;
end;
theorem Th06:
a <> 0 implies a * (b / (2 * a)) = b / 2
proof
assume
A1: a <> 0;
a * (b / (2 * a)) = (a * b) / (a * 2) by XCMPLX_1:74
.= (a / a * b) / 2 by XCMPLX_1:83
.= (1 * b) / 2 by A1,XCMPLX_1:60;
hence thesis;
end;
theorem Th07:
for b,c,d being non negative Real st a <= b * c * d &
d < e / (2 * b * |. c .|) holds a <= e / 2
proof
let b,c,d be non negative Real;
assume that
A1: a <= b * c * d and
A2: d < e / (2 * b * |. c .|);
A3: 0 < b & 0 < c by A2,Th05;
A4: (b * c) * d <= (b * c) * (e / (2 * b * |. c .|)) by A2,XREAL_1:64;
(b * c) * (e / (2 * b * |. c .|)) = (b * c) * (e / (2 * b * c))
by ABSVALUE:def 1
.= (b * c) * (e / (2 * (b * c)))
.= e / 2 by A3,Th06;
hence thesis by A4,A1,XXREAL_0:2;
end;
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 :DEFM1:
for x be Element of X holds it.x = min(f.x,g.x);
existence
proof
deffunc F(object) = min(f.(In($1,X)),g.(In($1,X)));
A1: for x be object st x in X holds F(x) in REAL by XREAL_0:def 1;
consider h be Function of X,REAL such that
A2: for x be object st x in X holds h.x = F(x) from FUNCT_2:sch 2(A1);
take h;
let x be Element of X;
h.x = min(f.x,g.(In(x,X))) by A2
.= min(f.x,g.x);
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of X,REAL such that
A3: for x be Element of X holds m1.x = min(f.x,g.x) and
A4: for x be Element of X holds m2.x = min(f.x,g.x);
now
dom m1 = X by PARTFUN1:def 2;
hence dom m1 = dom m2 by PARTFUN1:def 2;
hereby
let x be object;
assume x in dom m1;
then reconsider y = x as Element of X;
m1.x = min(f.y,g.y) by A3;
hence m1.x = m2.x by A4;
end;
end;
hence thesis;
end;
commutativity;
func max(f,g) -> Function of X,REAL means :DEFM2:
for x be Element of X holds it.x = max(f.x,g.x);
existence
proof
deffunc F(object) = max(f.(In($1,X)),g.(In($1,X)));
A1: for x be object st x in X holds F(x) in REAL by XREAL_0:def 1;
consider h be Function of X,REAL such that
A2: for x be object st x in X holds h.x = F(x) from FUNCT_2:sch 2(A1);
take h;
let x be Element of X;
h.x = max(f.x,g.(In(x,X))) by A2
.= max(f.x,g.x);
hence thesis;
end;
uniqueness
proof
let m1,m2 be Function of X,REAL such that
A3: for x be Element of X holds m1.x = max(f.x,g.x) and
A4: for x be Element of X holds m2.x = max(f.x,g.x);
now
dom m1 = X by PARTFUN1:def 2;
hence dom m1 = dom m2 by PARTFUN1:def 2;
hereby
let x be object;
assume x in dom m1;
then reconsider y = x as Element of X;
m1.x = max(f.y,g.y) by A3;
hence m1.x = m2.x by A4;
end;
end;
hence thesis;
end;
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;
coherence
proof
now
let r be Real;
assume r in rng min(f,g);
then consider x be object such that
A1: x in X and
A2: (min(f,g)).x = r by FUNCT_2:11;
reconsider y = x as Element of X by A1;
r = min(f.y,g.y) by A2,DEFM1;
then (r = f.y) or (r = g.y) by XXREAL_0:15;
then r in rng f or r in rng g by FUNCT_2:4;
hence 0 < r by PARTFUN3:def 1;
end;
hence thesis by PARTFUN3:def 1;
end;
end;
registration
let X be non empty set;
let f,g be positive-yielding Function of X,REAL;
cluster max(f,g) -> positive-yielding;
coherence
proof
now
let r be Real;
assume r in rng max(f,g);
then consider x be object such that
A1: x in X and
A2: (max(f,g)).x = r by FUNCT_2:11;
reconsider y = x as Element of X by A1;
r = max(f.y,g.y) by A2,DEFM2;
then (r = f.y) or (r = g.y) by XXREAL_0:16;
then r in rng f or r in rng g by FUNCT_2:4;
hence 0 < r by PARTFUN3:def 1;
end;
hence thesis by PARTFUN3:def 1;
end;
end;
definition
let X be non empty set;
let f,g be Function of X,REAL;
pred f <= g means for x being Element of X holds f.x <= g.x;
end;
theorem Th08:
for X being non empty set
for f,g being Function of X,REAL holds
min(f,g) <= f
proof
let X be non empty set;
let f,g be Function of X,REAL;
now
let x be Element of X;
(min(f,g)).x = min(f.x,g.x) by DEFM1;
hence (min(f,g)).x <= f.x & (min(f,g)).x <= g.x by XXREAL_0:17;
end;
hence thesis;
end;
Lm03:
for X be non empty set st
(ex s be object st (for r be object st r in X holds s = r)) holds
ex r be object st X = {r}
proof
let X be non empty set;
assume ex s be object st (for r be object st r in X holds s = r);
then consider s0 be object such that
A1: for r be object st r in X holds s0 = r;
set r0 = the Element of X;
take r0;
thus X c= {r0}
proof
let x be object;
assume
A3: x in X;
r0 = s0 by A1
.= x by A1,A3;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {r0};
then x = r0 by TARSKI:def 1;
hence thesis;
end;
theorem Th09:
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}
proof
let X be non empty real-membered set;
assume
A1: for r be Real st r in X holds upper_bound X = r;
ex s be object st (for x be object st x in X holds s = x)
proof
set s = upper_bound X;
take s;
thus thesis by A1;
end;
then consider r be object such that
A2: X = {r} by Lm03;
reconsider r0 = the Element of X as Real;
take r0;
thus thesis by A2,TARSKI:def 1;
end;
theorem
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}
proof
let X be non empty real-membered set;
assume
A1: for r be Real st r in X holds lower_bound X = r;
ex s be object st (for x be object st x in X holds s = x)
proof
set s = lower_bound X;
take s;
thus thesis by A1;
end;
then consider r be object such that
A2: X = {r} by Lm03;
set r0 = the Element of X;
take r0;
thus thesis by A2,TARSKI:def 1;
end;
theorem Th10:
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}
proof
let X be non empty bounded_below bounded_above real-membered set;
assume
A1: upper_bound X = lower_bound X;
for r be Real st r in X holds upper_bound X = r
proof
let r be Real;
assume r in X;
then upper_bound X <= r & r <= upper_bound X by A1,SEQ_4:def 1,def 2;
hence thesis by XXREAL_0:1;
end;
hence thesis by Th09;
end;
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 Th11:
chi(X,Y) is Function of Y,REAL
proof
({0,1} = {} implies X = {}) & {0,1} c= REAL by INT_1:3,NUMBERS:19;
hence thesis by FUNCT_2:7;
end;
theorem
A c= ].r,s.[ implies A is bounded_below
proof
assume
A1: A c= ].r,s.[;
].r,s.[ c= [.r,s.[ by XXREAL_1:22;
then A c= [.r,s.[ by A1;
hence thesis by XXREAL_2:44;
end;
theorem
A c= ].s,r.[ implies A is bounded_above
proof
assume
A1: A c= ].s,r.[;
].s,r.[ c= ].s,r.] by XXREAL_1:21;
then A c= ].s,r.] by A1;
hence thesis by XXREAL_2:43;
end;
theorem Th12:
rng f c= [.a,b.] implies f is bounded
proof
assume
A1: rng f c= [.a,b.];
[.a,b.] c= [.a, +infty .[ & [.a,b.] c= ]. -infty,b.] by XXREAL_1:251,265;
then rng f c= [.a, +infty .[ & rng f c= ]. -infty,b.] by A1;
then rng f is bounded_below & rng f is bounded_above by XXREAL_2:43,44;
then f is bounded_below & f is bounded_above by INTEGRA1:12,14;
hence thesis;
end;
theorem Th13:
a <= b implies {a,b} c= [.a,b.]
proof
assume
A1: a <= b;
let x be object;
assume x in {a,b};
then x = a or x = b by TARSKI:def 2;
hence thesis by A1,XXREAL_1:1;
end;
theorem Th14:
chi(X,Y) is bounded
proof
{0,1} c= [.0,1.] by Th13;
then rng chi(X,Y) c= [.0,1.];
hence thesis by Th12;
end;
theorem Th15:
X misses Y implies (for x being Element of X holds (chi(Y,X)).x = 0)
proof
assume
A1: X misses Y;
let x be Element of X;
per cases;
suppose A2: X is non empty;
then not x in Y by A1,XBOOLE_0:def 4;
then x in X \ Y by A2,XBOOLE_0:def 5;
hence thesis by FUNCT_3:37;
end;
suppose X is empty;
hence thesis;
end;
end;
theorem Th16:
for f be Function of Z,REAL holds (f is constant iff
(ex r be Real st f = r (#) chi(Z,Z)))
proof
let f be Function of Z,REAL;
hereby
assume
A1: f is constant;
set y = the Element of rng f;
consider x be object such that
A2: x in dom f and
A3: y = f.x by FUNCT_1:def 3;
reconsider r = y as Real;
take r;
now
thus
A3BIS: dom (r (#) chi (Z,Z)) = dom chi(Z,Z) by VALUED_1:def 5
.= Z by FUNCT_3:def 3
.= dom f by PARTFUN1:def 2;
thus for z be object st z in dom f holds f.z = (r (#) chi(Z,Z)).z
proof
let z be object;
assume
A4: z in dom f;
then (r (#) chi(Z,Z)).z = r * (chi(Z,Z).z) by A3BIS,VALUED_1:def 5
.= r * 1 by A4,FUNCT_3:def 3
.= f.z by A3,A1,A4,A2;
hence thesis;
end;
end;
hence f = r (#) chi(Z,Z);
end;
assume ex r be Real st f = r (#) chi(Z,Z);
then consider r be Real such that
A5: f = r (#) chi(Z,Z);
for x,y be object st x in dom f & y in dom f holds f.x = f.y
proof
let x,y be object;
assume that
A6: x in dom f and
A7: y in dom f;
f.x = r * (chi(Z,Z).x) by A5,A6,VALUED_1:def 5
.= r * 1 by A6,FUNCT_3:def 3
.= r * (chi(Z,Z).y) by A7,FUNCT_3:def 3
.= f.y by A5,A7,VALUED_1:def 5;
hence thesis;
end;
hence f is constant;
end;
theorem Th17:
chi(X,X) is positive-yielding
proof
now
let r be Real;
assume
A1: r in rng chi(X,X);
r <> 0
proof
assume
A2: r = 0;
ex s be Element of X st s in dom chi(X,X) & r = (chi(X,X)).s
by A1,PARTFUN1:3;
hence contradiction by A2,FUNCT_3:def 3;
end;
hence 0 < r by A1;
end;
hence thesis by PARTFUN3:def 1;
end;
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 Th18:
f is lower_integrable implies lower_sum(f,D) <= lower_integral(f)
proof
assume f is lower_integrable;
then
A1: rng lower_sum_set(f) is bounded_above by INTEGRA1:def 13;
set r = lower_integral(f);
r = upper_bound rng lower_sum_set(f) by INTEGRA1:def 15;
then
A2: for s be Real st s in rng lower_sum_set(f) holds s <= r by A1,SEQ_4:def 1;
A3: dom lower_sum_set(f) = divs I by PARTFUN1:def 2;
D in divs I by INTEGRA1:def 3;
then (lower_sum_set(f)).D <= r by A3,A2,FUNCT_1:3;
hence thesis by INTEGRA1:def 11;
end;
theorem Th19:
f is upper_integrable implies upper_integral(f) <= upper_sum(f,D)
proof
assume f is upper_integrable;
then
A1: rng upper_sum_set(f) is bounded_below by INTEGRA1:def 12;
set r = upper_integral(f);
r = lower_bound rng upper_sum_set(f) by INTEGRA1:def 14;
then
A2: for s be Real st s in rng upper_sum_set(f) holds r <= s by A1,SEQ_4:def 2;
A3: dom upper_sum_set(f) = divs I by PARTFUN1:def 2;
D in divs I by INTEGRA1:def 3;
then r <= (upper_sum_set(f)).D by A3,A2,FUNCT_1:3;
hence thesis by INTEGRA1:def 10;
end;
definition
let A be non empty closed_interval Subset of REAL;
func tagged_divs A -> set means :Def1:
for x being set holds (x in it iff x is tagged_division of A);
existence
proof
defpred P[set] means $1 is tagged_division of A;
consider R be set such that
A1: for x be set holds (x in R iff x in [: bool [:NAT,REAL:], REAL* :] & P[x])
from XFAMILY:sch 1;
take R;
let x be set;
thus x in R implies x is tagged_division of A by A1;
assume x is tagged_division of A;
then reconsider p = x as tagged_division of A;
consider D be Division of A,
T be Element of set_of_tagged_Division(D) such that
A2: p = [D,T] by COUSIN:def 3;
[D,T] in [: bool [:NAT,REAL:],REAL* :] by ZFMISC_1:87;
hence thesis by A1,A2;
end;
uniqueness
proof
let D1,D2 be set such that
A3: for x be set holds (x in D1 iff x is tagged_division of A) and
A4: for x be set holds (x in D2 iff x is tagged_division of A);
for x be object holds x in D1 iff x in D2 by A3,A4;
hence thesis by TARSKI:2;
end;
end;
registration
let A be non empty closed_interval Subset of REAL;
cluster tagged_divs A -> non empty;
coherence
proof
reconsider TD = the tagged_division of A as set by TARSKI:1;
TD in tagged_divs A by Def1;
hence thesis;
end;
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
:Def2:
ex D being Division of A, T being Element of set_of_tagged_Division(D) st
it = T & TD = [D,T];
existence
proof
consider D be Division of A,
T be Element of set_of_tagged_Division(D) such that
A1: TD = [D,T] by COUSIN:def 3;
ex s being non empty non-decreasing FinSequence of REAL st T = s &
dom s = dom D &
for i being Nat st i in dom s holds s.i in divset(D,i) by COUSIN:def 2;
hence thesis by A1;
end;
uniqueness by XTUPLE_0:1;
end;
theorem Th20:
TD = [D,T] implies T = tagged_of TD &
D = division_of TD
proof
assume
A1: TD = [D,T];
ex D1 be Division of I, T1 be Element of set_of_tagged_Division(D1) st
tagged_of(TD) = T1 & TD = [D1,T1] by Def2;
hence thesis by A1,XTUPLE_0:1,COUSIN:def 6;
end;
theorem Th21:
len tagged_of TD = len division_of TD
proof
consider D be Division of I,
T be Element of set_of_tagged_Division(D) such that
A1: TD = [D,T] by COUSIN:def 3;
consider s be non empty non-decreasing FinSequence of REAL such that
A2: T = s and
A3: dom s = dom D and
for i being Nat st i in dom s holds s.i in divset(D,i) by COUSIN:def 2;
tagged_of(TD) = T & division_of(TD) = D by A1,Th20;
hence thesis by A2,A3,FINSEQ_3:29;
end;
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
len division_of TD;
coherence;
func dom TD -> set equals
dom division_of TD;
coherence;
end;
theorem Th22:
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
proof
let I be non empty closed_interval Subset of REAL,
D be Division of I, T be Element of set_of_tagged_Division(D);
consider s be non empty non-decreasing FinSequence of REAL such that
A1: T = s & dom s = dom D &
for i be Nat st i in dom s holds s.i in divset(D,i) by COUSIN:def 2;
now
let x be object;
assume x in rng T;
then consider y be object such that
A2: y in dom T and
A3: x = T.y by FUNCT_1:def 3;
reconsider y as Nat by A2;
divset(D,y) c= I by A1,A2,INTEGRA1:8;
hence x in I by A3,A1,A2;
end;
hence thesis;
end;
theorem Th23:
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
proof
let I be non empty closed_interval Subset of REAL;
let jauge1,jauge2 be positive-yielding Function of I,REAL;
let TD be jauge1-fine tagged_division of I;
assume
A1: jauge1 <= jauge2;
consider D be Division of I,
T be Element of set_of_tagged_Division(D) such that
A2: TD = [D,T] and
A3: for i be Nat st i in dom D holds vol divset(D,i) <= jauge1.(T.i)
by COUSIN:def 4;
now
let i be Nat;
assume
A4: i in dom D;
then
A5: vol divset(D,i) <= jauge1.(T.i) by A3;
dom T = Seg len T by FINSEQ_1:def 3
.= Seg len tagged_of TD by A2,Th20
.= Seg len division_of TD by Th21
.= Seg len D by A2,Th20
.= dom D by FINSEQ_1:def 3; then
A6: T.i in rng T by A4,FUNCT_1:3;
rng T c= I by Th22;
then jauge1.(T.i) <= jauge2.(T.i) by A6,A1;
hence vol divset(D,i) <= jauge2.(T.i) by A5,XXREAL_0:2;
end;
hence thesis by A2,COUSIN:def 4;
end;
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 :Def4:
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));
existence
proof
deffunc F(Nat)=
In(f.((tagged_of(TD)).$1) * vol(divset(division_of(TD),$1)),REAL);
consider IT being FinSequence of REAL such that
A1: len IT = len (division_of TD) & for i be Nat st i in dom IT holds
IT.i=F(i) from FINSEQ_2:sch 1;
take IT;
thus len IT = len TD by A1;
let i be Nat;
A2: F(i)= f.((tagged_of(TD)).i) * vol(divset(division_of(TD),i));
assume i in dom TD;
then i in Seg len division_of TD by FINSEQ_1:def 3;
then i in dom IT by A1,FINSEQ_1:def 3;
hence thesis by A1,A2;
end;
uniqueness
proof
let s1,s2 be FinSequence of REAL such that
A3: len s1 = len TD and
A4: for i be Nat st i in dom TD holds
s1.i = f.((tagged_of(TD)).i) * vol(divset(division_of(TD),i)) and
A5: len s2 = len TD and
A6: for i be Nat st i in dom TD holds
s2.i = f.((tagged_of(TD)).i) * vol(divset(division_of(TD),i));
A7: dom s1 = dom TD by A3,FINSEQ_3:29;
for i be Nat st i in dom s1 holds s1.i = s2.i
proof
let i be Nat;
assume
A8: i in dom s1;
then s1.i = f.((tagged_of(TD)).i) * vol(divset(division_of(TD),i))
by A4,A7;
hence thesis by A6,A7,A8;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
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 Sum tagged_volume(f,TD);
coherence;
end;
theorem Th24:
Y c= X implies chi(X,Y) = chi(Y,Y)
proof
assume
A1: Y c= X;
now
thus dom chi(X,Y) = Y by FUNCT_3:def 3
.= dom chi(Y,Y) by FUNCT_3:def 3;
hereby
let x be object;
assume
A2: x in dom chi(X,Y);
then x in Y & x in X by A1;
hence (chi(X,Y)).x = 1 by FUNCT_3:def 3
.= (chi(Y,Y)).x by A2,FUNCT_3:def 3;
end;
end;
hence thesis;
end;
reserve f for Function of I,REAL;
theorem Th25:
I is non empty trivial implies vol I = 0
proof
assume I is non empty trivial;
then consider x be object such that
A1: I = {x} by ZFMISC_1:131;
x in I by A1,TARSKI:def 1;
then reconsider x as Real;
vol {x} = 0 by COUSIN:41;
hence thesis by A1;
end;
theorem Th26:
for r being Real st I = {r} holds
(for D being Division of I holds D = <* r *> )
proof
let r be Real;
assume
A1: I = {r};
A2: I = [.r,r.] by A1,XXREAL_1:17;
let D be Division of I;
len D = 1
proof
assume 1 <> len D;
then 2 <= len D by NAT_1:23;
then 1 <= len D & 1 <= 2 <= len D by XXREAL_0:2;
then
A3: 1 in dom D & 2 in dom D by FINSEQ_3:25;
then D.1 in I & D.2 in I by INTEGRA1:6;
then D.1 = r & D.2 = r by A1,TARSKI:def 1;
hence contradiction by A3,VALUED_0:def 13;
end;
hence thesis by A2,COUSIN:64;
end;
Lm04:
f = chi(I,I) implies tagged_sum(f,TD) = vol I
proof
assume
A1: f = chi(I,I);
A2: for i be Nat st i in dom TD holds
tagged_volume(f,TD).i = vol divset(division_of TD,i)
proof
let i be Nat;
assume
A3: i in dom TD;
consider D be Division of I,
T be Element of set_of_tagged_Division(D) such that
A4: tagged_of TD = T and
A5: TD = [D,T] by Def2;
A6: i in dom D by A3,Th20,A5;
A7: dom T = Seg len tagged_of TD by A4,FINSEQ_1:def 3
.= Seg len division_of TD by Th21
.= Seg len D by A5,Th20
.= dom D by FINSEQ_1:def 3;
rng T c= I by Th22;
then T.i in I by A7,A6,FUNCT_1:3;
then f.((tagged_of TD).i) = 1 by A4,A1,FUNCT_3:def 3;
then tagged_volume(f,TD).i = 1 * vol(divset(division_of TD,i)) by Def4,A3
.= vol(divset(division_of TD,i));
hence thesis;
end;
T1: dom tagged_volume(f,TD) = Seg len tagged_volume(f,TD) by FINSEQ_1:def 3
.= Seg len TD by Def4
.= Seg len division_of TD;
Seg len division_of TD = dom division_of TD by FINSEQ_1:def 3;
hence thesis by INTEGR20:6,T1,A2;
end;
definition
let I be non empty closed_interval Subset of REAL;
let f be Function of I,REAL;
attr f is HK-integrable means
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
A1: f is HK-integrable;
func HK-integral f -> Real means :DEFCC:
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;
existence by A1;
uniqueness
proof
let J1,J2 be Real such that
A2: for epsilon be Real st epsilon > 0 holds
ex jauge be positive-yielding Function of I,REAL st
for TD be tagged_division of I st TD is jauge-fine
holds |.tagged_sum(f,TD) - J1.| <= epsilon and
A3: for epsilon be Real st epsilon > 0 holds
ex jauge be positive-yielding Function of I,REAL st
for TD be tagged_division of I st TD is jauge-fine
holds |.tagged_sum(f,TD) - J2.| <= epsilon;
now
let epsilon be Real;
assume
A4: epsilon > 0;
reconsider e = epsilon / 2 as Real;
consider jauge1 be positive-yielding Function of I,REAL such that
A5: for TD be tagged_division of I st TD is jauge1-fine
holds |.tagged_sum(f,TD) - J1.| <= e by A4,A2;
consider jauge2 be positive-yielding Function of I,REAL such that
A6: for TD be tagged_division of I st TD is jauge2-fine
holds |.tagged_sum(f,TD) - J2.| <= e by A3,A4;
reconsider jauge = min(jauge1,jauge2)
as positive-yielding Function of I,REAL;
consider TD be tagged_division of I such that
A7: TD is jauge-fine by COUSIN:68;
TD is jauge1-fine & TD is jauge2-fine by A7,Th23,Th08;
then |.tagged_sum(f,TD) - J1.| <= e &
|.tagged_sum(f,TD) - J2.| <= e by A5,A6;
then
A8: |.J1 - tagged_sum(f,TD).| <= e &
|.J2 - tagged_sum(f,TD).| <= e by COMPLEX1:60;
|. (J1 - tagged_sum(f,TD)) - (J2 - tagged_sum(f,TD)) .|
<= |.J1 - tagged_sum(f,TD).| + |. J2 - tagged_sum(f,TD) .|
by COMPLEX1:57;
then |.J1 - J2.| <= e + |.J2 - tagged_sum(f,TD) .| by A8,Lm01;
then |.J1 - J2.| <= e + e by A8,Lm01;
hence |.J1 - J2.| <= epsilon;
end;
hence thesis by Th04;
end;
end;
theorem Th27:
for f being Function of I,REAL st I is trivial holds
f is HK-integrable & HK-integral(f) = 0
proof
let f be Function of I,REAL;
assume
A1: I is trivial;
reconsider J = 0 as Real;
A2: now
let epsilon be Real;
assume
A3: epsilon > 0;
reconsider jauge = chi(I,I) as positive-yielding Function of I,REAL
by Th17,Th11;
take jauge;
thus for TD be tagged_division of I st TD is jauge-fine holds
|.tagged_sum(f,TD) - J.| <= epsilon
proof
let TD be tagged_division of I;
assume TD is jauge-fine;
consider x be object such that
A4: I = {x} by A1,ZFMISC_1:131;
x in I by A4,TARSKI:def 1;
then reconsider x as Real;
A4Bis: division_of TD = <* x *> by A4,Th26;
A5: len tagged_volume(f,TD) = len TD &
for i be Nat st i in dom TD holds
tagged_volume(f,TD).i = f.((tagged_of TD).i)
* vol(divset(division_of TD,i)) by Def4;
A6: tagged_volume(f,TD).1
= f.((tagged_of TD).1) * vol(divset(division_of TD,1))
by A5,FINSEQ_5:6;
divset(division_of TD,1) = [. lower_bound I, (division_of TD).1 .]
by COUSIN:50
.= [. x,(division_of TD).1 .] by A4,SEQ_4:9
.= [. x,x .] by A4Bis
.= {x} by XXREAL_1:17;
then
A7: vol divset(division_of TD,1) = 0 by COUSIN:41;
len tagged_volume(f,TD) = len TD by Def4
.= 1 by A4Bis,FINSEQ_1:40;
then tagged_volume(f,TD) = <* tagged_volume(f,TD).1 *>
by FINSEQ_1:40;
then Sum tagged_volume(f,TD) = 0 by A6,A7,RVSUM_1:73;
hence thesis by A3;
end;
end;
then f is HK-integrable;
hence thesis by A2,DEFCC;
end;
theorem Th28:
A misses I & f = chi(A,I) implies tagged_sum(f,TD) = 0
proof
assume that
A1: A misses I and
A2: f = chi(A,I);
A3: dom tagged_volume(f,TD) = Seg len tagged_volume(f,TD) by FINSEQ_1:def 3
.= Seg len TD by Def4
.= dom TD by FINSEQ_1:def 3;
for i be Nat st i in dom TD holds tagged_volume(f,TD).i = 0
proof
let i be Nat;
assume
A4: i in dom TD;
consider D be Division of I,
T be Element of set_of_tagged_Division(D) such that
A5: tagged_of TD = T and
A6: TD = [D,T] by Def2;
A7: i in dom D by A4,Th20,A6;
A8: dom T = Seg len tagged_of TD by A5,FINSEQ_1:def 3
.= Seg len division_of TD by Th21
.= Seg len D by A6,Th20
.= dom D by FINSEQ_1:def 3;
rng T c= I by Th22;
then T.i in I by A8,A7,FUNCT_1:3;
then f.((tagged_of TD).i) = 0 by A1,A5,A2,Th15;
then tagged_volume(f,TD).i = 0 * vol(divset(division_of TD,i)) by Def4,A4
.= 0;
hence thesis;
end;
then for k be object st k in dom tagged_volume(f,TD) holds
(tagged_volume(f,TD)).k = 0 by A3;
then Sum tagged_volume(f,TD) = Sum ((len tagged_volume(f,TD)) |-> 0)
by INTEGR23:5
.= 0 by RVSUM_1:81;
hence thesis;
end;
theorem Th29:
A misses I & f = chi(A,I) implies f is HK-integrable & HK-integral(f) = 0
proof
assume that
A1: A misses I and
A2: f = chi(A,I);
reconsider J = 0 as Real;
A3: now
let epsilon be Real;
assume
A4: epsilon > 0;
reconsider jauge = chi(I,I) as Function of I,REAL by Th11;
now
let r be Real;
assume r in rng jauge;
then r in {1} by INTEGRA1:17;
hence 0 < r;
end;
then reconsider jauge as positive-yielding Function of I,REAL
by PARTFUN3:def 1;
now
take jauge;
hereby
let TD be tagged_division of I;
assume TD is jauge-fine;
|.tagged_sum(f,TD) - J.| = |.0.| by A1,A2,Th28
.= 0;
hence |.tagged_sum(f,TD) - J.| <= epsilon by A4;
end;
end;
hence 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;
then f is HK-integrable;
hence thesis by A3,DEFCC;
end;
theorem Th30:
I c= A & f = chi(A,I) implies f is HK-integrable & HK-integral(f) = vol(I)
proof
assume that
A1: I c= A and
A2: f = chi(A,I);
reconsider J = vol(I) as Real;
A3: now
let epsilon be Real;
assume
A4: epsilon > 0;
reconsider jauge = chi(I,I) as Function of I,REAL by Th11;
now
let r be Real;
assume r in rng jauge;
then r in {1} by INTEGRA1:17;
hence 0 < r;
end;
then reconsider jauge as positive-yielding Function of I,REAL
by PARTFUN3:def 1;
now
take jauge;
hereby
let TD be tagged_division of I;
assume TD is jauge-fine;
f = chi(I,I) by A1,A2,Th24;
then tagged_sum(f,TD) = vol I by Lm04;
hence |.tagged_sum(f,TD) - J.| <= epsilon by A4;
end;
end;
hence 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;
then f is HK-integrable;
hence thesis by A3,DEFCC;
end;
registration
let I be non empty closed_interval Subset of REAL;
cluster HK-integrable for Function of I,REAL;
existence
proof
reconsider f = chi(REAL \ I,I) as Function of I,REAL by Th11;
take f;
REAL \ I misses I by XBOOLE_1:79;
hence f is HK-integrable by Th29;
end;
end;
begin :: Linearity of jauge-integrale
reserve f,g for HK-integrable Function of I,REAL,
r for Real;
theorem Th31:
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))
proof
let i be Nat;
assume i in dom TD;
then (tagged_volume(r(#)f,TD)).i
= (r (#) f).((tagged_of TD).i) * vol(divset(division_of TD,i)) by Def4;
hence thesis by VALUED_1:6;
end;
theorem Th32:
tagged_volume(r(#)f,TD) = r * tagged_volume(f,TD)
proof
Z1: len (r * tagged_volume(f,TD)) = len tagged_volume(f,TD)
by RVSUM_1:117
.= len TD by Def4
.= len tagged_volume(r(#)f,TD) by Def4;
for i be Nat st i in dom tagged_volume(r(#)f,TD) holds
(tagged_volume(r(#)f,TD)).i = (r * tagged_volume(f,TD)).i
proof
let i be Nat;
assume i in dom tagged_volume(r(#)f,TD);
then i in Seg len tagged_volume(r(#)f,TD) by FINSEQ_1:def 3;
then i in Seg len TD by Def4; then
A1: i in dom TD by FINSEQ_1:def 3;
then (tagged_volume(r(#)f,TD)).i
= r * f.((tagged_of TD).i) * vol(divset(division_of TD,i)) by Th31
.= r * (f.((tagged_of TD).i) * vol(divset(division_of TD,i)))
.= r * (tagged_volume(f,TD)).i by A1,Def4;
hence thesis by RVSUM_1:45;
end;
hence thesis by FINSEQ_2:9,Z1;
end;
theorem Th33:
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))
proof
let i be Nat;
assume
A1: i in dom TD;
consider D be Division of I,
T be Element of set_of_tagged_Division(D) such that
A2: tagged_of TD = T and
A3: TD = [D,T] by Def2;
A4: i in dom D by A1,Th20,A3;
A5: dom T = Seg len tagged_of TD by A2,FINSEQ_1:def 3
.= Seg len division_of TD by Th21
.= Seg len D by A3,Th20
.= dom D by FINSEQ_1:def 3;
rng T c= I by Th22;
then reconsider c = (tagged_of TD).i as Element of I
by A2,A4,A5,FUNCT_1:3;
(tagged_volume(f + g,TD)).i = (f + g).c * vol(divset(division_of TD,i))
by A1,Def4
.= (f.c + g.c) * vol(divset(division_of TD,i))
by VALUED_1:1;
hence thesis;
end;
theorem Th34:
tagged_volume(f + g,TD) = tagged_volume(f,TD) + tagged_volume(g,TD)
proof
len tagged_volume(f,TD) = len TD &
len tagged_volume(g,TD) = len TD by Def4;
then reconsider R1 = tagged_volume(f,TD),
R2 = tagged_volume(g,TD)
as Element of len TD-tuples_on REAL by FINSEQ_2:92;
len tagged_volume(f,TD) = len TD by Def4
.= len tagged_volume(g,TD) by Def4; then
Z1: len (tagged_volume(f,TD) + tagged_volume(g,TD))
= len tagged_volume(f,TD) by RVSUM_1:115
.= len TD by Def4
.= len tagged_volume(f + g,TD) by Def4;
for i be Nat st i in dom tagged_volume(f + g,TD) holds
(tagged_volume(f + g,TD)).i
= ((tagged_volume(f,TD)) + tagged_volume(g,TD)).i
proof
let i be Nat;
assume i in dom tagged_volume(f + g,TD);
then i in Seg len tagged_volume(f + g,TD) by FINSEQ_1:def 3;
then i in Seg len TD by Def4;
then
A1: i in dom TD by FINSEQ_1:def 3;
then (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)) by Th33
.= tagged_volume(f,TD).i + g.((tagged_of TD).i)
* vol(divset(division_of TD,i)) by A1,Def4
.= R1.i + R2.i by A1,Def4
.= (tagged_volume(f,TD) + tagged_volume(g,TD)).i by RVSUM_1:11;
hence thesis;
end;
hence thesis by FINSEQ_2:9,Z1;
end;
theorem Th35:
f is HK-integrable implies
r (#) f is HK-integrable Function of I,REAL &
HK-integral (r (#) f) = r * HK-integral f
proof
assume f is HK-integrable;
then consider J being Real such that
A1: 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;
A2: 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(r (#) f,TD) - (r * J).| <= epsilon
proof
per cases;
suppose
A3: r = 0;
let epsilon be Real;
assume
A4: epsilon > 0;
set jauge = the positive-yielding Function of I,REAL;
take jauge;
for TD be tagged_division of I st TD is jauge-fine
holds |.tagged_sum(r (#) f,TD) - (r * J).| <= epsilon
proof
let TD be tagged_division of I;
assume TD is jauge-fine;
tagged_sum(r (#) f,TD) = Sum (r * tagged_volume(f,TD)) by Th32
.= r * Sum tagged_volume(f,TD) by RVSUM_1:87
.= 0 by A3;
hence |.tagged_sum(r (#) f,TD) - (r * J).| <= epsilon by A3,A4;
end;
hence thesis;
end;
suppose
A5: r <> 0;
let epsilon be Real;
assume
A6: epsilon > 0;
set e = epsilon / |. r .|;
consider jauge be positive-yielding Function of I,REAL such that
A7: for TD be tagged_division of I st TD is jauge-fine
holds |.tagged_sum(f,TD) - J.| <= e by A1,A5,A6;
take jauge;
for TD being tagged_division of I st TD is jauge-fine
holds |.tagged_sum(r (#) f,TD) - r * J.| <= epsilon
proof
let TD be tagged_division of I;
assume
A8: TD is jauge-fine;
|. r * tagged_sum(f,TD) - r * J.|
= |. r * (tagged_sum(f,TD) - J).|
.= |.r.| * |. tagged_sum(f,TD) - J.| by COMPLEX1:65;
then z1: |. r * tagged_sum(f,TD) - r * J.| <= |.r.| * e
by A7,A8,XREAL_1:64;
tagged_sum(r (#) f,TD)
= Sum (r * tagged_volume(f,TD)) by Th32
.= r * tagged_sum(f,TD) by RVSUM_1:87;
hence thesis by z1,A5,XCMPLX_1:87;
end;
hence thesis;
end;
end;
then
A9: r (#) f is HK-integrable;
then HK-integral (r (#) f) = r * J by A2,DEFCC
.= r * HK-integral f by A1,DEFCC;
hence thesis by A9;
end;
theorem
f + g is HK-integrable Function of I,REAL &
HK-integral (f + g) = HK-integral f + HK-integral g
proof
f is HK-integrable;
then consider J1 being Real such that
A1: 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) - J1.| <= epsilon;
g is HK-integrable;
then consider J2 being Real such that
A2: 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(g,TD) - J2.| <= epsilon;
A3: HK-integral g = J2 by A2,DEFCC;
A4: 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 + g,TD) - (J1 + J2).| <= epsilon
proof
let epsilon be Real;
assume
A5: epsilon > 0;
set e = epsilon / 2;
consider jauge1 be positive-yielding Function of I,REAL such that
A6: for TD being tagged_division of I st TD is jauge1-fine
holds |.tagged_sum(f,TD) - J1.| <= epsilon / 2 by A5,A1;
consider jauge2 be positive-yielding Function of I,REAL such that
A7: for TD being tagged_division of I st TD is jauge2-fine
holds |.tagged_sum(g,TD) - J2.| <= epsilon / 2 by A5,A2;
reconsider jauge = min(jauge1,jauge2) as
positive-yielding Function of I,REAL;
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 + g,TD) - (J1 + J2).| <= epsilon
proof
take jauge;
for TD being tagged_division of I st TD is jauge-fine
holds |.tagged_sum(f + g,TD) - (J1 + J2).| <= epsilon
proof
let TD be tagged_division of I;
assume TD is jauge-fine;
then
A8: TD is jauge1-fine & TD is jauge2-fine by Th23,Th08;
len tagged_volume(f,TD) = len TD &
len tagged_volume(g,TD) = len TD by Def4;
then reconsider R1 = tagged_volume(f,TD),
R2 = tagged_volume(g,TD)
as Element of len TD-tuples_on REAL
by FINSEQ_2:92;
tagged_sum(f + g,TD)
= Sum (tagged_volume(f,TD) + tagged_volume(g,TD)) by Th34
.= Sum R1 + Sum R2 by RVSUM_1:89
.= tagged_sum(f,TD) + tagged_sum(g,TD);
then tagged_sum(f + g,TD) - (J1 + J2)
= (tagged_sum(f,TD) - J1) + (tagged_sum(g,TD) - J2);
then |.tagged_sum(f + g,TD) - (J1 + J2).|
<= |.tagged_sum(f,TD) - J1.| + |.tagged_sum(g,TD) - J2.|
by COMPLEX1:56;
then |.tagged_sum(f + g,TD) - (J1 + J2).|
<= epsilon / 2 + |.tagged_sum(g,TD) - J2.| by A8,A6,Lm01;
then |.tagged_sum(f + g,TD) - (J1 + J2).|
<= epsilon / 2 + epsilon / 2 by A8,A7,Lm01;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
then
A9: f + g is HK-integrable;
then HK-integral(f + g) = J1 + J2 by A4,DEFCC
.= (HK-integral f) + (HK-integral g) by A1,DEFCC,A3;
hence thesis by A9;
end;
theorem Th36:
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))
proof
let f be Function of I,REAL;
assume f is constant;
then consider r be Real such that
A1: f = r (#) chi(I,I) by Th16;
reconsider g = chi(I,I) as Function of I,REAL by Th11;
A2: g is HK-integrable & HK-integral(g) = vol(I) by Th30;
hence f is HK-integrable by A1,Th35;
take r;
thus thesis by A1,A2,Th35;
end;
begin :: integrable + bounded -> HK-integrable
registration
let I being non empty closed_interval Subset of REAL;
cluster integrable for Function of I,REAL;
existence
proof
reconsider f = chi(I,I) as PartFunc of I,REAL by Th11;
f is integrable by INTEGRA4:2;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster bounded for Function of X,REAL;
existence
proof
reconsider f = chi(X,X) as PartFunc of X,REAL by Th11;
f is bounded by Th14;
hence thesis;
end;
end;
theorem Th37:
for f being bounded Function of I,REAL holds
|. upper_bound (rng f) - lower_bound (rng f) .| = 0 iff f is constant
proof
let f be bounded Function of I,REAL;
A1: rng f is real-bounded by INTEGRA1:15;
hereby
assume |. upper_bound (rng f) - lower_bound (rng f) .| = 0;
then upper_bound (rng f) - lower_bound (rng f) = 0;
then ex r be Real st rng f = {r} by A1,Th10;
hence f is constant;
end;
assume f is constant;
then consider y be Element of REAL such that
A2: rng f = {y} by FUNCT_2:111;
upper_bound rng f = y & lower_bound rng f = y by A2,SEQ_4:9;
hence |. upper_bound (rng f) - lower_bound (rng f) .| = 0;
end;
registration
let I be non empty closed_interval Subset of REAL;
cluster bounded for integrable Function of I,REAL;
existence
proof
reconsider f = chi(I,I) as PartFunc of I,REAL by Th11;
reconsider f as integrable Function of I,REAL by INTEGRA4:2;
f is bounded by Th14;
hence thesis;
end;
end;
theorem
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)
proof
let f be PartFunc of I,REAL;
assume f is upper_integrable;
then rng upper_sum_set(f) is bounded_below by INTEGRA1:def 12;
then consider r be Real such that
A1: for y being object st y in dom upper_sum_set(f) holds
r < (upper_sum_set(f)).y by INTEGRA1:12,SEQ_2:def 2;
A2: dom upper_sum_set(f) = divs I by FUNCT_2:def 1;
take r;
let D be Division of I;
D in divs(I) by INTEGRA1:def 3;
then r < (upper_sum_set(f)).D by A1,A2;
hence thesis by INTEGRA1:def 10;
end;
theorem
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
proof
let f be PartFunc of I,REAL;
assume f is lower_integrable;
then rng lower_sum_set(f) is bounded_above by INTEGRA1:def 13;
then consider r be Real such that
A1: for y being object st y in dom lower_sum_set(f) holds
(lower_sum_set(f)).y < r by INTEGRA1:14,SEQ_2:def 1;
A2: dom lower_sum_set(f) = divs I by FUNCT_2:def 1;
take r;
let D be Division of I;
D in divs(I) by INTEGRA1:def 3;
then (lower_sum_set(f)).D < r by A1,A2;
hence thesis by INTEGRA1:def 11;
end;
theorem Th38:
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)
proof
let f be Function of I,REAL;
let D,D1 be Division of I;
assume that
A1: D.1 = lower_bound I and
A2: D1 = D/^1;
D = <*D/.1*>^(D/^1) by FINSEQ_5:29;
then
A4: D = <*D.1*>^(D/^1) by FINSEQ_5:6,PARTFUN1:def 6;
A5: (upper_volume(f,D)).1 = 0
proof
divset(D,1) = [.D.1,D.1.] by A1,COUSIN:50;
then lower_bound divset(D,1) = D.1 &
upper_bound divset(D,1) = D.1 by JORDAN5A:19;
then
A6: vol divset(D,1) = D.1 - D.1 by INTEGRA1:def 5
.= 0;
1 in dom D by FINSEQ_5:6;
then (upper_volume(f,D)).1 = upper_bound rng (f|divset(D,1))
* vol divset(D,1) by INTEGRA1:def 6
.= 0 by A6;
hence thesis;
end;
0 < len upper_volume(f,D);
then Sum upper_volume(f,D)
= (upper_volume(f,D)).1 + Sum (upper_volume(f,D)/^1) by IRRAT_1:17
.= Sum (upper_volume(f,D1)) by A4,A1,A2,INTEGRA3:13,A5
.= upper_sum(f,D1) by INTEGRA1:def 8;
hence upper_sum(f,D1) = upper_sum(f,D) by INTEGRA1:def 8;
A7: (lower_volume(f,D)).1 = 0
proof
divset(D,1) = [.D.1,D.1.] by A1,COUSIN:50;
then lower_bound divset(D,1) = D.1 &
upper_bound divset(D,1) = D.1 by JORDAN5A:19;
then
A8: vol divset(D,1) = D.1 - D.1 by INTEGRA1:def 5
.= 0;
1 in dom D by FINSEQ_5:6;
then (lower_volume(f,D)).1
= lower_bound rng (f|divset(D,1)) * vol divset(D,1) by INTEGRA1:def 7
.= 0 by A8;
hence thesis;
end;
0 < len lower_volume(f,D);
then Sum lower_volume(f,D)
= (lower_volume(f,D)).1 + Sum (lower_volume(f,D)/^1) by IRRAT_1:17
.= Sum (lower_volume(f,D1)) by A4,A1,A2,INTEGRA3:13,A7
.= lower_sum(f,D1) by INTEGRA1:def 9;
hence thesis by INTEGRA1:def 9;
end;
reserve f for bounded integrable Function of I,REAL;
theorem Th39:
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
proof
let i be Nat;
assume
A1: i in dom TD;
set a = (lower_volume(f,division_of TD)).i,
b = (tagged_volume(f,TD)).i,
c = (upper_volume(f,division_of TD)).i;
reconsider D = division_of TD as Division of I;
set x = (tagged_of TD).i;
consider D9 be Division of I,
T9 be Element of set_of_tagged_Division(D9) such that
A2: tagged_of TD = T9 & TD = [D9,T9] by Def2;
A3: D = D9 & x = T9.i by A2,Th20;
consider s be non empty non-decreasing FinSequence of REAL such that
A4: T9 = s & dom s = dom D9 &
for i be Nat st i in dom s holds s.i in divset(D9,i) by COUSIN:def 2;
divset(D,i) c= I by A1,INTEGRA1:8;
then x in I by A1,A3,A4;
then
A5: x in dom f by FUNCT_2:def 1;
then reconsider y = f.x as Element of REAL by PARTFUN1:4;
f/.x in rng (f|divset(D,i)) by A1,A3,A4,A5,PARTFUN2:18; then
W1: f.x in rng (f|divset(D,i)) by A5,PARTFUN1:def 6;
rng f is bounded_below by INTEGRA1:11; then
rng (f|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44; then
W3: (lower_bound rng (f|divset(D,i))) <= f.((tagged_of TD).i)
by SEQ_4:def 2,W1;
0 <= vol divset(D,i) by INTEGRA1:9;
then (lower_bound rng (f|divset(D,i)))*vol divset(D,i)
<= f.((tagged_of TD).i) * vol(divset(division_of TD,i))
by XREAL_1:64,W3;
then (lower_volume(f,D)).i
<= f.((tagged_of TD).i) * vol(divset(division_of TD,i))
by A1,INTEGRA1:def 7;
hence a <= b by A1,Def4;
f/.x in rng (f|divset(D,i)) by A1,A3,A4,A5,PARTFUN2:18; then
T2: f.x in rng (f|divset(D,i)) by A5,PARTFUN1:def 6;
rng f is bounded_above by INTEGRA1:13; then
rng (f|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43; then
W1: f.((tagged_of TD).i) <= (upper_bound rng (f|divset(D,i)))
by SEQ_4:def 1,T2;
0 <= vol divset(D,i) by INTEGRA1:9;
then f.((tagged_of TD).i) * vol(divset(division_of TD,i))
<= (upper_bound rng (f|divset(D,i))) * vol divset(D,i) by W1,XREAL_1:64;
then f.((tagged_of TD).i) * vol(divset(division_of TD,i))
<= (upper_volume(f,D)).i by A1,INTEGRA1:def 6;
hence b <= c by A1,Def4;
end;
theorem Th40:
Sum lower_volume(f,division_of TD) <= Sum tagged_volume(f,TD)
<= Sum upper_volume(f,division_of TD)
proof
A1: len tagged_volume(f,TD) = len TD by Def4
.= len lower_volume(f,division_of TD)
by INTEGRA1:def 7;
dom TD = Seg len division_of TD by FINSEQ_1:def 3
.= Seg len lower_volume(f,division_of TD) by INTEGRA1:def 7
.= dom lower_volume(f,division_of TD) by FINSEQ_1:def 3; then
for i be Element of NAT st
i in dom lower_volume(f,division_of TD) holds
(lower_volume(f,division_of TD)).i <= (tagged_volume(f,TD)).i
by Th39;
hence Sum lower_volume(f,division_of TD) <= Sum tagged_volume(f,TD)
by INTEGRA5:3,A1;
B1: len tagged_volume(f,TD) = len TD by Def4
.= len upper_volume(f,division_of TD)
by INTEGRA1:def 6;
dom TD = Seg len TD by FINSEQ_1:def 3
.= Seg len tagged_volume(f,TD) by Def4
.= dom tagged_volume(f,TD) by FINSEQ_1:def 3; then
for i be Element of NAT st i in dom tagged_volume(f,TD) holds
(tagged_volume(f,TD)).i <= (upper_volume(f,division_of TD)).i
by Th39;
hence Sum tagged_volume(f,TD) <= Sum upper_volume(f,division_of TD)
by INTEGRA5:3,B1;
end;
theorem Th41:
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
proof
let epsilon be Real;
assume that
A1: I is non trivial and
A4: 0 < epsilon;
set J = integral(f);
A6: rng lower_sum_set f is bounded_above by INTEGRA1:def 13,def 16;
A7: lower_integral f = upper_integral f by INTEGRA1:def 16;
A8: lower_integral f = upper_bound rng lower_sum_set f
by INTEGRA1:def 15;
set X = rng lower_sum_set f;
set e = epsilon / 2;
consider ru be Real such that
A10: ru in X and
A11: upper_bound X - e < ru by A4,A6,SEQ_4:def 1;
consider x1 be object such that
A13: x1 in dom lower_sum_set f and
A14: ru = (lower_sum_set f).x1 by A10,FUNCT_1:def 3;
reconsider x1 as Division of I by A13,INTEGRA1:def 3;
ru = lower_sum(f,x1) by A14,INTEGRA1:def 11;
then
A15: J - e < lower_sum(f,x1) by A8,A7,INTEGRA1:def 17,A11;
A16: rng upper_sum_set f is bounded_below by INTEGRA1:def 12,def 16;
A17: upper_integral f = lower_bound rng upper_sum_set f by INTEGRA1:def 14;
set X2 = rng upper_sum_set f;
consider rl be Real such that
A18: rl in X2 and
A19: rl < lower_bound X2 + e by A4,A16,SEQ_4:def 2;
consider x2 be object such that
A20: x2 in dom upper_sum_set f and
A21: rl = (upper_sum_set f).x2 by A18,FUNCT_1:def 3;
reconsider x2 as Division of I by A20,INTEGRA1:def 3;
rl = upper_sum(f,x2) by A21,INTEGRA1:def 10;
then
A22: upper_sum(f,x2) < J + e by A17,INTEGRA1:def 17,A19;
consider x3 be Division of I such that
A23: x1 <= x3 and
A24: x2 <= x3 by INTEGRA1:47;
per cases;
suppose
A25: x3.1 = lower_bound I;
A26: 2 <= len x3
proof
assume
A27: len x3 < 2;
A28: upper_bound I = x3.(len x3) by INTEGRA1:def 2
.= x3.1 by A27,NAT_1:23;
I = [. x3.1,x3.1 .] by A25,A28,INTEGRA1:4;
then I = {x3.1} by XXREAL_1:17;
hence thesis by A1;
end;
then reconsider x4 = x3/^1 as Division of I by COUSIN:65;
take x4;
now
thus
A29: x4.1 <> lower_bound I
proof
assume
A30: x4.1 = lower_bound I;
A31: 1 <= len x3 by A26,XXREAL_0:2;
then len (x3/^1) = len x3 - 1 by RFINSEQ:def 1;
then 2 - 1 <= (len (x3/^1) + 1) - 1 by A26,XREAL_1:9;
then 1 in dom (x3/^1) by FINSEQ_3:25;
then
A32: x4.1 = x3.(1+1) by A31,RFINSEQ:def 1;
1 <= len x3 & 2 <= len x3 by A26,XXREAL_0:2;
then 1 in dom x3 & 2 in dom x3 by FINSEQ_3:25;
hence thesis by A32,A25,A30,VALUED_0:def 13;
end;
A33: upper_sum(f,x4) = upper_sum(f,x3) &
lower_sum(f,x4) = lower_sum(f,x3) by A25,Th38;
f|I is bounded_above & f|I is bounded_below;
then
A34: upper_sum(f,x4) <= upper_sum(f,x2) &
lower_sum(f,x1) <= lower_sum(f,x4) by A33,A23,A24,INTEGRA1:45,46;
then upper_sum(f,x4) < J + e &
J - e < lower_sum(f,x4) by A15,A22,XXREAL_0:2;
then upper_sum(f,x4) - lower_sum(f,x4) < 2 * e by Lm02;
hence thesis by A34,A15,A22,XXREAL_0:2,A29;
end;
hence thesis;
end;
suppose
A35: x3.1 <> lower_bound I;
f|I is bounded_above & f|I is bounded_below;
then upper_sum(f,x3) <= upper_sum(f,x2) &
lower_sum(f,x1) <= lower_sum(f,x3) by A23,A24,INTEGRA1:45,46;
then
A36: upper_sum(f,x3) < J + e &
J - e < lower_sum(f,x3) by A15,A22,XXREAL_0:2;
then upper_sum(f,x3) - lower_sum(f,x3) < 2 * e by Lm02;
hence thesis by A36,A35;
end;
end;
reserve jauge for positive-yielding Function of I,REAL;
theorem
jauge = r (#) chi(I,I) implies 0 < r
proof
assume
A1: jauge = r (#) chi(I,I);
assume
A2: r <= 0;
set x = the Element of I;
x in I;
then
A3: x in dom chi(I,I) & x in dom jauge by PARTFUN1:def 2;
then jauge.x = r * (chi(I,I)).x by A1,VALUED_1:def 5
.= r * 1 by FUNCT_3:def 3
.= r;
then jauge.x <= 0 & jauge.x in rng jauge by A2,A3,FUNCT_1:3;
hence contradiction by PARTFUN3:def 1;
end;
reserve D for tagged_division of I;
theorem Th42:
jauge = r (#) chi(I,I) & D is jauge-fine
implies delta(division_of D) <= r
proof
assume that
A1: jauge = r (#) chi(I,I) and
A2: D is jauge-fine;
A3: now
let i be Nat;
assume
A4: i in dom division_of D;
consider D9 be Division of I,
T9 be Element of set_of_tagged_Division(D9) such that
A5: D = [D9,T9] & for i being Nat st i in dom D9 holds
vol divset(D9,i) <= jauge.(T9.i) by A2,COUSIN:def 4;
A6: T9 = tagged_of D & D9 = division_of D by A5,Th20; then
A7: vol divset(division_of D,i) <= jauge.((tagged_of D).i) by A5,A4;
A8: dom (r (#) chi(I,I)) = dom chi(I,I) by VALUED_1:def 5
.= I by FUNCT_3:def 3;
i in Seg len division_of D by A4,FINSEQ_1:def 3;
then i in Seg len tagged_of D by Th21; then
A9: i in dom T9 by A6,FINSEQ_1:def 3;
rng T9 c= I by Th22; then
A10: (tagged_of D).i in I by A9,A6,FUNCT_1:3;
now
let x be object;
assume
A11: x in dom (r (#) chi(I,I));
then (r (#) chi(I,I)).x = r * (chi(I,I)).x by VALUED_1:def 5
.= r * 1 by A11,FUNCT_3:def 3
.= r;
hence jauge.x = r by A1;
end;
hence vol divset(division_of D,i) <= r by A7,A8,A10;
end;
reconsider g = chi(I,I) as Function of I,REAL by Th11;
A12: for i be Nat st i in dom division_of D holds
upper_volume(g,division_of D).i <= r
proof
let i be Nat;
assume
A13: i in dom division_of D;
then vol divset(division_of D,i) <= r by A3;
hence thesis by A13,INTEGRA1:20;
end;
delta(division_of D) <= r
proof
assume r < delta(division_of D);
then
A14: r < max rng upper_volume(g,division_of D) by INTEGRA3:def 1;
sup rng upper_volume(g,division_of D)
in rng upper_volume(g,division_of D) by XXREAL_2:def 6;
then consider x be object such that
A15: x in dom upper_volume(g,division_of D) and
A16: (upper_volume(g,division_of D)).x
= sup rng upper_volume(g,division_of D) by FUNCT_1:def 3;
A17: dom upper_volume(g,division_of D)
= Seg len upper_volume(g,division_of D) by FINSEQ_1:def 3
.= Seg len division_of D by INTEGRA1:def 6
.= dom division_of D by FINSEQ_1:def 3;
reconsider i = x as Nat by A15;
thus contradiction by A14,A15,A17,A16,A12;
end;
hence thesis;
end;
reserve r1,r2,s for Real,
D,D1 for Division of I,
fc for Function of I,REAL;
theorem Th43:
ex i being Nat st i in dom D &
min rng upper_volume(fc,D) = (upper_volume(fc,D)).i
proof
inf rng upper_volume(fc,D) in rng upper_volume(fc,D) by XXREAL_2:def 5;
then consider x be object such that
A1: x in dom upper_volume(fc,D) and
A2: (upper_volume(fc,D)).x = inf rng upper_volume(fc,D) by FUNCT_1:def 3;
A3: dom upper_volume(fc,D)
= Seg len upper_volume(fc,D) by FINSEQ_1:def 3
.= Seg len D by INTEGRA1:def 6
.= dom D by FINSEQ_1:def 3;
reconsider i = x as Nat by A1;
take i;
thus thesis by A2,A3,A1;
end;
theorem Th44:
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) .| )
proof
let f be Function of I,REAL;
let epsilon be Real;
assume that
A1: fc = chi(I,I) and
A2: r1 = min rng upper_volume(fc,D1) and
A3: r2 = epsilon / (2 * (len D1) *
|. upper_bound (rng f) - lower_bound (rng f) .| ) and
A4: 0 < r1 and
A5: 0 < r2 and
A6: s = min(r1,r2) / 2 and
A7: jauge = s (#) fc and
A8: TD is jauge-fine;
A9: delta(division_of TD) <= min(r1,r2) / 2 by A1,A6,A7,A8,Th42;
min(r1,r2) / 2 < min(r1,r2) / 1 by A4,A5,XREAL_1:76;
then delta(division_of TD) < min(r1,r2) by A9,XXREAL_0:2;
hence thesis by A2,A3,XXREAL_0:23;
end;
theorem Th45:
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
proof
let p be FinSequence of REAL;
assume that
A1: for i be Nat st i in dom p holds r <= p.i and
A2: ex i0 be Nat st i0 in dom p & p.i0 = r;
set X = rng p;
consider i0 be Nat such that
A3: i0 in dom p and
A4: p.i0 = r by A2;
reconsider X as non empty bounded_below real-membered set
by A3,A4,FUNCT_1:def 3;
A5: for a be Real st a in X holds r <= a
proof
let a be Real;
assume a in X;
then ex i be object st i in dom p & p.i = a by FUNCT_1:def 3;
hence thesis by A1;
end;
for s be Real st 0 < s ex a be Real st a in X & a < r + s
proof
let s be Real;
assume
A6: 0 < s;
consider i0 be Nat such that
A7: i0 in dom p and
A8: p.i0 = r by A2;
reconsider a = p.i0 as Real;
take a;
thus a in X by A7,FUNCT_1:def 3;
r + 0 < r + s by A6,XREAL_1:8;
hence a < r + s by A8;
end;
then r = lower_bound X by A5,SEQ_4:def 2;
hence thesis;
end;
theorem Th46:
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.])
proof
assume
A1: fc = chi(I,I);
consider i0 be Nat such that
A2: i0 in dom D and
A3: min rng upper_volume(fc,D) = (upper_volume(fc,D)).i0 by Th43;
min rng upper_volume(fc,D) = vol(divset(D,i0)) by A1,A2,A3,INTEGRA1:20;
hence 0 <= min rng upper_volume(fc,D) by INTEGRA1:9;
thus 0 = min rng upper_volume(fc,D) iff divset(D,1) = [.D.1,D.1.]
proof
hereby
assume 0 = min rng upper_volume(fc,D);
then
A4: vol(divset(D,i0)) = 0 by A3,A1,A2,INTEGRA1:20;
rng D <> {};
then 1 in dom D by FINSEQ_3:32;
then D.1 in I by INTEGRA1:6;
then D.1 in [. lower_bound I, upper_bound I.] by INTEGRA1:4;
then
A5: lower_bound I <= D.1 by XXREAL_1:1;
now
1 <= i0 <= len D by A2,FINSEQ_3:25;
then per cases by XXREAL_0:1;
suppose i0 = 1;
then divset(D,i0) = [.lower_bound I,D.1.] by COUSIN:50;
then lower_bound divset(D,i0) = lower_bound I &
upper_bound divset(D,i0) = D.1 by A5,JORDAN5A:19;
then vol divset(D,i0) = D.1 - lower_bound I by INTEGRA1:def 5;
hence divset(D,1) = [.D.1,D.1.] by A4,COUSIN:50;
end;
suppose
A6: 1 < i0;
A7: now
thus i0 in dom D by A2;
thus i0 - 1 in dom D by A6,A2,CGAMES_1:20;
i0 - 1 < i0 - 0 by XREAL_1:15;
hence i0 - 1 < i0;
end;
then
A8: D.(i0 - 1) < D.i0 by VALUED_0:def 13;
divset(D,i0) = [.D.(i0-1),D.i0.] by A6,A2,COUSIN:50;
then lower_bound divset(D,i0) = D.(i0 - 1) &
upper_bound divset(D,i0) = D.i0 by A8,JORDAN5A:19;
then vol divset(D,i0) = D.i0 - D.(i0 - 1) by INTEGRA1:def 5;
hence divset(D,1) = [.D.1,D.1.] by A4,A7,VALUED_0:def 13;
end;
end;
hence divset(D,1) = [.D.1,D.1.];
end;
assume
A9: divset(D,1) = [.D.1,D.1.];
A10: vol divset(D,1)
= upper_bound divset(D,1) - lower_bound divset(D,1) by INTEGRA1:def 5
.= D.1 - lower_bound divset(D,1) by A9,JORDAN5A:19
.= D.1 - D.1 by A9,JORDAN5A:19
.= 0;
rng D <> {}; then
A11: 1 in dom D by FINSEQ_3:32; then
A12: upper_volume(fc,D).1 = 0 by A1,A10,INTEGRA1:20;
1 in Seg len D by A11,FINSEQ_1:def 3;
then 1 in Seg len upper_volume(fc,D) by INTEGRA1:def 6; then
A13: 1 in dom upper_volume(fc,D) by FINSEQ_1:def 3;
now
let i be Nat;
assume i in dom upper_volume(fc,D);
then i in Seg len upper_volume(fc,D) by FINSEQ_1:def 3;
then i in Seg len D by INTEGRA1:def 6;
then i in dom D by FINSEQ_1:def 3;
then upper_volume(fc,D).i = vol divset(D,i) by A1,INTEGRA1:20;
hence 0 <= upper_volume(fc,D).i by INTEGRA1:9;
end;
hence 0 = min rng upper_volume(fc,D) by A13,A12,Th45;
end;
end;
theorem Th47:
divset(D,1) = [.D.1,D.1.] implies D.1 = lower_bound I
proof
assume divset(D,1) = [.D.1,D.1.]; then
A1: lower_bound divset(D,1) = D.1 & upper_bound divset(D,1) = D.1
by JORDAN5A:19;
A2: divset(D,1) = [.lower_bound I,D.1.] by COUSIN:50;
rng D <> {};
then 1 in dom D by FINSEQ_3:32;
then D.1 in I by INTEGRA1:6;
then D.1 in [. lower_bound I, upper_bound I.] by INTEGRA1:4;
then lower_bound I <= D.1 <= upper_bound I by XXREAL_1:1;
hence thesis by A1,A2,JORDAN5A:19;
end;
theorem Th48:
for f being bounded integrable Function of I,REAL
holds f is HK-integrable & HK-integral(f) = integral(f)
proof
let f be bounded integrable Function of I,REAL;
per cases;
suppose
A1: f is constant;
then consider r be Real such that
A2: f = r (#) chi(I,I) and
A3: HK-integral f = r * vol(I) by Th36;
reconsider g = chi(I,I) as Function of I,REAL by Th11;
A4: g|I is bounded by Th14;
g is integrable by INTEGRA4:2;
then integral f = r * integral g by A2,A4,INTEGRA2:31;
hence thesis by A1,Th36,A3,INTEGRA4:2;
end;
suppose
A5: f is non constant;
per cases;
suppose I is trivial;
then f is HK-integrable & HK-integral(f) = 0 & vol I = 0
by Th25,Th27;
hence thesis by INTEGRA4:6;
end;
suppose
A6: I is non trivial;
set J = integral(f);
A7: now
let epsilon be Real;
assume
A8: epsilon > 0;
consider D be Division of I such that
A9: D.1 <> lower_bound I and
A10: upper_sum(f,D) < integral(f) + (epsilon / 2) and
A11: integral(f) - (epsilon / 2) < lower_sum(f,D) and
upper_sum(f,D) - lower_sum(f,D) < epsilon by A6,A8,Th41;
reconsider fc = chi(I,I) as Function of I,REAL by Th11;
0 < min rng upper_volume(fc,D)
proof
assume not 0 < min rng upper_volume(fc,D);
then 0 = min rng upper_volume(fc,D) by Th46;
then divset(D,1) = [.D.1,D.1.] by Th46;
hence contradiction by A9,Th47;
end;
then reconsider r1 = min rng upper_volume(fc,D) as positive Real;
|. upper_bound (rng f) - lower_bound (rng f) .| <> 0 by A5,Th37;
then reconsider r2 = epsilon / (2 * (len D) *
|. upper_bound (rng f) - lower_bound (rng f) .| )
as positive Real by A8;
reconsider s = min(r1,r2) / 2 as positive Real;
chi(I,I) is positive-yielding by Th17;
then reconsider jauge = s (#) fc
as positive-yielding Function of I,REAL;
take jauge;
thus for TD being tagged_division of I st TD is jauge-fine
holds |.tagged_sum(f,TD) - (integral f).| <= epsilon
proof
let TD be tagged_division of I;
assume
A12: TD is jauge-fine;
Sum lower_volume(f,division_of TD) <= Sum tagged_volume(f,TD)
<= Sum upper_volume(f,division_of TD) by Th40;
then
A13: lower_sum(f,division_of TD) <= tagged_sum(f,TD)
<= upper_sum(f,division_of TD) by INTEGRA1:def 8,def 9;
A14: f|I is bounded & delta(division_of TD)
< min rng upper_volume(fc,D) by A12,Th44;
then consider D9 be Division of I such that
A15: D <=D9 and
A16: division_of TD<=D9 and
A17: rng D9 = rng (division_of TD) \/ rng D and
A18: upper_sum(f,division_of TD)-upper_sum(f,D9)
<= (len D) * (upper_bound(rng f)-lower_bound(rng f))
* delta(division_of TD) by INTEGRA3:24;
consider D9B be Division of I such that
D <= D9B and
division_of TD <= D9B and
A19: rng D9B = rng (division_of TD) \/ rng D and
A20: lower_sum(f,D9B) - lower_sum(f,division_of TD)
<= (len D) * (upper_bound(rng f)-lower_bound(rng f))
* delta(division_of TD) by A14,INTEGRA3:22;
f|I is bounded_above;
then
A21: upper_sum(f,D9) <= upper_sum(f,division_of TD) &
upper_sum(f,D9) <= upper_sum(f,D) by A16,A15,INTEGRA1:45;
f|I is bounded_below;
then
A22: lower_sum(f,division_of TD) <= lower_sum(f,D9) &
lower_sum(f,D) <= lower_sum(f,D9) by A16,A15,INTEGRA1:46;
A23: J = upper_integral(f) by INTEGRA1:def 17;
then
A24: J = lower_integral(f) by INTEGRA1:def 16;
then
A25: lower_sum(f,division_of TD) <= J by Th18,INTEGRA1:def 16;
A26: J - (epsilon / 2) < lower_sum(f,D9) <= J
by A22,A11,XXREAL_0:2,Th18,INTEGRA1:def 16,A24;
A27: J <= upper_sum(f,division_of TD)
by A23,Th19,INTEGRA1:def 16;
A28: J <= upper_sum(f,D9) < J + (epsilon / 2)
by A21,A10,XXREAL_0:2,A23,INTEGRA1:def 16,Th19;
now
thus upper_sum(f,division_of TD)-upper_sum(f,D9)
<= (len D) * (upper_bound(rng f)-lower_bound(rng f))
* delta(division_of TD) by A18;
thus 0 <= len D;
lower_bound rng f <= upper_bound rng f by INTEGRA1:15,SEQ_4:11;
hence 0 <= upper_bound(rng f)-lower_bound(rng f) by XREAL_1:48;
thus 0 <= delta(division_of TD) by INTEGRA3:9;
thus delta(division_of TD) < epsilon / (2 * len D *
|. upper_bound(rng f)-lower_bound(rng f) .|) by A12,Th44;
end;
then
A29: upper_sum(f,division_of TD)-upper_sum(f,D9)
<= epsilon / 2 by Th07;
A30: lower_sum(f,D9) - lower_sum(f,division_of TD) <= epsilon / 2
proof
A31: lower_sum(f,D9) - lower_sum(f,division_of TD)
<= (len D) * (upper_bound(rng f)-lower_bound(rng f))
* delta(division_of TD)
by A20,A17,A19,INTEGRA3:6;
lower_bound rng f <= upper_bound rng f
by INTEGRA1:15,SEQ_4:11;
then
A32: 0 <= upper_bound(rng f)-lower_bound(rng f) by XREAL_1:48;
0 <= delta(division_of TD) by INTEGRA3:9;
hence thesis by A31,A32,Th07,A12,Th44;
end;
A33: |. lower_sum(f,division_of TD) - J .| <= epsilon
proof
(J - (epsilon / 2)) - lower_sum(f,division_of TD)
<= lower_sum(f,D9) - lower_sum(f,division_of TD)
by A26,XREAL_1:9;
then (J - (epsilon / 2)) - lower_sum(f,division_of TD)
<= epsilon / 2 by A30,XXREAL_0:2;
then (J - lower_sum(f,division_of TD)) - (epsilon / 2)
+ (epsilon / 2)
<= epsilon / 2 + epsilon / 2 by XREAL_1:6;
hence thesis by Th01,A25;
end;
|. upper_sum(f,division_of TD) - J .| <= epsilon
proof
upper_sum(f,division_of TD) - (J + (epsilon /2))
< upper_sum(f,division_of TD) - upper_sum(f,D9)
by A28,XREAL_1:15;
then upper_sum(f,division_of TD) - (J + (epsilon /2))
< epsilon / 2 by A29,XXREAL_0:2;
then (upper_sum(f,division_of TD)) - J - (epsilon / 2)
+ (epsilon / 2)
< epsilon / 2 + (epsilon / 2) by XREAL_1:8;
hence thesis by A27,Th02;
end;
hence thesis by A13,A33,Th03;
end;
end;
hence f is HK-integrable;
hence thesis by A7,DEFCC;
end;
end;
end;
registration
let I be non empty closed_interval Subset of REAL;
cluster bounded integrable -> HK-integrable for Function of I,REAL;
coherence by Th48;
end;