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

Definition df-itg 25671
Description: Define the full Lebesgue integral, for complex-valued functions to . The syntax is designed to be suggestive of the standard notation for integrals. For example, our notation for the integral of 𝑥↑2 from 0 to 1 is ∫(0[,]1)(𝑥↑2) d𝑥 = (1 / 3). The only real function of this definition is to break the integral up into nonnegative real parts and send it off to df-itg2 25669 for further processing. Note that this definition cannot handle integrals which evaluate to infinity, because addition and multiplication are not currently defined on extended reals. (You can use df-itg2 25669 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.)
Assertion
Ref Expression
df-itg 𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘(𝐵 / (i↑𝑘))) / 𝑦if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
Distinct variable groups:   𝑦,𝑘,𝐴   𝐵,𝑘,𝑦   𝑥,𝑘,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-itg
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3citg 25666 . 2 class 𝐴𝐵 d𝑥
5 cc0 11152 . . . 4 class 0
6 c3 12319 . . . 4 class 3
7 cfz 13543 . . . 4 class ...
85, 6, 7co 7430 . . 3 class (0...3)
9 ci 11154 . . . . 5 class i
10 vk . . . . . 6 setvar 𝑘
1110cv 1535 . . . . 5 class 𝑘
12 cexp 14098 . . . . 5 class
139, 11, 12co 7430 . . . 4 class (i↑𝑘)
14 cr 11151 . . . . . 6 class
15 vy . . . . . . 7 setvar 𝑦
16 cdiv 11917 . . . . . . . . 9 class /
173, 13, 16co 7430 . . . . . . . 8 class (𝐵 / (i↑𝑘))
18 cre 15132 . . . . . . . 8 class
1917, 18cfv 6562 . . . . . . 7 class (ℜ‘(𝐵 / (i↑𝑘)))
201cv 1535 . . . . . . . . . 10 class 𝑥
2120, 2wcel 2105 . . . . . . . . 9 wff 𝑥𝐴
2215cv 1535 . . . . . . . . . 10 class 𝑦
23 cle 11293 . . . . . . . . . 10 class
245, 22, 23wbr 5147 . . . . . . . . 9 wff 0 ≤ 𝑦
2521, 24wa 395 . . . . . . . 8 wff (𝑥𝐴 ∧ 0 ≤ 𝑦)
2625, 22, 5cif 4530 . . . . . . 7 class if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
2715, 19, 26csb 3907 . . . . . 6 class (ℜ‘(𝐵 / (i↑𝑘))) / 𝑦if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
281, 14, 27cmpt 5230 . . . . 5 class (𝑥 ∈ ℝ ↦ (ℜ‘(𝐵 / (i↑𝑘))) / 𝑦if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))
29 citg2 25664 . . . . 5 class 2
3028, 29cfv 6562 . . . 4 class (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘(𝐵 / (i↑𝑘))) / 𝑦if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))
31 cmul 11157 . . . 4 class ·
3213, 30, 31co 7430 . . 3 class ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘(𝐵 / (i↑𝑘))) / 𝑦if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
338, 32, 10csu 15718 . 2 class Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘(𝐵 / (i↑𝑘))) / 𝑦if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
344, 33wceq 1536 1 wff 𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘(𝐵 / (i↑𝑘))) / 𝑦if((𝑥𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
Colors of variables: wff setvar class
This definition is referenced by:  dfitg  25818  itgex  25819  itgeq1f  25820  itgeq1  25822  nfitg1  25823  cbvitgv  25826  itgeq12i  36187  itgeq12sdv  36201  cbvitgvw2  36230  cbvitgdavw  36263  cbvitgdavw2  36279
  Copyright terms: Public domain W3C validator