![]() |
Metamath
Proof Explorer Theorem List (p. 255 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mbfposr 25401* | Converse to mbfpos 25400. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) & β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) β β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) | ||
Theorem | mbfposb 25402* | A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β MblFn β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn))) | ||
Theorem | ismbf3d 25403* | Simplified form of ismbfd 25388. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfimaopnlem 25404* | Lemma for mbfimaopn 25405. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ π½ = (TopOpenββfld) & β’ πΊ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π΅ = ((,) β (β Γ β)) & β’ πΎ = ran (π₯ β π΅, π¦ β π΅ β¦ (π₯ Γ π¦)) β β’ ((πΉ β MblFn β§ π΄ β π½) β (β‘πΉ β π΄) β dom vol) | ||
Theorem | mbfimaopn 25405 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 25407, which explains why π΄ β dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ π½ = (TopOpenββfld) β β’ ((πΉ β MblFn β§ π΄ β π½) β (β‘πΉ β π΄) β dom vol) | ||
Theorem | mbfimaopn2 25406 | The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π΅) β β’ (((πΉ β MblFn β§ πΉ:π΄βΆπ΅ β§ π΅ β β) β§ πΆ β πΎ) β (β‘πΉ β πΆ) β dom vol) | ||
Theorem | cncombf 25407 | The composition of a continuous function with a measurable function is measurable. (More generally, πΊ can be a Borel-measurable function, but notably the condition that πΊ be only measurable is too weak, the usual counterexample taking πΊ to be the Cantor function and πΉ the indicator function of the πΊ-image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ ((πΉ β MblFn β§ πΉ:π΄βΆπ΅ β§ πΊ β (π΅βcnββ)) β (πΊ β πΉ) β MblFn) | ||
Theorem | cnmbf 25408 | A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 26-Mar-2015.) |
β’ ((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β πΉ β MblFn) | ||
Theorem | mbfaddlem 25409 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfadd 25410 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfsub 25411 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf β πΊ) β MblFn) | ||
Theorem | mbfmulc2 25412* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) | ||
Theorem | mbfsup 25413* | The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, π΅(π, π₯) is a function of both π and π₯, since it is an π-indexed sequence of functions on π₯. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ πΊ = (π₯ β π΄ β¦ sup(ran (π β π β¦ π΅), β, < )) & β’ (π β π β β€) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) & β’ ((π β§ π₯ β π΄) β βπ¦ β β βπ β π π΅ β€ π¦) β β’ (π β πΊ β MblFn) | ||
Theorem | mbfinf 25414* | The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 13-Sep-2020.) |
β’ π = (β€β₯βπ) & β’ πΊ = (π₯ β π΄ β¦ inf(ran (π β π β¦ π΅), β, < )) & β’ (π β π β β€) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) & β’ ((π β§ π₯ β π΄) β βπ¦ β β βπ β π π¦ β€ π΅) β β’ (π β πΊ β MblFn) | ||
Theorem | mbflimsup 25415* | The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
β’ π = (β€β₯βπ) & β’ πΊ = (π₯ β π΄ β¦ (lim supβ(π β π β¦ π΅))) & β’ π» = (π β β β¦ sup((((π β π β¦ π΅) β (π[,)+β)) β© β*), β*, < )) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (lim supβ(π β π β¦ π΅)) β β) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) β β’ (π β πΊ β MblFn) | ||
Theorem | mbflimlem 25416* | The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Theorem | mbflim 25417* | The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β π) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Syntax | c0p 25418 | Extend class notation to include the zero polynomial. |
class 0π | ||
Definition | df-0p 25419 | Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ 0π = (β Γ {0}) | ||
Theorem | 0pval 25420 | The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β (0πβπ΄) = 0) | ||
Theorem | 0plef 25421 | Two ways to say that the function πΉ on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (πΉ:ββΆ(0[,)+β) β (πΉ:ββΆβ β§ 0π βr β€ πΉ)) | ||
Theorem | 0pledm 25422 | Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ (π β π΄ β β) & β’ (π β πΉ Fn π΄) β β’ (π β (0π βr β€ πΉ β (π΄ Γ {0}) βr β€ πΉ)) | ||
Theorem | isi1f 25423 | The predicate "πΉ is a simple function". A simple function is a finite nonnegative linear combination of indicator functions for finitely measurable sets. We use the idiom πΉ β dom β«1 to represent this concept because β«1 is the first preparation function for our final definition β« (see df-itg 25372); unlike that operator, which can integrate any function, this operator can only integrate simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β (πΉ β MblFn β§ (πΉ:ββΆβ β§ ran πΉ β Fin β§ (volβ(β‘πΉ β (β β {0}))) β β))) | ||
Theorem | i1fmbf 25424 | Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ β MblFn) | ||
Theorem | i1ff 25425 | A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ:ββΆβ) | ||
Theorem | i1frn 25426 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β ran πΉ β Fin) | ||
Theorem | i1fima 25427 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β‘πΉ β π΄) β dom vol) | ||
Theorem | i1fima2 25428 | 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 25429 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ π΄ β (π΅ β {0})) β (volβ(β‘πΉ β {π΄})) β β) | ||
Theorem | i1fd 25430* | 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 25431 | 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 25432* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) = Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) | ||
Theorem | itg1val2 25433* | 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 25434 | Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) β β) | ||
Theorem | itg1ge0 25435 | Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ 0π βr β€ πΉ) β 0 β€ (β«1βπΉ)) | ||
Theorem | i1f0 25436 | The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (β Γ {0}) β dom β«1 | ||
Theorem | itg10 25437 | The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (β«1β(β Γ {0})) = 0 | ||
Theorem | i1f1lem 25438* | Lemma for i1f1 25439 and itg11 25440. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, 1, 0)) β β’ (πΉ:ββΆ{0, 1} β§ (π΄ β dom vol β (β‘πΉ β {1}) = π΄)) | ||
Theorem | i1f1 25439* | 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 25440* | 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 25441* | 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 25442* | Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ ((π β§ π΄ β β) β (β‘(πΉ βf + πΊ) β {π΄}) = βͺ π¦ β ran πΊ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦}))) | ||
Theorem | i1fmullem 25443* | Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ ((π β§ π΄ β (β β {0})) β (β‘(πΉ βf Β· πΊ) β {π΄}) = βͺ π¦ β (ran πΊ β {0})((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦}))) | ||
Theorem | i1fadd 25444 | 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 25445 | 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 25446* | Lemma for itg1add 25451. 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 25448 and itg1addlem5 25450. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) β β’ (π β πΌ:(β Γ β)βΆβ) | ||
Theorem | itg1addlem3 25447* | Lemma for itg1add 25451. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) β β’ (((π΄ β β β§ π΅ β β) β§ Β¬ (π΄ = 0 β§ π΅ = 0)) β (π΄πΌπ΅) = (volβ((β‘πΉ β {π΄}) β© (β‘πΊ β {π΅})))) | ||
Theorem | itg1addlem4 25448* | Lemma for itg1add 25451. (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 25449* | Obsolete version of itg1addlem4 25448 as of 6-Oct-2024. (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 25450* | Lemma for itg1add 25451. (Contributed by Mario Carneiro, 27-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) & β’ π = ( + βΎ (ran πΉ Γ ran πΊ)) β β’ (π β (β«1β(πΉ βf + πΊ)) = ((β«1βπΉ) + (β«1βπΊ))) | ||
Theorem | itg1add 25451 | 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 25452 | Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) β β’ (((π β§ π΄ β 0) β§ π΅ β β) β (β‘((β Γ {π΄}) βf Β· πΉ) β {π΅}) = (β‘πΉ β {(π΅ / π΄)})) | ||
Theorem | i1fmulc 25453 | 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 25454 | 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 25455* | 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 25456* | 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 25457* | Deduction form of i1fposd 25457. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ (π β (π₯ β β β¦ π΄) β dom β«1) β β’ (π β (π₯ β β β¦ if(0 β€ π΄, π΄, 0)) β dom β«1) | ||
Theorem | i1fsub 25458 | 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 25459 | 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 25460* | 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 25461* | 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 25462* | Approximate version of itg1le 25463. 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 25463 | 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 25464* | 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 25465* | Lemma for mbfi1fseq 25471. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) β β’ (π β π½:(β Γ β)βΆ(0[,)+β)) | ||
Theorem | mbfi1fseqlem2 25466* | Lemma for mbfi1fseq 25471. (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 25467* | Lemma for mbfi1fseq 25471. (Contributed by Mario Carneiro, 16-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ π½ = (π β β, π¦ β β β¦ ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) & β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) β β’ ((π β§ π΄ β β) β (πΊβπ΄):ββΆran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) | ||
Theorem | mbfi1fseqlem4 25468* | Lemma for mbfi1fseq 25471. 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 25469* | Lemma for mbfi1fseq 25471. 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 25470* | Lemma for mbfi1fseq 25471. 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 25471* | 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 25472* | Lemma for mbfi1flim 25473. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆβ) β β’ (π β βπ(π:ββΆdom β«1 β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) | ||
Theorem | mbfi1flim 25473* | 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 25474* | Lemma for mbfmul 25476. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) & β’ (π β π:ββΆdom β«1) & β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) & β’ (π β π:ββΆdom β«1) & β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯)) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | mbfmullem 25475 | Lemma for mbfmul 25476. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | mbfmul 25476 | The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf Β· πΊ) β MblFn) | ||
Theorem | itg2lcl 25477* | The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ πΏ β β* | ||
Theorem | itg2val 25478* | Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) = sup(πΏ, β*, < )) | ||
Theorem | itg2l 25479* | 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 25480* | Sufficient condition for elementhood in the set πΏ. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(π βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ ((πΊ β dom β«1 β§ πΊ βr β€ πΉ) β (β«1βπΊ) β πΏ) | ||
Theorem | xrge0f 25481 | 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 25482 | The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) β β*) | ||
Theorem | itg2ub 25483 | 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 25484* | 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 25485 | 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 25486 | 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 25487 | The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (β«2β(β Γ {0})) = 0 | ||
Theorem | itg2lecl 25488 | If an β«2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ ((πΉ:ββΆ(0[,]+β) β§ π΄ β β β§ (β«2βπΉ) β€ π΄) β (β«2βπΉ) β β) | ||
Theorem | itg2le 25489 | 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 25490* | 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 25491* | 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 25492* | 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 25505, 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 25493* | Approximate version of itg2ub 25483. If πΉ approximately dominates πΊ, then β«1πΊ β€ β«2πΉ. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,]+β)) & β’ (π β πΊ β dom β«1) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΊβπ₯) β€ (πΉβπ₯)) β β’ (π β (β«1βπΊ) β€ (β«2βπΉ)) | ||
Theorem | itg2lea 25494* | Approximate version of itg2le 25489. If πΉ β€ πΊ for almost all π₯, then β«2πΉ β€ β«2πΊ. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β πΉ:ββΆ(0[,]+β)) & β’ (π β πΊ:ββΆ(0[,]+β)) & β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (β«2βπΉ) β€ (β«2βπΊ)) | ||
Theorem | itg2eqa 25495* | 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 25496 | Lemma for itg2mulc 25497. (Contributed by Mario Carneiro, 8-Jul-2014.) |
β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β π΄ β β+) β β’ (π β (β«2β((β Γ {π΄}) βf Β· πΉ)) β€ (π΄ Β· (β«2βπΉ))) | ||
Theorem | itg2mulc 25497 | 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 25498* | Lemma for itg2split 25499. (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 25499* | The β«2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25509, 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 25500* | Lemma for itg2mono 25503. 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 25503. 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 25464. 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βπ»)) β€ π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |