:: INTEGRA5 semantic presentation

theorem Th1: :: INTEGRA5:1
for b1, b2, b3 being FinSequence of REAL
for b4, b5 being Real st ( b2 = <*b4*> ^ b1 or b2 = b1 ^ <*b4*> ) & ( b3 = <*b5*> ^ b1 or b3 = b1 ^ <*b5*> ) holds
Sum (b2 - b3) = b4 - b5
proof end;

theorem Th2: :: INTEGRA5:2
for b1, b2 being FinSequence of REAL st len b1 = len b2 holds
( len (b1 + b2) = len b1 & len (b1 - b2) = len b1 & Sum (b1 + b2) = (Sum b1) + (Sum b2) & Sum (b1 - b2) = (Sum b1) - (Sum b2) )
proof end;

theorem Th3: :: INTEGRA5:3
for b1, b2 being FinSequence of REAL st len b1 = len b2 & ( for b3 being Nat st b3 in dom b1 holds
b1 . b3 <= b2 . b3 ) holds
Sum b1 <= Sum b2
proof end;

definition
let c1 be non empty Subset of REAL ;
let c2 be PartFunc of REAL , REAL ;
func c2 || c1 -> PartFunc of a1, REAL equals :: INTEGRA5:def 1
a2 | a1;
correctness
coherence
c2 | c1 is PartFunc of c1, REAL ;
by PARTFUN1:43;
end;

:: deftheorem Def1 defines || INTEGRA5:def 1 :
for b1 being non empty Subset of REAL
for b2 being PartFunc of REAL , REAL holds b2 || b1 = b2 | b1;

theorem Th4: :: INTEGRA5:4
for b1, b2 being PartFunc of REAL , REAL
for b3 being non empty Subset of REAL holds (b1 || b3) (#) (b2 || b3) = (b1 (#) b2) || b3
proof end;

theorem Th5: :: INTEGRA5:5
for b1, b2 being PartFunc of REAL , REAL
for b3 being non empty Subset of REAL holds (b1 + b2) || b3 = (b1 || b3) + (b2 || b3)
proof end;

definition
let c1 be closed-interval Subset of REAL ;
let c2 be PartFunc of REAL , REAL ;
pred c2 is_integrable_on c1 means :Def2: :: INTEGRA5:def 2
a2 || a1 is_integrable_on a1;
end;

:: deftheorem Def2 defines is_integrable_on INTEGRA5:def 2 :
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL holds
( b2 is_integrable_on b1 iff b2 || b1 is_integrable_on b1 );

definition
let c1 be closed-interval Subset of REAL ;
let c2 be PartFunc of REAL , REAL ;
func integral c2,c1 -> Real equals :: INTEGRA5:def 3
 integral (a2 || a1);
correctness
coherence
integral (c2 || c1) is Real;
;
end;

:: deftheorem Def3 defines integral INTEGRA5:def 3 :
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL holds integral b2,b1 = integral (b2 || b1);

theorem Th6: :: INTEGRA5:6
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 holds
b2 || b1 is total
proof end;

theorem Th7: :: INTEGRA5:7
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_bounded_above_on b1 holds
b2 || b1 is_bounded_above_on b1
proof end;

theorem Th8: :: INTEGRA5:8
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_bounded_below_on b1 holds
b2 || b1 is_bounded_below_on b1
proof end;

theorem Th9: :: INTEGRA5:9
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_bounded_on b1 holds
b2 || b1 is_bounded_on b1
proof end;

theorem Th10: :: INTEGRA5:10
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_continuous_on b1 holds
b2 is_bounded_on b1
proof end;

theorem Th11: :: INTEGRA5:11
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_continuous_on b1 holds
b2 is_integrable_on b1
proof end;

theorem Th12: :: INTEGRA5:12
for b1 being closed-interval Subset of REAL
for b2 being set
for b3 being PartFunc of REAL , REAL
for b4 being Element of divs b1 st b1 c= b2 & b3 is_differentiable_on b2 & b3 `| b2 is_bounded_on b1 holds
( lower_sum ((b3 `| b2) || b1),b4 <= (b3 . (sup b1)) - (b3 . (inf b1)) & (b3 . (sup b1)) - (b3 . (inf b1)) <= upper_sum ((b3 `| b2) || b1),b4 )
proof end;

theorem Th13: :: INTEGRA5:13
for b1 being closed-interval Subset of REAL
for b2 being set
for b3 being PartFunc of REAL , REAL st b1 c= b2 & b3 is_differentiable_on b2 & b3 `| b2 is_integrable_on b1 & b3 `| b2 is_bounded_on b1 holds
integral (b3 `| b2),b1 = (b3 . (sup b1)) - (b3 . (inf b1))
proof end;

theorem Th14: :: INTEGRA5:14
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_non_decreasing_on b1 & b1 c= dom b2 holds
rng (b2 | b1) is bounded
proof end;

theorem Th15: :: INTEGRA5:15
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_non_decreasing_on b1 & b1 c= dom b2 holds
( inf (rng (b2 | b1)) = b2 . (inf b1) & sup (rng (b2 | b1)) = b2 . (sup b1) )
proof end;

Lemma17: for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_non_decreasing_on b1 & b1 c= dom b2 holds
b2 is_integrable_on b1
proof end;

theorem Th16: :: INTEGRA5:16
for b1 being closed-interval Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_monotone_on b1 & b1 c= dom b2 holds
b2 is_integrable_on b1
proof end;

theorem Th17: :: INTEGRA5:17
for b1 being PartFunc of REAL , REAL
for b2, b3 being closed-interval Subset of REAL st b1 is_continuous_on b2 & b3 c= b2 holds
b1 is_integrable_on b3
proof end;

theorem Th18: :: INTEGRA5:18
for b1 being PartFunc of REAL , REAL
for b2, b3, b4 being closed-interval Subset of REAL
for b5 being set st b2 c= b5 & b1 is_differentiable_on b5 & b1 `| b5 is_continuous_on b2 & inf b2 = inf b3 & sup b3 = inf b4 & sup b4 = sup b2 holds
( b3 c= b2 & b4 c= b2 & integral (b1 `| b5),b2 = (integral (b1 `| b5),b3) + (integral (b1 `| b5),b4) )
proof end;

