Definition df-ibl 25139

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 25134	. 2 class 𝐿1
2		vx	. . . . . . 7 setvar 𝑥
3		cr 11109	. . . . . . 7 class ℝ
4		vy	. . . . . . . 8 setvar 𝑦
5	2	cv 1541	. . . . . . . . . . 11 class 𝑥
6		vf	. . . . . . . . . . . 12 setvar 𝑓
7	6	cv 1541	. . . . . . . . . . 11 class 𝑓
8	5, 7	cfv 6544	. . . . . . . . . 10 class (𝑓‘𝑥)
9		ci 11112	. . . . . . . . . . 11 class i
10		vk	. . . . . . . . . . . 12 setvar 𝑘
11	10	cv 1541	. . . . . . . . . . 11 class 𝑘
12		cexp 14027	. . . . . . . . . . 11 class ↑
13	9, 11, 12	co 7409	. . . . . . . . . 10 class (i↑𝑘)
14		cdiv 11871	. . . . . . . . . 10 class /
15	8, 13, 14	co 7409	. . . . . . . . 9 class ((𝑓‘𝑥) / (i↑𝑘))
16		cre 15044	. . . . . . . . 9 class ℜ
17	15, 16	cfv 6544	. . . . . . . 8 class (ℜ‘((𝑓‘𝑥) / (i↑𝑘)))
18	7	cdm 5677	. . . . . . . . . . 11 class dom 𝑓
19	5, 18	wcel 2107	. . . . . . . . . 10 wff 𝑥 ∈ dom 𝑓
20		cc0 11110	. . . . . . . . . . 11 class 0
21	4	cv 1541	. . . . . . . . . . 11 class 𝑦
22		cle 11249	. . . . . . . . . . 11 class ≤
23	20, 21, 22	wbr 5149	. . . . . . . . . 10 wff 0 ≤ 𝑦
24	19, 23	wa 397	. . . . . . . . 9 wff (𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦)
25	24, 21, 20	cif 4529	. . . . . . . 8 class if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
26	4, 17, 25	csb 3894	. . . . . . 7 class ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	2, 3, 26	cmpt 5232	. . . . . 6 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))
28		citg2 25133	. . . . . 6 class ∫2
29	27, 28	cfv 6544	. . . . 5 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)))
30	29, 3	wcel 2107	. . . 4 wff (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
31		c3 12268	. . . . 5 class 3
32		cfz 13484	. . . . 5 class ...
33	20, 31, 32	co 7409	. . . 4 class (0...3)
34	30, 10, 33	wral 3062	. . 3 wff ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
35		cmbf 25131	. . 3 class MblFn
36	34, 6, 35	crab 3433	. 2 class {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
37	1, 36	wceq 1542	1 wff 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}

This definition is referenced by:  isibl  25283  iblmbf  25285