Definition df-ibl 24225

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 24220	. 2 class 𝐿1
2		vx	. . . . . . 7 setvar 𝑥
3		cr 10538	. . . . . . 7 class ℝ
4		vy	. . . . . . . 8 setvar 𝑦
5	2	cv 1536	. . . . . . . . . . 11 class 𝑥
6		vf	. . . . . . . . . . . 12 setvar 𝑓
7	6	cv 1536	. . . . . . . . . . 11 class 𝑓
8	5, 7	cfv 6357	. . . . . . . . . 10 class (𝑓‘𝑥)
9		ci 10541	. . . . . . . . . . 11 class i
10		vk	. . . . . . . . . . . 12 setvar 𝑘
11	10	cv 1536	. . . . . . . . . . 11 class 𝑘
12		cexp 13432	. . . . . . . . . . 11 class ↑
13	9, 11, 12	co 7158	. . . . . . . . . 10 class (i↑𝑘)
14		cdiv 11299	. . . . . . . . . 10 class /
15	8, 13, 14	co 7158	. . . . . . . . 9 class ((𝑓‘𝑥) / (i↑𝑘))
16		cre 14458	. . . . . . . . 9 class ℜ
17	15, 16	cfv 6357	. . . . . . . 8 class (ℜ‘((𝑓‘𝑥) / (i↑𝑘)))
18	7	cdm 5557	. . . . . . . . . . 11 class dom 𝑓
19	5, 18	wcel 2114	. . . . . . . . . 10 wff 𝑥 ∈ dom 𝑓
20		cc0 10539	. . . . . . . . . . 11 class 0
21	4	cv 1536	. . . . . . . . . . 11 class 𝑦
22		cle 10678	. . . . . . . . . . 11 class ≤
23	20, 21, 22	wbr 5068	. . . . . . . . . 10 wff 0 ≤ 𝑦
24	19, 23	wa 398	. . . . . . . . 9 wff (𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦)
25	24, 21, 20	cif 4469	. . . . . . . 8 class if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
26	4, 17, 25	csb 3885	. . . . . . 7 class ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	2, 3, 26	cmpt 5148	. . . . . 6 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))
28		citg2 24219	. . . . . 6 class ∫2
29	27, 28	cfv 6357	. . . . 5 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)))
30	29, 3	wcel 2114	. . . 4 wff (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
31		c3 11696	. . . . 5 class 3
32		cfz 12895	. . . . 5 class ...
33	20, 31, 32	co 7158	. . . 4 class (0...3)
34	30, 10, 33	wral 3140	. . 3 wff ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
35		cmbf 24217	. . 3 class MblFn
36	34, 6, 35	crab 3144	. 2 class {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
37	1, 36	wceq 1537	1 wff 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}

This definition is referenced by:  isibl  24368  iblmbf  24370