definition
let c1, c2 be real number ;
assume E19: c1 <= c2 ;
func ['c1,c2'] -> closed-interval Subset of REAL equals :Def4: :: INTEGRA5:def 4
[.a1,a2.];
correctness
coherence
[.c1,c2.] is closed-interval Subset of REAL ;
proof end;
end;

:: deftheorem Def4 defines [' INTEGRA5:def 4 :
for b1, b2 being real number st b1 <= b2 holds
['b1,b2'] = [.b1,b2.];

definition
let c1, c2 be real number ;
let c3 be PartFunc of REAL , REAL ;
func integral c3,c1,c2 -> Real equals :Def5: :: INTEGRA5:def 5
 integral a3,['a1,a2'] if a1 <= a2
otherwise - (integral a3,['a2,a1']);
correctness
coherence
( ( c1 <= c2 implies integral c3,['c1,c2'] is Real ) & ( not c1 <= c2 implies - (integral c3,['c2,c1']) is Real ) );
consistency
for b1 being Real holds verum;
;
end;

:: deftheorem Def5 defines integral INTEGRA5:def 5 :
for b1, b2 being real number
for b3 being PartFunc of REAL , REAL holds
( ( b1 <= b2 implies integral b3,b1,b2 = integral b3,['b1,b2'] ) & ( not b1 <= b2 implies integral b3,b1,b2 = - (integral b3,['b2,b1']) ) );

theorem Th19: :: INTEGRA5:19
for b1 being PartFunc of REAL , REAL
for b2 being closed-interval Subset of REAL
for b3, b4 being Real st b2 = [.b3,b4.] holds
integral b1,b2 = integral b1,b3,b4
proof end;

theorem Th20: :: INTEGRA5:20
for b1 being PartFunc of REAL , REAL
for b2 being closed-interval Subset of REAL
for b3, b4 being Real st b2 = [.b4,b3.] holds
- (integral b1,b2) = integral b1,b3,b4
proof end;

theorem Th21: :: INTEGRA5:21
for b1 being closed-interval Subset of REAL
for b2, b3 being PartFunc of REAL , REAL
for b4 being open Subset of REAL st b2 is_differentiable_on b4 & b3 is_differentiable_on b4 & b1 c= b4 & b2 `| b4 is_integrable_on b1 & b2 `| b4 is_bounded_on b1 & b3 `| b4 is_integrable_on b1 & b3 `| b4 is_bounded_on b1 holds
integral ((b2 `| b4) (#) b3),b1 = (((b2 . (sup b1)) * (b3 . (sup b1))) - ((b2 . (inf b1)) * (b3 . (inf b1)))) - (integral (b2 (#) (b3 `| b4)),b1)
proof end;