![]() |
Metamath
Proof Explorer Theorem List (p. 252 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uniioombllem3 25101* | Lemma for uniioombl 25105. (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 25102* | Lemma for uniioombl 25105. (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 25103* | Lemma for uniioombl 25105. (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 25104* | Lemma for uniioombl 25105. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) & β’ π΄ = βͺ ran ((,) β πΉ) & β’ (π β (vol*βπΈ) β β) & β’ (π β πΆ β β+) & β’ (π β πΊ:ββΆ( β€ β© (β Γ β))) & β’ (π β πΈ β βͺ ran ((,) β πΊ)) & β’ π = seq1( + , ((abs β β ) β πΊ)) & β’ (π β sup(ran π, β*, < ) β€ ((vol*βπΈ) + πΆ)) β β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) β€ ((vol*βπΈ) + (4 Β· πΆ))) | ||
Theorem | uniioombl 25105* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25069.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ((,) β πΉ) β dom vol) | ||
Theorem | uniiccmbl 25106* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25069.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
β’ (π β πΉ:ββΆ( β€ β© (β Γ β))) & β’ (π β Disj π₯ β β ((,)β(πΉβπ₯))) & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ (π β βͺ ran ([,] β πΉ) β dom vol) | ||
Theorem | dyadf 25107* | 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 25108* | Value of the dyadic rational function πΉ. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (π΄πΉπ΅) = β¨(π΄ / (2βπ΅)), ((π΄ + 1) / (2βπ΅))β©) | ||
Theorem | dyadovol 25109* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((π΄ β β€ β§ π΅ β β0) β (vol*β([,]β(π΄πΉπ΅))) = (1 / (2βπ΅))) | ||
Theorem | dyadss 25110* | 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 25111* | Lemma for dyaddisj 25112. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ ((((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β0 β§ π· β β0)) β§ πΆ β€ π·) β (([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·)) β¨ ([,]β(π΅πΉπ·)) β ([,]β(π΄πΉπΆ)) β¨ (((,)β(π΄πΉπΆ)) β© ((,)β(π΅πΉπ·))) = β )) | ||
Theorem | dyaddisj 25112* | 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 25113* | Lemma for dyadmax 25114. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β πΆ β β0) & β’ (π β π· β β0) & β’ (π β Β¬ π· < πΆ) & β’ (π β ([,]β(π΄πΉπΆ)) β ([,]β(π΅πΉπ·))) β β’ (π β (π΄ = π΅ β§ πΆ = π·)) | ||
Theorem | dyadmax 25114* | 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 25115* | Lemma for dyadmbl 25116. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) = βͺ ([,] β πΊ)) | ||
Theorem | dyadmbl 25116* | Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) & β’ πΊ = {π§ β π΄ β£ βπ€ β π΄ (([,]βπ§) β ([,]βπ€) β π§ = π€)} & β’ (π β π΄ β ran πΉ) β β’ (π β βͺ ([,] β π΄) β dom vol) | ||
Theorem | opnmbllem 25117* | Lemma for opnmbl 25118. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ πΉ = (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | opnmbl 25118 | All open sets are measurable. This proof, via dyadmbl 25116 and uniioombl 25105, 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 25119 | All open sets are measurable. This alternative proof of opnmbl 25118 is significantly shorter, at the expense of invoking countable choice ax-cc 10429. (This was also the original proof before the current opnmbl 25118 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β (topGenβran (,)) β π΄ β dom vol) | ||
Theorem | subopnmbl 25120 | 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 25121* | 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 25122* | 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 25123* | 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 25124* | Lemma for vitali 25129. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} β β’ βΌ Er (0[,]1) | ||
Theorem | vitalilem2 25125* | Lemma for vitali 25129. (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 25126* | Lemma for vitali 25129. (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 25127* | Lemma for vitali 25129. (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 25128* | Lemma for vitali 25129. (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 25129 | 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 25130 | Extend class notation with the class of measurable functions. |
class MblFn | ||
Syntax | citg1 25131 | Extend class notation with the Lebesgue integral for simple functions. |
class β«1 | ||
Syntax | citg2 25132 | Extend class notation with the Lebesgue integral for nonnegative functions. |
class β«2 | ||
Syntax | cibl 25133 | Extend class notation with the class of integrable functions. |
class πΏ1 | ||
Syntax | citg 25134 | Extend class notation with the general Lebesgue integral. |
class β«π΄π΅ dπ₯ | ||
Definition | df-mbf 25135* | 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 25042) 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 25136* | 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 25137* | 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 25138* | 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 25139* | 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 25137 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 25137 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β«π΄π΅ dπ₯ = Ξ£π β (0...3)((iβπ) Β· (β«2β(π₯ β β β¦ β¦(ββ(π΅ / (iβπ))) / π¦β¦if((π₯ β π΄ β§ 0 β€ π¦), π¦, 0)))) | ||
Theorem | ismbf1 25140* | The predicate "πΉ is a measurable function". This is more naturally stated for functions on the reals, see ismbf 25144 and ismbfcn 25145 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 25141 | A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) | ||
Theorem | mbfdm 25142 | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ β MblFn β dom πΉ β dom vol) | ||
Theorem | mbfconstlem 25143 | Lemma for mbfconst 25149 and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ ((π΄ β dom vol β§ πΆ β β) β (β‘(π΄ Γ {πΆ}) β π΅) β dom vol) | ||
Theorem | ismbf 25144* | 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 25042. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol)) | ||
Theorem | ismbfcn 25145 | 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 25146 | 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 25147 | The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β‘πΉ β (π΅[,]πΆ)) β dom vol) | ||
Theorem | mbfimasn 25148 | The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ β§ π΅ β β) β (β‘πΉ β {π΅}) β dom vol) | ||
Theorem | mbfconst 25149 | A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β) β (π΄ Γ {π΅}) β MblFn) | ||
Theorem | mbf0 25150 | The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.) |
β’ β β MblFn | ||
Theorem | mbfid 25151 | The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (π΄ β dom vol β ( I βΎ π΄) β MblFn) | ||
Theorem | mbfmptcl 25152* | Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | mbfdm2 25153* | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ (π β π΄ β dom vol) | ||
Theorem | ismbfcn2 25154* | 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 25155* | 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 25170. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ ((π β§ π₯ β β*) β (β‘πΉ β (π₯(,)+β)) β dom vol) & β’ ((π β§ π₯ β β*) β (β‘πΉ β (-β(,)π₯)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | ismbf2d 25156* | Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β dom vol) & β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom vol) & β’ ((π β§ π₯ β β) β (β‘πΉ β (-β(,)π₯)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfeqalem1 25157* | Lemma for mbfeqalem2 25158. (Contributed by Mario Carneiro, 2-Sep-2014.) (Revised by AV, 19-Aug-2022.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) & β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) β β’ (π β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β dom vol) | ||
Theorem | mbfeqalem2 25158* | Lemma for mbfeqa 25159. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by AV, 19-Aug-2022.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) & β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) β β’ (π β ((π₯ β π΅ β¦ πΆ) β MblFn β (π₯ β π΅ β¦ π·) β MblFn)) | ||
Theorem | mbfeqa 25159* | 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 25160 | The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (πΉ βΎ π΄) β MblFn) | ||
Theorem | mbfres2 25161 | 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 25162* | Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β dom vol) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = 0) & β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) β β’ (π β (π₯ β π΅ β¦ πΆ) β MblFn) | ||
Theorem | mbfmulc2lem 25163 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β π΅ β β) & β’ (π β πΉ:π΄βΆβ) β β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) | ||
Theorem | mbfmulc2re 25164 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β π΅ β β) & β’ (π β πΉ:π΄βΆβ) β β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) | ||
Theorem | mbfmax 25165* | The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β MblFn) & β’ (π β πΊ:π΄βΆβ) & β’ (π β πΊ β MblFn) & β’ π» = (π₯ β π΄ β¦ if((πΉβπ₯) β€ (πΊβπ₯), (πΊβπ₯), (πΉβπ₯))) β β’ (π β π» β MblFn) | ||
Theorem | mbfneg 25166* | The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ -π΅) β MblFn) | ||
Theorem | mbfpos 25167* | The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) | ||
Theorem | mbfposr 25168* | Converse to mbfpos 25167. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) & β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) β β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) | ||
Theorem | mbfposb 25169* | 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 25170* | Simplified form of ismbfd 25155. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfimaopnlem 25171* | Lemma for mbfimaopn 25172. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ π½ = (TopOpenββfld) & β’ πΊ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π΅ = ((,) β (β Γ β)) & β’ πΎ = ran (π₯ β π΅, π¦ β π΅ β¦ (π₯ Γ π¦)) β β’ ((πΉ β MblFn β§ π΄ β π½) β (β‘πΉ β π΄) β dom vol) | ||
Theorem | mbfimaopn 25172 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 25174, 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 25173 | 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 25174 | 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 25175 | 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 25176 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfadd 25177 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfsub 25178 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf β πΊ) β MblFn) | ||
Theorem | mbfmulc2 25179* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) | ||
Theorem | mbfsup 25180* | 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 25181* | 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 25182* | 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 25183* | The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Theorem | mbflim 25184* | The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β π) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Syntax | c0p 25185 | Extend class notation to include the zero polynomial. |
class 0π | ||
Definition | df-0p 25186 | Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ 0π = (β Γ {0}) | ||
Theorem | 0pval 25187 | The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β (0πβπ΄) = 0) | ||
Theorem | 0plef 25188 | Two ways to say that the function πΉ on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (πΉ:ββΆ(0[,)+β) β (πΉ:ββΆβ β§ 0π βr β€ πΉ)) | ||
Theorem | 0pledm 25189 | 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 25190 | 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 25139); 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 25191 | Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ β MblFn) | ||
Theorem | i1ff 25192 | A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ:ββΆβ) | ||
Theorem | i1frn 25193 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β ran πΉ β Fin) | ||
Theorem | i1fima 25194 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β‘πΉ β π΄) β dom vol) | ||
Theorem | i1fima2 25195 | 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 25196 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ π΄ β (π΅ β {0})) β (volβ(β‘πΉ β {π΄})) β β) | ||
Theorem | i1fd 25197* | 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 25198 | 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 25199* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) = Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) | ||
Theorem | itg1val2 25200* | 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 > |