Metamath Proof Explorer

Definition df-itg

Description: Define the full Lebesgue integral, for complex-valued functions to RR . The syntax is designed to be suggestive of the standard notation for integrals. For example, our notation for the integral of x ^ 2 from 0 to 1 is S. ( 0 , 1 ) ( x ^ 2 ) _d x = ( 1 / 3 ) . The only real function of this definition is to break the integral up into nonnegative real parts and send it off to df-itg2 for further processing. Note that this definition cannot handle integrals which evaluate to infinity, because addition and multiplication are not currently defined on extended reals. (You can use df-itg2 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion df-itg 
|- S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 vx 
 |-  x
3 2 0 1 citg 
 |-  S. A B _d x
4 vk 
 |-  k
5 cc0 
 |-  0
6 cfz 
 |-  ...
7 c3 
 |-  3
8 5 7 6 co 
 |-  ( 0 ... 3 )
9 ci 
 |-  _i
10 cexp 
 |-  ^
11 4 cv 
 |-  k
12 9 11 10 co 
 |-  ( _i ^ k )
13 cmul 
 |-  x.
14 citg2 
 |-  S.2
15 cr 
 |-  RR
16 cre 
 |-  Re
17 cdiv 
 |-  /
18 1 12 17 co 
 |-  ( B / ( _i ^ k ) )
19 18 16 cfv 
 |-  ( Re ` ( B / ( _i ^ k ) ) )
20 vy 
 |-  y
21 2 cv 
 |-  x
22 21 0 wcel 
 |-  x e. A
23 cle 
 |-  <_
24 20 cv 
 |-  y
25 5 24 23 wbr 
 |-  0 <_ y
26 22 25 wa 
 |-  ( x e. A /\ 0 <_ y )
27 26 24 5 cif 
 |-  if ( ( x e. A /\ 0 <_ y ) , y , 0 )
28 20 19 27 csb 
 |-  [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 )
29 2 15 28 cmpt 
 |-  ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) )
30 29 14 cfv 
 |-  ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) )
31 12 30 13 co 
 |-  ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )
32 8 31 4 csu 
 |-  sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )
33 3 32 wceq 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )