![]() |
Metamath
Proof Explorer Theorem List (p. 253 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | i1frn 25201 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β ran πΉ β Fin) | ||
Theorem | i1fima 25202 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β‘πΉ β π΄) β dom vol) | ||
Theorem | i1fima2 25203 | Any preimage of a simple function not containing zero has finite measure. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ Β¬ 0 β π΄) β (volβ(β‘πΉ β π΄)) β β) | ||
Theorem | i1fima2sn 25204 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ π΄ β (π΅ β {0})) β (volβ(β‘πΉ β {π΄})) β β) | ||
Theorem | i1fd 25205* | A simplified set of assumptions to show that a given function is simple. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β ran πΉ β Fin) & β’ ((π β§ π₯ β (ran πΉ β {0})) β (β‘πΉ β {π₯}) β dom vol) & β’ ((π β§ π₯ β (ran πΉ β {0})) β (volβ(β‘πΉ β {π₯})) β β) β β’ (π β πΉ β dom β«1) | ||
Theorem | i1f0rn 25206 | Any simple function takes the value zero on a set of unbounded measure, so in particular this set is not empty. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β 0 β ran πΉ) | ||
Theorem | itg1val 25207* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) = Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) | ||
Theorem | itg1val2 25208* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ (π΄ β Fin β§ (ran πΉ β {0}) β π΄ β§ π΄ β (β β {0}))) β (β«1βπΉ) = Ξ£π₯ β π΄ (π₯ Β· (volβ(β‘πΉ β {π₯})))) | ||
Theorem | itg1cl 25209 | Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) β β) | ||
Theorem | itg1ge0 25210 | Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ 0π βr β€ πΉ) β 0 β€ (β«1βπΉ)) | ||
Theorem | i1f0 25211 | The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (β Γ {0}) β dom β«1 | ||
Theorem | itg10 25212 | The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (β«1β(β Γ {0})) = 0 | ||
Theorem | i1f1lem 25213* | Lemma for i1f1 25214 and itg11 25215. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, 1, 0)) β β’ (πΉ:ββΆ{0, 1} β§ (π΄ β dom vol β (β‘πΉ β {1}) = π΄)) | ||
Theorem | i1f1 25214* | Base case simple functions are indicator functions of measurable sets. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, 1, 0)) β β’ ((π΄ β dom vol β§ (volβπ΄) β β) β πΉ β dom β«1) | ||
Theorem | itg11 25215* | The integral of an indicator function is the volume of the set. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, 1, 0)) β β’ ((π΄ β dom vol β§ (volβπ΄) β β) β (β«1βπΉ) = (volβπ΄)) | ||
Theorem | itg1addlem1 25216* | Decompose a preimage, which is always a disjoint union. (Contributed by Mario Carneiro, 25-Jun-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ (π β πΉ:πβΆπ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (β‘πΉ β {π})) & β’ ((π β§ π β π΄) β π΅ β dom vol) & β’ ((π β§ π β π΄) β (volβπ΅) β β) β β’ (π β (volββͺ π β π΄ π΅) = Ξ£π β π΄ (volβπ΅)) | ||
Theorem | i1faddlem 25217* | Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ ((π β§ π΄ β β) β (β‘(πΉ βf + πΊ) β {π΄}) = βͺ π¦ β ran πΊ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦}))) | ||
Theorem | i1fmullem 25218* | Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ ((π β§ π΄ β (β β {0})) β (β‘(πΉ βf Β· πΊ) β {π΄}) = βͺ π¦ β (ran πΊ β {0})((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦}))) | ||
Theorem | i1fadd 25219 | The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ (π β (πΉ βf + πΊ) β dom β«1) | ||
Theorem | i1fmul 25220 | The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ (π β (πΉ βf Β· πΊ) β dom β«1) | ||
Theorem | itg1addlem2 25221* | Lemma for itg1add 25226. The function πΌ represents the pieces into which we will break up the domain of the sum. Since it is infinite only when both π and π are zero, we arbitrarily define it to be zero there to simplify the sums that are manipulated in itg1addlem4 25223 and itg1addlem5 25225. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) β β’ (π β πΌ:(β Γ β)βΆβ) | ||
Theorem | itg1addlem3 25222* | Lemma for itg1add 25226. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) β β’ (((π΄ β β β§ π΅ β β) β§ Β¬ (π΄ = 0 β§ π΅ = 0)) β (π΄πΌπ΅) = (volβ((β‘πΉ β {π΄}) β© (β‘πΊ β {π΅})))) | ||
Theorem | itg1addlem4 25223* | Lemma for itg1add 25226. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof shortened by SN, 3-Oct-2024.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) & β’ π = ( + βΎ (ran πΉ Γ ran πΊ)) β β’ (π β (β«1β(πΉ βf + πΊ)) = Ξ£π¦ β ran πΉΞ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§))) | ||
Theorem | itg1addlem4OLD 25224* | Obsolete version of itg1addlem4 25223. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) & β’ π = ( + βΎ (ran πΉ Γ ran πΊ)) β β’ (π β (β«1β(πΉ βf + πΊ)) = Ξ£π¦ β ran πΉΞ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§))) | ||
Theorem | itg1addlem5 25225* | Lemma for itg1add 25226. (Contributed by Mario Carneiro, 27-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) & β’ π = ( + βΎ (ran πΉ Γ ran πΊ)) β β’ (π β (β«1β(πΉ βf + πΊ)) = ((β«1βπΉ) + (β«1βπΊ))) | ||
Theorem | itg1add 25226 | The integral of a sum of simple functions is the sum of the integrals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ (π β (β«1β(πΉ βf + πΊ)) = ((β«1βπΉ) + (β«1βπΊ))) | ||
Theorem | i1fmulclem 25227 | Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) β β’ (((π β§ π΄ β 0) β§ π΅ β β) β (β‘((β Γ {π΄}) βf Β· πΉ) β {π΅}) = (β‘πΉ β {(π΅ / π΄)})) | ||
Theorem | i1fmulc 25228 | A nonnegative constant times a simple function gives another simple function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) β β’ (π β ((β Γ {π΄}) βf Β· πΉ) β dom β«1) | ||
Theorem | itg1mulc 25229 | The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) β β’ (π β (β«1β((β Γ {π΄}) βf Β· πΉ)) = (π΄ Β· (β«1βπΉ))) | ||
Theorem | i1fres 25230* | The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside π΄.) (Contributed by Mario Carneiro, 29-Jun-2014.) |
β’ πΊ = (π₯ β β β¦ if(π₯ β π΄, (πΉβπ₯), 0)) β β’ ((πΉ β dom β«1 β§ π΄ β dom vol) β πΊ β dom β«1) | ||
Theorem | i1fpos 25231* | The positive part of a simple function is simple. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΊ = (π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) β β’ (πΉ β dom β«1 β πΊ β dom β«1) | ||
Theorem | i1fposd 25232* | Deduction form of i1fposd 25232. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ (π β (π₯ β β β¦ π΄) β dom β«1) β β’ (π β (π₯ β β β¦ if(0 β€ π΄, π΄, 0)) β dom β«1) | ||
Theorem | i1fsub 25233 | The difference of two simple functions is a simple function. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ ((πΉ β dom β«1 β§ πΊ β dom β«1) β (πΉ βf β πΊ) β dom β«1) | ||
Theorem | itg1sub 25234 | The integral of a difference of two simple functions. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ ((πΉ β dom β«1 β§ πΊ β dom β«1) β (β«1β(πΉ βf β πΊ)) = ((β«1βπΉ) β (β«1βπΊ))) | ||
Theorem | itg10a 25235* | The integral of a simple function supported on a nullset is zero. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) = 0) β β’ (π β (β«1βπΉ) = 0) | ||
Theorem | itg1ge0a 25236* | The integral of an almost positive simple function is positive. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β 0 β€ (πΉβπ₯)) β β’ (π β 0 β€ (β«1βπΉ)) | ||
Theorem | itg1lea 25237* | Approximate version of itg1le 25238. If πΉ β€ πΊ for almost all π₯, then β«1πΉ β€ β«1πΊ. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ (π β πΊ β dom β«1) & β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (β«1βπΉ) β€ (β«1βπΊ)) | ||
Theorem | itg1le 25238 | If one simple function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.) |
β’ ((πΉ β dom β«1 β§ πΊ β dom β«1 β§ πΉ βr β€ πΊ) β (β«1βπΉ) β€ (β«1βπΊ)) | ||
Theorem | itg1climres 25239* | 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 25240* | Lemma for mbfi1fseq 25246. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) β β’ (π β π½:(β Γ β)βΆ(0[,)+β)) | ||
Theorem | mbfi1fseqlem2 25241* | Lemma for mbfi1fseq 25246. (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 25242* | Lemma for mbfi1fseq 25246. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) & β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) β β’ ((π β§ π΄ β β) β (πΊβπ΄):ββΆran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) | ||
Theorem | mbfi1fseqlem4 25243* | Lemma for mbfi1fseq 25246. 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 25244* | Lemma for mbfi1fseq 25246. 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 25245* | Lemma for mbfi1fseq 25246. 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 25246* | 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 25247* | Lemma for mbfi1flim 25248. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆβ) β β’ (π β βπ(π:ββΆdom β«1 β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) | ||
Theorem | mbfi1flim 25248* | 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 25249* | Lemma for mbfmul 25251. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) & β’ (π β π:ββΆdom β«1) & β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) & β’ (π β π:ββΆdom β«1) & β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯)) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | mbfmullem 25250 | Lemma for mbfmul 25251. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | mbfmul 25251 | The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | itg2lcl 25252* | The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ πΏ β β* | ||
Theorem | itg2val 25253* | Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) = sup(πΏ, β*, < )) | ||
Theorem | itg2l 25254* | 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 25255* | Sufficient condition for elementhood in the set πΏ. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ ((πΊ β dom β«1 β§ πΊ βr β€ πΉ) β (β«1βπΊ) β πΏ) | ||
Theorem | xrge0f 25256 | 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 25257 | The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) β β*) | ||
Theorem | itg2ub 25258 | 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 25259* | 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 25260 | 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 25261 | 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 25262 | The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (β«2β(β Γ {0})) = 0 | ||
Theorem | itg2lecl 25263 | If an β«2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ ((πΉ:ββΆ(0[,]+β) β§ π΄ β β β§ (β«2βπΉ) β€ π΄) β (β«2βπΉ) β β) | ||
Theorem | itg2le 25264 | 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 25265* | 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 25266* | 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 25267* | 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 25280, 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 25268* | Approximate version of itg2ub 25258. If πΉ approximately dominates πΊ, then β«1πΊ β€ β«2πΉ. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,]+β)) & β’ (π β πΊ β dom β«1) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΊβπ₯) β€ (πΉβπ₯)) β β’ (π β (β«1βπΊ) β€ (β«2βπΉ)) | ||
Theorem | itg2lea 25269* | Approximate version of itg2le 25264. If πΉ β€ πΊ for almost all π₯, then β«2πΉ β€ β«2πΊ. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,]+β)) & β’ (π β πΊ:ββΆ(0[,]+β)) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (β«2βπΉ) β€ (β«2βπΊ)) | ||
Theorem | itg2eqa 25270* | 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 25271 | Lemma for itg2mulc 25272. (Contributed by Mario Carneiro, 8-Jul-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β π΄ β β+) β β’ (π β (β«2β((β Γ {π΄}) βf Β· πΉ)) β€ (π΄ Β· (β«2βπΉ))) | ||
Theorem | itg2mulc 25272 | 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 25273* | Lemma for itg2split 25274. (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 25274* | The β«2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25284, 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 25275* | Lemma for itg2mono 25278. 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 25278. 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 25239. 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 25276* | Lemma for itg2mono 25278. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ πΊ = (π₯ β β β¦ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) & β’ ((π β§ π β β) β (πΉβπ) β MblFn) & β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) & β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) & β’ ((π β§ π₯ β β) β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦) & β’ π = sup(ran (π β β β¦ (β«2β(πΉβπ))), β*, < ) & β’ (π β π β dom β«1) & β’ (π β π βr β€ πΊ) & β’ (π β Β¬ (β«1βπ) β€ π) β β’ (π β π β β) | ||
Theorem | itg2monolem3 25277* | Lemma for itg2mono 25278. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ πΊ = (π₯ β β β¦ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) & β’ ((π β§ π β β) β (πΉβπ) β MblFn) & β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) & β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) & β’ ((π β§ π₯ β β) β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦) & β’ π = sup(ran (π β β β¦ (β«2β(πΉβπ))), β*, < ) & β’ (π β π β dom β«1) & β’ (π β π βr β€ πΊ) & β’ (π β Β¬ (β«1βπ) β€ π) β β’ (π β (β«1βπ) β€ π) | ||
Theorem | itg2mono 25278* | 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 25279* | Subject to the conditions coming from mbfi1fseq 25246, 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 25280* | Subject to the conditions coming from mbfi1fseq 25246, 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 25281* | In an extension to the results of itg2i1fseq 25280, 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 25282* | Special case of itg2i1fseq2 25281: 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 25283* | Lemma for itg2add 25284. (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 25284 | 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 25285* | 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 25286* | Lemma for itgcn 25369. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β πΉ β MblFn) & β’ (π β (β«2βπΉ) β β) β β’ (π β sup(ran (π β β β¦ (β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) = (β«2βπΉ)) | ||
Theorem | itg2cnlem2 25287* | Lemma for itgcn 25369. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β πΉ β MblFn) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΆ β β+) & β’ (π β π β β) & β’ (π β Β¬ (β«2β(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) β€ ((β«2βπΉ) β (πΆ / 2))) β β’ (π β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) | ||
Theorem | itg2cn 25288* | A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a 25561 which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β πΉ β MblFn) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΆ β β+) β β’ (π β βπ β β+ βπ’ β dom vol((volβπ’) < π β (β«2β(π₯ β β β¦ if(π₯ β π’, (πΉβπ₯), 0))) < πΆ)) | ||
Theorem | ibllem 25289 | Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β if((π₯ β π΄ β§ 0 β€ π΅), π΅, 0) = if((π₯ β π΄ β§ 0 β€ πΆ), πΆ, 0)) | ||
Theorem | isibl 25290* | 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 25291* | 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 25292 | An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.) |
β’ (πΉ β πΏ1 β πΉ β MblFn) | ||
Theorem | iblitg 25293* | 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 25294* | Evaluate the class substitution in df-itg 25147. (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 25295 | An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β«π΄π΅ dπ₯ β V | ||
Theorem | itgeq1f 25296 | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ (π΄ = π΅ β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | itgeq1 25297* | Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (π΄ = π΅ β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) | ||
Theorem | nfitg1 25298 | Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β²π₯β«π΄π΅ dπ₯ | ||
Theorem | nfitg 25299* | 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 25300* | Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (π₯ = π¦ β π΅ = πΆ) & β’ β²π¦π΅ & β’ β²π₯πΆ β β’ β«π΄π΅ dπ₯ = β«π΄πΆ dπ¦ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |