Definition df-ibl 23197

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	⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}

Distinct variable group:   𝑦,𝑘,𝑓,𝑥

Detailed syntax breakdown of Definition df-ibl

Step	Hyp	Ref	Expression
1		cibl 23192	. 2 class 𝐿1
2		vx	. . . . . . 7 setvar 𝑥
3		cr 9814	. . . . . . 7 class ℝ
4		vy	. . . . . . . 8 setvar 𝑦
5	2	cv 1474	. . . . . . . . . . 11 class 𝑥
6		vf	. . . . . . . . . . . 12 setvar 𝑓
7	6	cv 1474	. . . . . . . . . . 11 class 𝑓
8	5, 7	cfv 5804	. . . . . . . . . 10 class (𝑓‘𝑥)
9		ci 9817	. . . . . . . . . . 11 class i
10		vk	. . . . . . . . . . . 12 setvar 𝑘
11	10	cv 1474	. . . . . . . . . . 11 class 𝑘
12		cexp 12722	. . . . . . . . . . 11 class ↑
13	9, 11, 12	co 6549	. . . . . . . . . 10 class (i↑𝑘)
14		cdiv 10563	. . . . . . . . . 10 class /
15	8, 13, 14	co 6549	. . . . . . . . 9 class ((𝑓‘𝑥) / (i↑𝑘))
16		cre 13685	. . . . . . . . 9 class ℜ
17	15, 16	cfv 5804	. . . . . . . 8 class (ℜ‘((𝑓‘𝑥) / (i↑𝑘)))
18	7	cdm 5038	. . . . . . . . . . 11 class dom 𝑓
19	5, 18	wcel 1977	. . . . . . . . . 10 wff 𝑥 ∈ dom 𝑓
20		cc0 9815	. . . . . . . . . . 11 class 0
21	4	cv 1474	. . . . . . . . . . 11 class 𝑦
22		cle 9954	. . . . . . . . . . 11 class ≤
23	20, 21, 22	wbr 4583	. . . . . . . . . 10 wff 0 ≤ 𝑦
24	19, 23	wa 383	. . . . . . . . 9 wff (𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦)
25	24, 21, 20	cif 4036	. . . . . . . 8 class if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
26	4, 17, 25	csb 3499	. . . . . . 7 class ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	2, 3, 26	cmpt 4643	. . . . . 6 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))
28		citg2 23191	. . . . . 6 class ∫2
29	27, 28	cfv 5804	. . . . 5 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)))
30	29, 3	wcel 1977	. . . 4 wff (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
31		c3 10948	. . . . 5 class 3
32		cfz 12197	. . . . 5 class ...
33	20, 31, 32	co 6549	. . . 4 class (0...3)
34	30, 10, 33	wral 2896	. . 3 wff ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
35		cmbf 23189	. . 3 class MblFn
36	34, 6, 35	crab 2900	. 2 class {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
37	1, 36	wceq 1475	1 wff 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}

This definition is referenced by:  isibl  23338  iblmbf  23340