![]() |
Metamath
Proof Explorer Theorem List (p. 256 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uniioombllem3 25501* | Lemma for uniioombl 25505. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ (π β π β β) & β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) & β’ πΎ = βͺ (((,) β πΊ) β (1...π)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) < (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ))) | ||
Theorem | uniioombllem4 25502* | Lemma for uniioombl 25505. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ (π β π β β) & β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) & β’ πΎ = βͺ (((,) β πΊ) β (1...π)) & β’ (π β π β β) & β’ (π β βπ β (1...π)(absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π)) & β’ πΏ = βͺ (((,) β πΉ) β (1...π)) β β’ (π β (vol*β(πΎ β© π΄)) β€ ((vol*β(πΎ β© πΏ)) + πΆ)) | ||
Theorem | uniioombllem5 25503* | Lemma for uniioombl 25505. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) & β’ (π β π β β) & β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) & β’ πΎ = βͺ (((,) β πΊ) β (1...π)) & β’ (π β π β β) & β’ (π β βπ β (1...π)(absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π)) & β’ πΏ = βͺ (((,) β πΉ) β (1...π)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ ((vol*βπΈ) + (4 Β· πΆ))) | ||
Theorem | uniioombllem6 25504* | Lemma for uniioombl 25505. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ ((vol*βπΈ) + (4 Β· πΆ))) | ||
Theorem | uniioombl 25505* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25469.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ((,) β πΉ) β dom vol) | ||
Theorem | uniiccmbl 25506* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25469.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ([,] β πΉ) β dom vol) | ||
Theorem | dyadf 25507* | The function πΉ returns the endpoints of a dyadic rational covering of the real line. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ πΉ:(β€ Γ β0)βΆ( β€ β© (β Γ β)) | ||
Theorem | dyadval 25508* | Value of the dyadic rational function πΉ. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (π΄πΉπ΅) = β¨(π΄ / (2βπ΅)), ((π΄ + 1) / (2βπ΅))β©) | ||
Theorem | dyadovol 25509* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (vol*β([,]β(π΄πΉπ΅))) = (1 / (2βπ΅))) | ||
Theorem | dyadss 25510* | Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) (Proof shortened by Mario Carneiro, 26-Apr-2016.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β0 β§ π· β β0)) β (([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·)) β π· β€ πΆ)) | ||
Theorem | dyaddisjlem 25511* | Lemma for dyaddisj 25512. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β0 β§ π· β β0)) β§ πΆ β€ π·) β (([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·)) β¨ ([,]β(π΅πΉπ·)) β ([,]β(π΄πΉπΆ)) β¨ (((,)β(π΄πΉπΆ)) β© ((,)β(π΅πΉπ·))) = β )) | ||
Theorem | dyaddisj 25512* | Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β ran πΉ β§ π΅ β ran πΉ) β (([,]βπ΄) β ([,]βπ΅) β¨ ([,]βπ΅) β ([,]βπ΄) β¨ (((,)βπ΄) β© ((,)βπ΅)) = β )) | ||
Theorem | dyadmaxlem 25513* | Lemma for dyadmax 25514. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β0) & β’ (π β π· β β0) & β’ (π β Β¬ π· < πΆ) & β’ (π β ([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·))) β β’ (π β (π΄ = π΅ β§ πΆ = π·)) | ||
Theorem | dyadmax 25514* | Any nonempty set of dyadic rational intervals has a maximal element. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β ran πΉ β§ π΄ β β ) β βπ§ β π΄ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)) | ||
Theorem | dyadmbllem 25515* | Lemma for dyadmbl 25516. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) = βͺ ([,] β πΊ)) | ||
Theorem | dyadmbl 25516* | Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) β dom vol) | ||
Theorem | opnmbllem 25517* | Lemma for opnmbl 25518. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | opnmbl 25518 | All open sets are measurable. This proof, via dyadmbl 25516 and uniioombl 25505, shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | opnmblALT 25519 | All open sets are measurable. This alternative proof of opnmbl 25518 is significantly shorter, at the expense of invoking countable choice ax-cc 10450. (This was also the original proof before the current opnmbl 25518 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | subopnmbl 25520 | Sets which are open in a measurable subspace are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ π½ = ((topGenβran (,)) βΎt π΄) β β’ ((π΄ β dom vol β§ π΅ β π½) β π΅ β dom vol) | ||
Theorem | volsup2 25521* | The volume of π΄ is the supremum of the sequence vol*β(π΄ β© (-π[,]π)) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β β§ π΅ < (volβπ΄)) β βπ β β π΅ < (volβ(π΄ β© (-π[,]π)))) | ||
Theorem | volcn 25522* | The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ πΉ = (π₯ β β β¦ (volβ(π΄ β© (π΅[,]π₯)))) β β’ ((π΄ β dom vol β§ π΅ β β) β πΉ β (ββcnββ)) | ||
Theorem | volivth 25523* | The Intermediate Value Theorem for the Lebesgue volume function. For any positive π΅ β€ (volβπ΄), there is a measurable subset of π΄ whose volume is π΅. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ ((π΄ β dom vol β§ π΅ β (0[,](volβπ΄))) β βπ₯ β dom vol(π₯ β π΄ β§ (volβπ₯) = π΅)) | ||
Theorem | vitalilem1 25524* | Lemma for vitali 25529. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} β β’ βΌ Er (0[,]1) | ||
Theorem | vitalilem2 25525* | Lemma for vitali 25529. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ (π β (ran πΉ β (0[,]1) β§ (0[,]1) β βͺ π β β (πβπ) β§ βͺ π β β (πβπ) β (-1[,]2))) | ||
Theorem | vitalilem3 25526* | Lemma for vitali 25529. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ (π β Disj π β β (πβπ)) | ||
Theorem | vitalilem4 25527* | Lemma for vitali 25529. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ ((π β§ π β β) β (vol*β(πβπ)) = 0) | ||
Theorem | vitalilem5 25528* | Lemma for vitali 25529. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} & β’ π = ((0[,]1) / βΌ ) & β’ (π β πΉ Fn π) & β’ (π β βπ§ β π (π§ β β β (πΉβπ§) β π§)) & β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) & β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) & β’ (π β Β¬ ran πΉ β (π« β β dom vol)) β β’ Β¬ π | ||
Theorem | vitali 25529 | If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ( < We β β dom vol β π« β) | ||
Syntax | cmbf 25530 | Extend class notation with the class of measurable functions. |
class MblFn | ||
Syntax | citg1 25531 | Extend class notation with the Lebesgue integral for simple functions. |
class β«1 | ||
Syntax | citg2 25532 | Extend class notation with the Lebesgue integral for nonnegative functions. |
class β«2 | ||
Syntax | cibl 25533 | Extend class notation with the class of integrable functions. |
class πΏ1 | ||
Syntax | citg 25534 | Extend class notation with the general Lebesgue integral. |
class β«π΄π΅ dπ₯ | ||
Definition | df-mbf 25535* | Define the class of measurable functions on the reals. A real function is measurable if the preimage of every open interval is a measurable set (see ismbl 25442) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ MblFn = {π β (β βpm β) β£ βπ₯ β ran (,)((β‘(β β π) β π₯) β dom vol β§ (β‘(β β π) β π₯) β dom vol)} | ||
Definition | df-itg1 25536* | Define the Lebesgue integral for simple functions. A simple function is a finite linear combination of indicator functions for finitely measurable sets, whose assigned value is the sum of the measures of the sets times their respective weights. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ β«1 = (π β {π β MblFn β£ (π:ββΆβ β§ ran π β Fin β§ (volβ(β‘π β (β β {0}))) β β)} β¦ Ξ£π₯ β (ran π β {0})(π₯ Β· (volβ(β‘π β {π₯})))) | ||
Definition | df-itg2 25537* | Define the Lebesgue integral for nonnegative functions. A nonnegative function's integral is the supremum of the integrals of all simple functions that are less than the input function. Note that this may be +β for functions that take the value +β on a set of positive measure or functions that are bounded below by a positive number on a set of infinite measure. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β«2 = (π β ((0[,]+β) βm β) β¦ sup({π₯ β£ βπ β dom β«1(π βr β€ π β§ π₯ = (β«1βπ))}, β*, < )) | ||
Definition | df-ibl 25538* | Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ πΏ1 = {π β MblFn β£ βπ β (0...3)(β«2β(π₯ β β β¦ β¦(ββ((πβπ₯) / (iβπ))) / π¦β¦if((π₯ β dom π β§ 0 β€ π¦), π¦, 0))) β β} | ||
Definition | df-itg 25539* | Define the full Lebesgue integral, for complex-valued functions to β. The syntax is designed to be suggestive of the standard notation for integrals. For example, our notation for the integral of π₯β2 from 0 to 1 is β«(0[,]1)(π₯β2) dπ₯ = (1 / 3). The only real function of this definition is to break the integral up into nonnegative real parts and send it off to df-itg2 25537 for further processing. Note that this definition cannot handle integrals which evaluate to infinity, because addition and multiplication are not currently defined on extended reals. (You can use df-itg2 25537 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β«π΄π΅ dπ₯ = Ξ£π β (0...3)((iβπ) Β· (β«2β(π₯ β β β¦ β¦(ββ(π΅ / (iβπ))) / π¦β¦if((π₯ β π΄ β§ 0 β€ π¦), π¦, 0)))) | ||
Theorem | ismbf1 25540* | The predicate "πΉ is a measurable function". This is more naturally stated for functions on the reals, see ismbf 25544 and ismbfcn 25545 for the decomposition of the real and imaginary parts. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ β MblFn β (πΉ β (β βpm β) β§ βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) | ||
Theorem | mbff 25541 | A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) | ||
Theorem | mbfdm 25542 | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ β MblFn β dom πΉ β dom vol) | ||
Theorem | mbfconstlem 25543 | Lemma for mbfconst 25549 and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ ((π΄ β dom vol β§ πΆ β β) β (β‘(π΄ Γ {πΆ}) β π΅) β dom vol) | ||
Theorem | ismbf 25544* | The predicate "πΉ is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl 25442. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol)) | ||
Theorem | ismbfcn 25545 | A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β ((β β πΉ) β MblFn β§ (β β πΉ) β MblFn))) | ||
Theorem | mbfima 25546 | Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (π΅(,)πΆ)) β dom vol) | ||
Theorem | mbfimaicc 25547 | The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β‘πΉ β (π΅[,]πΆ)) β dom vol) | ||
Theorem | mbfimasn 25548 | The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ β§ π΅ β β) β (β‘πΉ β {π΅}) β dom vol) | ||
Theorem | mbfconst 25549 | A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β) β (π΄ Γ {π΅}) β MblFn) | ||
Theorem | mbf0 25550 | The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.) |
β’ β β MblFn | ||
Theorem | mbfid 25551 | The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (π΄ β dom vol β ( I βΎ π΄) β MblFn) | ||
Theorem | mbfmptcl 25552* | Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | mbfdm2 25553* | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ (π β π΄ β dom vol) | ||
Theorem | ismbfcn2 25554* | A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 13-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β MblFn β ((π₯ β π΄ β¦ (ββπ΅)) β MblFn β§ (π₯ β π΄ β¦ (ββπ΅)) β MblFn))) | ||
Theorem | ismbfd 25555* | Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d 25570. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ ((π β§ π₯ β β*) β (β‘πΉ β (π₯(,)+β)) β dom vol) & β’ ((π β§ π₯ β β*) β (β‘πΉ β (-β(,)π₯)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | ismbf2d 25556* | Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β dom vol) & β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom vol) & β’ ((π β§ π₯ β β) β (β‘πΉ β (-β(,)π₯)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfeqalem1 25557* | Lemma for mbfeqalem2 25558. (Contributed by Mario Carneiro, 2-Sep-2014.) (Revised by AV, 19-Aug-2022.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) & β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) β β’ (π β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β dom vol) | ||
Theorem | mbfeqalem2 25558* | Lemma for mbfeqa 25559. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by AV, 19-Aug-2022.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) & β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) β β’ (π β ((π₯ β π΅ β¦ πΆ) β MblFn β (π₯ β π΅ β¦ π·) β MblFn)) | ||
Theorem | mbfeqa 25559* | If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 2-Sep-2014.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) & β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) β β’ (π β ((π₯ β π΅ β¦ πΆ) β MblFn β (π₯ β π΅ β¦ π·) β MblFn)) | ||
Theorem | mbfres 25560 | The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (πΉ βΎ π΄) β MblFn) | ||
Theorem | mbfres2 25561 | Measurability of a piecewise function: if πΉ is measurable on subsets π΅ and πΆ of its domain, and these pieces make up all of π΄, then πΉ is measurable on the whole domain. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β (πΉ βΎ π΅) β MblFn) & β’ (π β (πΉ βΎ πΆ) β MblFn) & β’ (π β (π΅ βͺ πΆ) = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfss 25562* | Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β dom vol) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = 0) & β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) β β’ (π β (π₯ β π΅ β¦ πΆ) β MblFn) | ||
Theorem | mbfmulc2lem 25563 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β π΅ β β) & β’ (π β πΉ:π΄βΆβ) β β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) | ||
Theorem | mbfmulc2re 25564 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β π΅ β β) & β’ (π β πΉ:π΄βΆβ) β β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) | ||
Theorem | mbfmax 25565* | The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β MblFn) & β’ (π β πΊ:π΄βΆβ) & β’ (π β πΊ β MblFn) & β’ π» = (π₯ β π΄ β¦ if((πΉβπ₯) β€ (πΊβπ₯), (πΊβπ₯), (πΉβπ₯))) β β’ (π β π» β MblFn) | ||
Theorem | mbfneg 25566* | The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ -π΅) β MblFn) | ||
Theorem | mbfpos 25567* | The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) | ||
Theorem | mbfposr 25568* | Converse to mbfpos 25567. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) & β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) β β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) | ||
Theorem | mbfposb 25569* | 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 25570* | Simplified form of ismbfd 25555. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfimaopnlem 25571* | Lemma for mbfimaopn 25572. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ π½ = (TopOpenββfld) & β’ πΊ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π΅ = ((,) β (β Γ β)) & β’ πΎ = ran (π₯ β π΅, π¦ β π΅ β¦ (π₯ Γ π¦)) β β’ ((πΉ β MblFn β§ π΄ β π½) β (β‘πΉ β π΄) β dom vol) | ||
Theorem | mbfimaopn 25572 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 25574, 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 25573 | 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 25574 | 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 25575 | 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 25576 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfadd 25577 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfsub 25578 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf β πΊ) β MblFn) | ||
Theorem | mbfmulc2 25579* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) | ||
Theorem | mbfsup 25580* | 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 25581* | 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 25582* | 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 25583* | The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Theorem | mbflim 25584* | The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β π) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Syntax | c0p 25585 | Extend class notation to include the zero polynomial. |
class 0π | ||
Definition | df-0p 25586 | Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ 0π = (β Γ {0}) | ||
Theorem | 0pval 25587 | The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β (0πβπ΄) = 0) | ||
Theorem | 0plef 25588 | Two ways to say that the function πΉ on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (πΉ:ββΆ(0[,)+β) β (πΉ:ββΆβ β§ 0π βr β€ πΉ)) | ||
Theorem | 0pledm 25589 | 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 25590 | 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 25539); 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 25591 | Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ β MblFn) | ||
Theorem | i1ff 25592 | A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ:ββΆβ) | ||
Theorem | i1frn 25593 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β ran πΉ β Fin) | ||
Theorem | i1fima 25594 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β‘πΉ β π΄) β dom vol) | ||
Theorem | i1fima2 25595 | 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 25596 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ π΄ β (π΅ β {0})) β (volβ(β‘πΉ β {π΄})) β β) | ||
Theorem | i1fd 25597* | 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 25598 | 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 25599* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) = Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) | ||
Theorem | itg1val2 25600* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ (π΄ β Fin β§ (ran πΉ β {0}) β π΄ β§ π΄ β (β β {0}))) β (β«1βπΉ) = Ξ£π₯ β π΄ (π₯ Β· (volβ(β‘πΉ β {π₯})))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |