MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ibl Structured version   Visualization version   GIF version

Definition df-ibl 23297
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
StepHypRef Expression
1 cibl 23292 . 2 class 𝐿1
2 vx . . . . . . 7 setvar 𝑥
3 cr 9879 . . . . . . 7 class
4 vy . . . . . . . 8 setvar 𝑦
52cv 1479 . . . . . . . . . . 11 class 𝑥
6 vf . . . . . . . . . . . 12 setvar 𝑓
76cv 1479 . . . . . . . . . . 11 class 𝑓
85, 7cfv 5847 . . . . . . . . . 10 class (𝑓𝑥)
9 ci 9882 . . . . . . . . . . 11 class i
10 vk . . . . . . . . . . . 12 setvar 𝑘
1110cv 1479 . . . . . . . . . . 11 class 𝑘
12 cexp 12800 . . . . . . . . . . 11 class
139, 11, 12co 6604 . . . . . . . . . 10 class (i↑𝑘)
14 cdiv 10628 . . . . . . . . . 10 class /
158, 13, 14co 6604 . . . . . . . . 9 class ((𝑓𝑥) / (i↑𝑘))
16 cre 13771 . . . . . . . . 9 class
1715, 16cfv 5847 . . . . . . . 8 class (ℜ‘((𝑓𝑥) / (i↑𝑘)))
187cdm 5074 . . . . . . . . . . 11 class dom 𝑓
195, 18wcel 1987 . . . . . . . . . 10 wff 𝑥 ∈ dom 𝑓
20 cc0 9880 . . . . . . . . . . 11 class 0
214cv 1479 . . . . . . . . . . 11 class 𝑦
22 cle 10019 . . . . . . . . . . 11 class
2320, 21, 22wbr 4613 . . . . . . . . . 10 wff 0 ≤ 𝑦
2419, 23wa 384 . . . . . . . . 9 wff (𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦)
2524, 21, 20cif 4058 . . . . . . . 8 class if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
264, 17, 25csb 3514 . . . . . . 7 class (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
272, 3, 26cmpt 4673 . . . . . 6 class (𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))
28 citg2 23291 . . . . . 6 class 2
2927, 28cfv 5847 . . . . 5 class (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)))
3029, 3wcel 1987 . . . 4 wff (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
31 c3 11015 . . . . 5 class 3
32 cfz 12268 . . . . 5 class ...
3320, 31, 32co 6604 . . . 4 class (0...3)
3430, 10, 33wral 2907 . . 3 wff 𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
35 cmbf 23289 . . 3 class MblFn
3634, 6, 35crab 2911 . 2 class {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
371, 36wceq 1480 1 wff 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
Colors of variables: wff setvar class
This definition is referenced by:  isibl  23438  iblmbf  23440
  Copyright terms: Public domain W3C validator