let a, b be Real; for X being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f holds
f is_integrable_on ['a,b']
let X be RealBanachSpace; for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f holds
f is_integrable_on ['a,b']
let f be continuous PartFunc of REAL, the carrier of X; ( a <= b & ['a,b'] c= dom f implies f is_integrable_on ['a,b'] )
set A = ['a,b'];
assume A1:
( a <= b & ['a,b'] c= dom f )
; f is_integrable_on ['a,b']
then reconsider h = f | ['a,b'] as Function of ['a,b'], the carrier of X by Lm1;
A2:
f | ['a,b'] is uniformly_continuous
by A1, Th3;
consider T0 being DivSequence of ['a,b'] such that
A3:
( delta T0 is convergent & lim (delta T0) = 0 )
by INTEGRA4:11;
set S0 = the middle_volume_Sequence of h,T0;
set I = lim (middle_sum (h, the middle_volume_Sequence of h,T0));
for T being DivSequence of ['a,b']
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) )
proof
let T be
DivSequence of
['a,b'];
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) )let S be
middle_volume_Sequence of
h,
T;
( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) ) )
assume A4:
(
delta T is
convergent &
lim (delta T) = 0 )
;
( middle_sum (h,S) is convergent & lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0)) )
hence
middle_sum (
h,
S) is
convergent
by A2, Th13;
lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0))
consider T1 being
DivSequence of
['a,b'] such that A5:
for
i being
Nat holds
(
T1 . (2 * i) = T0 . i &
T1 . ((2 * i) + 1) = T . i )
by Th15;
consider S1 being
middle_volume_Sequence of
h,
T1 such that A6:
for
i being
Nat holds
(
S1 . (2 * i) = the
middle_volume_Sequence of
h,
T0 . i &
S1 . ((2 * i) + 1) = S . i )
by A5, Th17;
(
delta T1 is
convergent &
lim (delta T1) = 0 )
by A4, A5, A3, Th16;
then A7:
middle_sum (
h,
S1) is
convergent
by A2, Th13;
A8:
for
i being
Nat holds
(
(middle_sum (h,S1)) . (2 * i) = (middle_sum (h, the middle_volume_Sequence of h,T0)) . i &
(middle_sum (h,S1)) . ((2 * i) + 1) = (middle_sum (h,S)) . i )
proof
let i be
Nat;
( (middle_sum (h,S1)) . (2 * i) = (middle_sum (h, the middle_volume_Sequence of h,T0)) . i & (middle_sum (h,S1)) . ((2 * i) + 1) = (middle_sum (h,S)) . i )
reconsider S1 =
S1 as
middle_volume_Sequence of
h,
T1 ;
(
(middle_sum (h,S1)) . (2 * i) = middle_sum (
h,
(S1 . (2 * i))) &
(middle_sum (h,S1)) . ((2 * i) + 1) = middle_sum (
h,
(S1 . ((2 * i) + 1))) )
by INTEGR18:def 4;
then
(
(middle_sum (h,S1)) . (2 * i) = middle_sum (
h,
( the middle_volume_Sequence of h,T0 . i)) &
(middle_sum (h,S1)) . ((2 * i) + 1) = middle_sum (
h,
(S . i)) )
by A6;
hence
(
(middle_sum (h,S1)) . (2 * i) = (middle_sum (h, the middle_volume_Sequence of h,T0)) . i &
(middle_sum (h,S1)) . ((2 * i) + 1) = (middle_sum (h,S)) . i )
by INTEGR18:def 4;
verum
end;
lim (middle_sum (h,S)) = lim (middle_sum (h,S1))
by A7, A8, Th18;
hence
lim (middle_sum (h,S)) = lim (middle_sum (h, the middle_volume_Sequence of h,T0))
by A7, A8, Th18;
verum
end;
then
h is integrable
;
hence
f is_integrable_on ['a,b']
; verum