Home | Metamath
Proof Explorer Theorem List (p. 251 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itg1climres 25001* | Restricting the simple function πΉ to the increasing sequence π΄(π) of measurable sets whose union is β yields a sequence of simple functions whose integrals approach the integral of πΉ. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β π΄:ββΆdom vol) & β’ ((π β§ π β β) β (π΄βπ) β (π΄β(π + 1))) & β’ (π β βͺ ran π΄ = β) & β’ (π β πΉ β dom β«1) & β’ πΊ = (π₯ β β β¦ if(π₯ β (π΄βπ), (πΉβπ₯), 0)) β β’ (π β (π β β β¦ (β«1βπΊ)) β (β«1βπΉ)) | ||
Theorem | mbfi1fseqlem1 25002* | Lemma for mbfi1fseq 25008. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) β β’ (π β π½:(β Γ β)βΆ(0[,)+β)) | ||
Theorem | mbfi1fseqlem2 25003* | Lemma for mbfi1fseq 25008. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) & β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) β β’ (π΄ β β β (πΊβπ΄) = (π₯ β β β¦ if(π₯ β (-π΄[,]π΄), if((π΄π½π₯) β€ π΄, (π΄π½π₯), π΄), 0))) | ||
Theorem | mbfi1fseqlem3 25004* | Lemma for mbfi1fseq 25008. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) & β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) β β’ ((π β§ π΄ β β) β (πΊβπ΄):ββΆran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) | ||
Theorem | mbfi1fseqlem4 25005* | Lemma for mbfi1fseq 25008. This lemma is not as interesting as it is long - it is simply checking that πΊ is in fact a sequence of simple functions, by verifying that its range is in (0...π2βπ) / (2βπ) (which is to say, the numbers from 0 to π in increments of 1 / (2βπ)), and also that the preimage of each point π is measurable, because it is equal to (-π[,]π) β© (β‘πΉ β (π[,)π + 1 / (2βπ))) for π < π and (-π[,]π) β© (β‘πΉ β (π[,)+β)) for π = π. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) & β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) β β’ (π β πΊ:ββΆdom β«1) | ||
Theorem | mbfi1fseqlem5 25006* | Lemma for mbfi1fseq 25008. Verify that πΊ describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) & β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) β β’ ((π β§ π΄ β β) β (0π βr β€ (πΊβπ΄) β§ (πΊβπ΄) βr β€ (πΊβ(π΄ + 1)))) | ||
Theorem | mbfi1fseqlem6 25007* | Lemma for mbfi1fseq 25008. Verify that πΊ converges pointwise to πΉ, and wrap up the existential quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) & β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) β β’ (π β βπ(π:ββΆdom β«1 β§ βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) | ||
Theorem | mbfi1fseq 25008* | A characterization of measurability in terms of simple functions (this is an if and only if for nonnegative functions, although we don't prove it). Any nonnegative measurable function is the limit of an increasing sequence of nonnegative simple functions. This proof is an example of a poor de Bruijn factor - the formalized proof is much longer than an average hand proof, which usually just describes the function πΊ and "leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) β β’ (π β βπ(π:ββΆdom β«1 β§ βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) | ||
Theorem | mbfi1flimlem 25009* | Lemma for mbfi1flim 25010. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆβ) β β’ (π β βπ(π:ββΆdom β«1 β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) | ||
Theorem | mbfi1flim 25010* | Any real measurable function has a sequence of simple functions that converges to it. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:π΄βΆβ) β β’ (π β βπ(π:ββΆdom β«1 β§ βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) | ||
Theorem | mbfmullem2 25011* | Lemma for mbfmul 25013. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) & β’ (π β π:ββΆdom β«1) & β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) & β’ (π β π:ββΆdom β«1) & β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯)) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | mbfmullem 25012 | Lemma for mbfmul 25013. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | mbfmul 25013 | The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | itg2lcl 25014* | The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ πΏ β β* | ||
Theorem | itg2val 25015* | Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) = sup(πΏ, β*, < )) | ||
Theorem | itg2l 25016* | Elementhood in the set πΏ of lower sums of the integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ (π΄ β πΏ β βπ β dom β«1(π βr β€ πΉ β§ π΄ = (β«1βπ))) | ||
Theorem | itg2lr 25017* | Sufficient condition for elementhood in the set πΏ. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ ((πΊ β dom β«1 β§ πΊ βr β€ πΉ) β (β«1βπΊ) β πΏ) | ||
Theorem | xrge0f 25018 | A real function is a nonnegative extended real function if all its values are greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 28-Jul-2014.) |
β’ ((πΉ:ββΆβ β§ 0π βr β€ πΉ) β πΉ:ββΆ(0[,]+β)) | ||
Theorem | itg2cl 25019 | The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) β β*) | ||
Theorem | itg2ub 25020 | The integral of a nonnegative real function πΉ is an upper bound on the integrals of all simple functions πΊ dominated by πΉ. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ ((πΉ:ββΆ(0[,]+β) β§ πΊ β dom β«1 β§ πΊ βr β€ πΉ) β (β«1βπΊ) β€ (β«2βπΉ)) | ||
Theorem | itg2leub 25021* | Any upper bound on the integrals of all simple functions πΊ dominated by πΉ is greater than (β«2βπΉ), the least upper bound. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ ((πΉ:ββΆ(0[,]+β) β§ π΄ β β*) β ((β«2βπΉ) β€ π΄ β βπ β dom β«1(π βr β€ πΉ β (β«1βπ) β€ π΄))) | ||
Theorem | itg2ge0 25022 | The integral of a nonnegative real function is greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (πΉ:ββΆ(0[,]+β) β 0 β€ (β«2βπΉ)) | ||
Theorem | itg2itg1 25023 | The integral of a nonnegative simple function using β«2 is the same as its value under β«1. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ 0π βr β€ πΉ) β (β«2βπΉ) = (β«1βπΉ)) | ||
Theorem | itg20 25024 | The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (β«2β(β Γ {0})) = 0 | ||
Theorem | itg2lecl 25025 | If an β«2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ ((πΉ:ββΆ(0[,]+β) β§ π΄ β β β§ (β«2βπΉ) β€ π΄) β (β«2βπΉ) β β) | ||
Theorem | itg2le 25026 | If one function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ ((πΉ:ββΆ(0[,]+β) β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β (β«2βπΉ) β€ (β«2βπΊ)) | ||
Theorem | itg2const 25027* | Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ ((π΄ β dom vol β§ (volβπ΄) β β β§ π΅ β (0[,)+β)) β (β«2β(π₯ β β β¦ if(π₯ β π΄, π΅, 0))) = (π΅ Β· (volβπ΄))) | ||
Theorem | itg2const2 25028* | When the base set of a constant function has infinite volume, the integral is also infinite and vice-versa. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β+) β ((volβπ΄) β β β (β«2β(π₯ β β β¦ if(π₯ β π΄, π΅, 0))) β β)) | ||
Theorem | itg2seq 25029* | Definitional property of the β«2 integral: for any function πΉ there is a countable sequence π of simple functions less than πΉ whose integrals converge to the integral of πΉ. (This theorem is for the most part unnecessary in lieu of itg2i1fseq 25042, but unlike that theorem this one doesn't require πΉ to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014.) |
β’ (πΉ:ββΆ(0[,]+β) β βπ(π:ββΆdom β«1 β§ βπ β β (πβπ) βr β€ πΉ β§ (β«2βπΉ) = sup(ran (π β β β¦ (β«1β(πβπ))), β*, < ))) | ||
Theorem | itg2uba 25030* | Approximate version of itg2ub 25020. If πΉ approximately dominates πΊ, then β«1πΊ β€ β«2πΉ. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,]+β)) & β’ (π β πΊ β dom β«1) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΊβπ₯) β€ (πΉβπ₯)) β β’ (π β (β«1βπΊ) β€ (β«2βπΉ)) | ||
Theorem | itg2lea 25031* | Approximate version of itg2le 25026. If πΉ β€ πΊ for almost all π₯, then β«2πΉ β€ β«2πΊ. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,]+β)) & β’ (π β πΊ:ββΆ(0[,]+β)) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (β«2βπΉ) β€ (β«2βπΊ)) | ||
Theorem | itg2eqa 25032* | Approximate equality of integrals. If πΉ = πΊ for almost all π₯, then β«2πΉ = β«2πΊ. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,]+β)) & β’ (π β πΊ:ββΆ(0[,]+β)) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) = (πΊβπ₯)) β β’ (π β (β«2βπΉ) = (β«2βπΊ)) | ||
Theorem | itg2mulclem 25033 | Lemma for itg2mulc 25034. (Contributed by Mario Carneiro, 8-Jul-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β π΄ β β+) β β’ (π β (β«2β((β Γ {π΄}) βf Β· πΉ)) β€ (π΄ Β· (β«2βπΉ))) | ||
Theorem | itg2mulc 25034 | The integral of a nonnegative constant times a function is the constant times the integral of the original function. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β π΄ β (0[,)+β)) β β’ (π β (β«2β((β Γ {π΄}) βf Β· πΉ)) = (π΄ Β· (β«2βπΉ))) | ||
Theorem | itg2splitlem 25035* | Lemma for itg2split 25036. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β π΄ β dom vol) & β’ (π β π΅ β dom vol) & β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β (0[,]+β)) & β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, πΆ, 0)) & β’ πΊ = (π₯ β β β¦ if(π₯ β π΅, πΆ, 0)) & β’ π» = (π₯ β β β¦ if(π₯ β π, πΆ, 0)) & β’ (π β (β«2βπΉ) β β) & β’ (π β (β«2βπΊ) β β) β β’ (π β (β«2βπ») β€ ((β«2βπΉ) + (β«2βπΊ))) | ||
Theorem | itg2split 25036* | The β«2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25046, which requires countable choice. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β π΄ β dom vol) & β’ (π β π΅ β dom vol) & β’ (π β (vol*β(π΄ β© π΅)) = 0) & β’ (π β π = (π΄ βͺ π΅)) & β’ ((π β§ π₯ β π) β πΆ β (0[,]+β)) & β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, πΆ, 0)) & β’ πΊ = (π₯ β β β¦ if(π₯ β π΅, πΆ, 0)) & β’ π» = (π₯ β β β¦ if(π₯ β π, πΆ, 0)) & β’ (π β (β«2βπΉ) β β) & β’ (π β (β«2βπΊ) β β) β β’ (π β (β«2βπ») = ((β«2βπΉ) + (β«2βπΊ))) | ||
Theorem | itg2monolem1 25037* | Lemma for itg2mono 25040. We show that for any constant π‘ less than one, π‘ Β· β«1π» is less than π, and so β«1π» β€ π, which is one half of the equality in itg2mono 25040. Consider the sequence π΄(π) = {π₯ β£ π‘ Β· π» β€ πΉ(π)}. This is an increasing sequence of measurable sets whose union is β, and so π» βΎ π΄(π) has an integral which equals β«1π» in the limit, by itg1climres 25001. Then by taking the limit in (π‘ Β· π») βΎ π΄(π) β€ πΉ(π), we get π‘ Β· β«1π» β€ π as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΊ = (π₯ β β β¦ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) & β’ ((π β§ π β β) β (πΉβπ) β MblFn) & β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) & β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) & β’ ((π β§ π₯ β β) β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦) & β’ π = sup(ran (π β β β¦ (β«2β(πΉβπ))), β*, < ) & β’ (π β π β (0(,)1)) & β’ (π β π» β dom β«1) & β’ (π β π» βr β€ πΊ) & β’ (π β π β β) & β’ π΄ = (π β β β¦ {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) β β’ (π β (π Β· (β«1βπ»)) β€ π) | ||
Theorem | itg2monolem2 25038* | Lemma for itg2mono 25040. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ πΊ = (π₯ β β β¦ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) & β’ ((π β§ π β β) β (πΉβπ) β MblFn) & β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) & β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) & β’ ((π β§ π₯ β β) β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦) & β’ π = sup(ran (π β β β¦ (β«2β(πΉβπ))), β*, < ) & β’ (π β π β dom β«1) & β’ (π β π βr β€ πΊ) & β’ (π β Β¬ (β«1βπ) β€ π) β β’ (π β π β β) | ||
Theorem | itg2monolem3 25039* | Lemma for itg2mono 25040. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ πΊ = (π₯ β β β¦ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) & β’ ((π β§ π β β) β (πΉβπ) β MblFn) & β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) & β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) & β’ ((π β§ π₯ β β) β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦) & β’ π = sup(ran (π β β β¦ (β«2β(πΉβπ))), β*, < ) & β’ (π β π β dom β«1) & β’ (π β π βr β€ πΊ) & β’ (π β Β¬ (β«1βπ) β€ π) β β’ (π β (β«1βπ) β€ π) | ||
Theorem | itg2mono 25040* | The Monotone Convergence Theorem for nonnegative functions. If {(πΉβπ):π β β} is a monotone increasing sequence of positive, measurable, real-valued functions, and πΊ is the pointwise limit of the sequence, then (β«2βπΊ) is the limit of the sequence {(β«2β(πΉβπ)):π β β}. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ πΊ = (π₯ β β β¦ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) & β’ ((π β§ π β β) β (πΉβπ) β MblFn) & β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) & β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) & β’ ((π β§ π₯ β β) β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦) & β’ π = sup(ran (π β β β¦ (β«2β(πΉβπ))), β*, < ) β β’ (π β (β«2βπΊ) = π) | ||
Theorem | itg2i1fseqle 25041* | Subject to the conditions coming from mbfi1fseq 25008, the sequence of simple functions are all less than the target function πΉ. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β π:ββΆdom β«1) & β’ (π β βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) & β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) β β’ ((π β§ π β β) β (πβπ) βr β€ πΉ) | ||
Theorem | itg2i1fseq 25042* | Subject to the conditions coming from mbfi1fseq 25008, the integral of the sequence of simple functions converges to the integral of the target function. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β π:ββΆdom β«1) & β’ (π β βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) & β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) & β’ π = (π β β β¦ (β«1β(πβπ))) β β’ (π β (β«2βπΉ) = sup(ran π, β*, < )) | ||
Theorem | itg2i1fseq2 25043* | In an extension to the results of itg2i1fseq 25042, if there is an upper bound on the integrals of the simple functions approaching πΉ, then β«2πΉ is real and the standard limit relation applies. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β π:ββΆdom β«1) & β’ (π β βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) & β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) & β’ π = (π β β β¦ (β«1β(πβπ))) & β’ (π β π β β) & β’ ((π β§ π β β) β (β«1β(πβπ)) β€ π) β β’ (π β π β (β«2βπΉ)) | ||
Theorem | itg2i1fseq3 25044* | Special case of itg2i1fseq2 25043: if the integral of πΉ is a real number, then the standard limit relation holds on the integrals of simple functions approaching πΉ. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β π:ββΆdom β«1) & β’ (π β βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) & β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) & β’ π = (π β β β¦ (β«1β(πβπ))) & β’ (π β (β«2βπΉ) β β) β β’ (π β π β (β«2βπΉ)) | ||
Theorem | itg2addlem 25045* | Lemma for itg2add 25046. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΊ β MblFn) & β’ (π β πΊ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΊ) β β) & β’ (π β π:ββΆdom β«1) & β’ (π β βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) & β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) & β’ (π β π:ββΆdom β«1) & β’ (π β βπ β β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) & β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯)) β β’ (π β (β«2β(πΉ βf + πΊ)) = ((β«2βπΉ) + (β«2βπΊ))) | ||
Theorem | itg2add 25046 | The β«2 integral is linear. (Measurability is an essential component of this theorem; otherwise consider the characteristic function of a nonmeasurable set and its complement.) (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΊ β MblFn) & β’ (π β πΊ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΊ) β β) β β’ (π β (β«2β(πΉ βf + πΊ)) = ((β«2βπΉ) + (β«2βπΊ))) | ||
Theorem | itg2gt0 25047* | If the function πΉ is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ (π β π΄ β dom vol) & β’ (π β 0 < (volβπ΄)) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β πΉ β MblFn) & β’ ((π β§ π₯ β π΄) β 0 < (πΉβπ₯)) β β’ (π β 0 < (β«2βπΉ)) | ||
Theorem | itg2cnlem1 25048* | Lemma for itgcn 25131. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β πΉ β MblFn) & β’ (π β (β«2βπΉ) β β) β β’ (π β sup(ran (π β β β¦ (β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) = (β«2βπΉ)) | ||
Theorem | itg2cnlem2 25049* | Lemma for itgcn 25131. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β πΉ β MblFn) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΆ β β+) & β’ (π β π β β) & β’ (π β Β¬ (β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) β β’ (π β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) | ||
Theorem | itg2cn 25050* | A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a 25323 which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β πΉ β MblFn) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΆ β β+) β β’ (π β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) | ||
Theorem | ibllem 25051 | Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β if((π₯ β π΄ β§ 0 β€ π΅), π΅, 0) = if((π₯ β π΄ β§ 0 β€ πΆ), πΆ, 0)) | ||
Theorem | isibl 25052* | The predicate "πΉ is integrable". The "integrable" predicate corresponds roughly to the range of validity of β«π΄π΅ dπ₯, which is to say that the expression β«π΄π΅ dπ₯ doesn't make sense unless (π₯ β π΄ β¦ π΅) β πΏ1. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΊ = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π), π, 0))) & β’ ((π β§ π₯ β π΄) β π = (ββ(π΅ / (iβπ)))) & β’ (π β dom πΉ = π΄) & β’ ((π β§ π₯ β π΄) β (πΉβπ₯) = π΅) β β’ (π β (πΉ β πΏ1 β (πΉ β MblFn β§ βπ β (0...3)(β«2βπΊ) β β))) | ||
Theorem | isibl2 25053* | The predicate "πΉ is integrable" when πΉ is a mapping operation. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΊ = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π), π, 0))) & β’ ((π β§ π₯ β π΄) β π = (ββ(π΅ / (iβπ)))) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β ((π₯ β π΄ β¦ π΅) β MblFn β§ βπ β (0...3)(β«2βπΊ) β β))) | ||
Theorem | iblmbf 25054 | An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.) |
β’ (πΉ β πΏ1 β πΉ β MblFn) | ||
Theorem | iblitg 25055* | If a function is integrable, then the β«2 integrals of the function's decompositions all exist. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΊ = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π), π, 0))) & β’ ((π β§ π₯ β π΄) β π = (ββ(π΅ / (iβπΎ)))) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ ((π β§ πΎ β β€) β (β«2βπΊ) β β) | ||
Theorem | dfitg 25056* | Evaluate the class substitution in df-itg 24909. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ π = (ββ(π΅ / (iβπ))) β β’ β«π΄π΅ dπ₯ = Ξ£π β (0...3)((iβπ) Β· (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π), π, 0)))) | ||
Theorem | itgex 25057 | An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β«π΄π΅ dπ₯ β V | ||
Theorem | itgeq1f 25058 | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ (π΄ = π΅ β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | itgeq1 25059* | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (π΄ = π΅ β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | nfitg1 25060 | Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β²π₯β«π΄π΅ dπ₯ | ||
Theorem | nfitg 25061* | Bound-variable hypothesis builder for an integral: if π¦ is (effectively) not free in π΄ and π΅, it is not free in β«π΄π΅ dπ₯. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β²π¦π΄ & β’ β²π¦π΅ β β’ β²π¦β«π΄π΅ dπ₯ | ||
Theorem | cbvitg 25062* | Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (π₯ = π¦ β π΅ = πΆ) & β’ β²π¦π΅ & β’ β²π₯πΆ β β’ β«π΄π΅ dπ₯ = β«π΄πΆ dπ¦ | ||
Theorem | cbvitgv 25063* | Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (π₯ = π¦ β π΅ = πΆ) β β’ β«π΄π΅ dπ₯ = β«π΄πΆ dπ¦ | ||
Theorem | itgeq2 25064 | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (βπ₯ β π΄ π΅ = πΆ β β«π΄π΅ dπ₯ = β«π΄πΆ dπ₯) | ||
Theorem | itgresr 25065 | The domain of an integral only matters in its intersection with β. (Contributed by Mario Carneiro, 29-Jun-2014.) |
β’ β«π΄π΅ dπ₯ = β«(π΄ β© β)π΅ dπ₯ | ||
Theorem | itg0 25066 | The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014.) |
β’ β«β π΄ dπ₯ = 0 | ||
Theorem | itgz 25067 | The integral of zero on any set is zero. (Contributed by Mario Carneiro, 29-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ β«π΄0 dπ₯ = 0 | ||
Theorem | itgeq2dv 25068* | Equality theorem for an integral. (Contributed by Mario Carneiro, 7-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β β«π΄π΅ dπ₯ = β«π΄πΆ dπ₯) | ||
Theorem | itgmpt 25069* | Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ (π β β«π΄π΅ dπ₯ = β«π΄((π₯ β π΄ β¦ π΅)βπ¦) dπ¦) | ||
Theorem | itgcl 25070* | The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β β«π΄π΅ dπ₯ β β) | ||
Theorem | itgvallem 25071* | Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (iβπΎ) = π β β’ (π = πΎ β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(π΅ / (iβπ)))), (ββ(π΅ / (iβπ))), 0))) = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(π΅ / π))), (ββ(π΅ / π)), 0)))) | ||
Theorem | itgvallem3 25072* | Lemma for itgposval 25082 and itgreval 25083. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ = 0) β β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π΅), π΅, 0))) = 0) | ||
Theorem | ibl0 25073 | The zero function is integrable on any measurable set. (Unlike iblconst 25104, this does not require π΄ to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.) |
β’ (π΄ β dom vol β (π΄ Γ {0}) β πΏ1) | ||
Theorem | iblcnlem1 25074* | Lemma for iblcnlem 25075. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β ((π₯ β π΄ β¦ π΅) β MblFn β§ (π β β β§ π β β) β§ (π β β β§ π β β)))) | ||
Theorem | iblcnlem 25075* | Expand out the universal quantifier in isibl2 25053. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β ((π₯ β π΄ β¦ π΅) β MblFn β§ (π β β β§ π β β) β§ (π β β β§ π β β)))) | ||
Theorem | itgcnlem 25076* | Expand out the sum in dfitg 25056. (Contributed by Mario Carneiro, 1-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββπ΅)), (ββπ΅), 0))) & β’ π = (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(ββπ΅)), -(ββπ΅), 0))) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β β«π΄π΅ dπ₯ = ((π β π) + (i Β· (π β π)))) | ||
Theorem | iblrelem 25077* | Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β ((π₯ β π΄ β¦ π΅) β MblFn β§ (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π΅), π΅, 0))) β β β§ (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -π΅), -π΅, 0))) β β))) | ||
Theorem | iblposlem 25078* | Lemma for iblpos 25079. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -π΅), -π΅, 0))) = 0) | ||
Theorem | iblpos 25079* | Integrability of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β ((π₯ β π΄ β¦ π΅) β MblFn β§ (β«2β(π₯ β β β¦ if(π₯ β π΄, π΅, 0))) β β))) | ||
Theorem | iblre 25080* | Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β πΏ1 β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β πΏ1))) | ||
Theorem | itgrevallem1 25081* | Lemma for itgposval 25082 and itgreval 25083. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β β«π΄π΅ dπ₯ = ((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π΅), π΅, 0))) β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -π΅), -π΅, 0))))) | ||
Theorem | itgposval 25082* | The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β β«π΄π΅ dπ₯ = (β«2β(π₯ β β β¦ if(π₯ β π΄, π΅, 0)))) | ||
Theorem | itgreval 25083* | Decompose the integral of a real function into positive and negative parts. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β β«π΄π΅ dπ₯ = (β«π΄if(0 β€ π΅, π΅, 0) dπ₯ β β«π΄if(0 β€ -π΅, -π΅, 0) dπ₯)) | ||
Theorem | itgrecl 25084* | Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β β«π΄π΅ dπ₯ β β) | ||
Theorem | iblcn 25085* | Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β ((π₯ β π΄ β¦ (ββπ΅)) β πΏ1 β§ (π₯ β π΄ β¦ (ββπ΅)) β πΏ1))) | ||
Theorem | itgcnval 25086* | Decompose the integral of a complex function into real and imaginary parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β β«π΄π΅ dπ₯ = (β«π΄(ββπ΅) dπ₯ + (i Β· β«π΄(ββπ΅) dπ₯))) | ||
Theorem | itgre 25087* | Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β (βββ«π΄π΅ dπ₯) = β«π΄(ββπ΅) dπ₯) | ||
Theorem | itgim 25088* | Imaginary part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β (βββ«π΄π΅ dπ₯) = β«π΄(ββπ΅) dπ₯) | ||
Theorem | iblneg 25089* | The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β (π₯ β π΄ β¦ -π΅) β πΏ1) | ||
Theorem | itgneg 25090* | Negation of an integral. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) β β’ (π β -β«π΄π΅ dπ₯ = β«π΄-π΅ dπ₯) | ||
Theorem | iblss 25091* | A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ (π β π΄ β π΅) & β’ (π β π΄ β dom vol) & β’ ((π β§ π₯ β π΅) β πΆ β π) & β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) | ||
Theorem | iblss2 25092* | Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β dom vol) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = 0) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) β β’ (π β (π₯ β π΅ β¦ πΆ) β πΏ1) | ||
Theorem | itgitg2 25093* | Transfer an integral using β«2 to an equivalent integral using β«. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β 0 β€ π΄) & β’ (π β (π₯ β β β¦ π΄) β πΏ1) β β’ (π β β«βπ΄ dπ₯ = (β«2β(π₯ β β β¦ π΄))) | ||
Theorem | i1fibl 25094 | A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ (πΉ β dom β«1 β πΉ β πΏ1) | ||
Theorem | itgitg1 25095* | Transfer an integral using β«1 to an equivalent integral using β«. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ (πΉ β dom β«1 β β«β(πΉβπ₯) dπ₯ = (β«1βπΉ)) | ||
Theorem | itgle 25096* | Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β β«π΄π΅ dπ₯ β€ β«π΄πΆ dπ₯) | ||
Theorem | itgge0 25097* | The integral of a positive function is positive. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β 0 β€ β«π΄π΅ dπ₯) | ||
Theorem | itgss 25098* | Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = 0) β β’ (π β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | itgss2 25099* | Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π΄ β π΅ β β«π΄πΆ dπ₯ = β«π΅if(π₯ β π΄, πΆ, 0) dπ₯) | ||
Theorem | itgeqa 25100* | Approximate equality of integrals. If πΆ(π₯) = π·(π₯) for almost all π₯, then β«π΅πΆ(π₯) dπ₯ = β«π΅π·(π₯) dπ₯ and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 2-Sep-2014.) |
β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) β β’ (π β (((π₯ β π΅ β¦ πΆ) β πΏ1 β (π₯ β π΅ β¦ π·) β πΏ1) β§ β«π΅πΆ dπ₯ = β«π΅π· dπ₯)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |