Definition df-ibl 23391

Description: Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014.)

Assertion

Ref	Expression
df-ibl	|- L^1 = { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }

Distinct variable group:   y, k, f, x

Detailed syntax breakdown of Definition df-ibl

Step	Hyp	Ref	Expression
1		cibl 23386	. 2 class L^1
2		vx	. . . . . . 7 setvar x
3		cr 9935	. . . . . . 7 class RR
4		vy	. . . . . . . 8 setvar y
5	2	cv 1482	. . . . . . . . . . 11 class x
6		vf	. . . . . . . . . . . 12 setvar f
7	6	cv 1482	. . . . . . . . . . 11 class f
8	5, 7	cfv 5888	. . . . . . . . . 10 class ( f ` x )
9		ci 9938	. . . . . . . . . . 11 class _i
10		vk	. . . . . . . . . . . 12 setvar k
11	10	cv 1482	. . . . . . . . . . 11 class k
12		cexp 12860	. . . . . . . . . . 11 class ^
13	9, 11, 12	co 6650	. . . . . . . . . 10 class ( _i ^ k )
14		cdiv 10684	. . . . . . . . . 10 class /
15	8, 13, 14	co 6650	. . . . . . . . 9 class ( ( f ` x ) / ( _i ^ k ) )
16		cre 13837	. . . . . . . . 9 class Re
17	15, 16	cfv 5888	. . . . . . . 8 class ( Re ` ( ( f ` x ) / ( _i ^ k ) ) )
18	7	cdm 5114	. . . . . . . . . . 11 class dom f
19	5, 18	wcel 1990	. . . . . . . . . 10 wff x e. dom f
20		cc0 9936	. . . . . . . . . . 11 class 0
21	4	cv 1482	. . . . . . . . . . 11 class y
22		cle 10075	. . . . . . . . . . 11 class <_
23	20, 21, 22	wbr 4653	. . . . . . . . . 10 wff 0 <_ y
24	19, 23	wa 384	. . . . . . . . 9 wff ( x e. dom f /\ 0 <_ y )
25	24, 21, 20	cif 4086	. . . . . . . 8 class if ( ( x e. dom f /\ 0 <_ y ) , y , 0 )
26	4, 17, 25	csb 3533	. . . . . . 7 class [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 )
27	2, 3, 26	cmpt 4729	. . . . . 6 class ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) )
28		citg2 23385	. . . . . 6 class S.2
29	27, 28	cfv 5888	. . . . 5 class ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) )
30	29, 3	wcel 1990	. . . 4 wff ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR
31		c3 11071	. . . . 5 class 3
32		cfz 12326	. . . . 5 class ...
33	20, 31, 32	co 6650	. . . 4 class ( 0 ... 3 )
34	30, 10, 33	wral 2912	. . 3 wff A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR
35		cmbf 23383	. . 3 class MblFn
36	34, 6, 35	crab 2916	. 2 class { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }
37	1, 36	wceq 1483	1 wff L^1 = { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }

This definition is referenced by:  isibl  23532  iblmbf  23534