Home | Metamath
Proof Explorer Theorem List (p. 250 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | citg1 24901 | Extend class notation with the Lebesgue integral for simple functions. |
class β«1 | ||
Syntax | citg2 24902 | Extend class notation with the Lebesgue integral for nonnegative functions. |
class β«2 | ||
Syntax | cibl 24903 | Extend class notation with the class of integrable functions. |
class πΏ1 | ||
Syntax | citg 24904 | Extend class notation with the general Lebesgue integral. |
class β«π΄π΅ dπ₯ | ||
Definition | df-mbf 24905* | 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 24812) 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 24906* | 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 24907* | 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 24908* | 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 24909* | 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 24907 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 24907 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ β«π΄π΅ dπ₯ = Ξ£π β (0...3)((iβπ) Β· (β«2β(π₯ β β β¦ β¦(ββ(π΅ / (iβπ))) / π¦β¦if((π₯ β π΄ β§ 0 β€ π¦), π¦, 0)))) | ||
Theorem | ismbf1 24910* | The predicate "πΉ is a measurable function". This is more naturally stated for functions on the reals, see ismbf 24914 and ismbfcn 24915 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 24911 | A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) | ||
Theorem | mbfdm 24912 | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ β MblFn β dom πΉ β dom vol) | ||
Theorem | mbfconstlem 24913 | Lemma for mbfconst 24919 and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ ((π΄ β dom vol β§ πΆ β β) β (β‘(π΄ Γ {πΆ}) β π΅) β dom vol) | ||
Theorem | ismbf 24914* | 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 24812. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol)) | ||
Theorem | ismbfcn 24915 | 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 24916 | 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 24917 | The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (((πΉ β MblFn β§ πΉ:π΄βΆβ) β§ (π΅ β β β§ πΆ β β)) β (β‘πΉ β (π΅[,]πΆ)) β dom vol) | ||
Theorem | mbfimasn 24918 | The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ β§ π΅ β β) β (β‘πΉ β {π΅}) β dom vol) | ||
Theorem | mbfconst 24919 | A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ ((π΄ β dom vol β§ π΅ β β) β (π΄ Γ {π΅}) β MblFn) | ||
Theorem | mbf0 24920 | The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.) |
β’ β β MblFn | ||
Theorem | mbfid 24921 | The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (π΄ β dom vol β ( I βΎ π΄) β MblFn) | ||
Theorem | mbfmptcl 24922* | Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | mbfdm2 24923* | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.) |
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ (π β π΄ β dom vol) | ||
Theorem | ismbfcn2 24924* | 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 24925* | 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 24940. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ ((π β§ π₯ β β*) β (β‘πΉ β (π₯(,)+β)) β dom vol) & β’ ((π β§ π₯ β β*) β (β‘πΉ β (-β(,)π₯)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | ismbf2d 24926* | Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β dom vol) & β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom vol) & β’ ((π β§ π₯ β β) β (β‘πΉ β (-β(,)π₯)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfeqalem1 24927* | Lemma for mbfeqalem2 24928. (Contributed by Mario Carneiro, 2-Sep-2014.) (Revised by AV, 19-Aug-2022.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) & β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) β β’ (π β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β dom vol) | ||
Theorem | mbfeqalem2 24928* | Lemma for mbfeqa 24929. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by AV, 19-Aug-2022.) |
β’ (π β π΄ β β) & β’ (π β (vol*βπ΄) = 0) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) & β’ ((π β§ π₯ β π΅) β πΆ β β) & β’ ((π β§ π₯ β π΅) β π· β β) β β’ (π β ((π₯ β π΅ β¦ πΆ) β MblFn β (π₯ β π΅ β¦ π·) β MblFn)) | ||
Theorem | mbfeqa 24929* | 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 24930 | The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ ((πΉ β MblFn β§ π΄ β dom vol) β (πΉ βΎ π΄) β MblFn) | ||
Theorem | mbfres2 24931 | 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 24932* | Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β dom vol) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = 0) & β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) β β’ (π β (π₯ β π΅ β¦ πΆ) β MblFn) | ||
Theorem | mbfmulc2lem 24933 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β π΅ β β) & β’ (π β πΉ:π΄βΆβ) β β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) | ||
Theorem | mbfmulc2re 24934 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β π΅ β β) & β’ (π β πΉ:π΄βΆβ) β β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) | ||
Theorem | mbfmax 24935* | The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β MblFn) & β’ (π β πΊ:π΄βΆβ) & β’ (π β πΊ β MblFn) & β’ π» = (π₯ β π΄ β¦ if((πΉβπ₯) β€ (πΊβπ₯), (πΊβπ₯), (πΉβπ₯))) β β’ (π β π» β MblFn) | ||
Theorem | mbfneg 24936* | The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ -π΅) β MblFn) | ||
Theorem | mbfpos 24937* | The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) | ||
Theorem | mbfposr 24938* | Converse to mbfpos 24937. (Contributed by Mario Carneiro, 11-Aug-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) & β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) β β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) | ||
Theorem | mbfposb 24939* | 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 24940* | Simplified form of ismbfd 24925. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom vol) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfimaopnlem 24941* | Lemma for mbfimaopn 24942. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ π½ = (TopOpenββfld) & β’ πΊ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π΅ = ((,) β (β Γ β)) & β’ πΎ = ran (π₯ β π΅, π¦ β π΅ β¦ (π₯ Γ π¦)) β β’ ((πΉ β MblFn β§ π΄ β π½) β (β‘πΉ β π΄) β dom vol) | ||
Theorem | mbfimaopn 24942 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 24944, 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 24943 | 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 24944 | 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 24945 | 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 24946 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) & β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfadd 24947 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf + πΊ) β MblFn) | ||
Theorem | mbfsub 24948 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ (π β πΉ β MblFn) & β’ (π β πΊ β MblFn) β β’ (π β (πΉ βf β πΊ) β MblFn) | ||
Theorem | mbfmulc2 24949* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) | ||
Theorem | mbfsup 24950* | 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 24951* | 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 24952* | 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 24953* | The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β β) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Theorem | mbflim 24954* | The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π₯ β π΄) β (π β π β¦ π΅) β πΆ) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ (π β π β§ π₯ β π΄)) β π΅ β π) β β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) | ||
Syntax | c0p 24955 | Extend class notation to include the zero polynomial. |
class 0π | ||
Definition | df-0p 24956 | Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ 0π = (β Γ {0}) | ||
Theorem | 0pval 24957 | The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β (0πβπ΄) = 0) | ||
Theorem | 0plef 24958 | Two ways to say that the function πΉ on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.) |
β’ (πΉ:ββΆ(0[,)+β) β (πΉ:ββΆβ β§ 0π βr β€ πΉ)) | ||
Theorem | 0pledm 24959 | 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 24960 | 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 24909); 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 24961 | Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ β MblFn) | ||
Theorem | i1ff 24962 | A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β πΉ:ββΆβ) | ||
Theorem | i1frn 24963 | A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β ran πΉ β Fin) | ||
Theorem | i1fima 24964 | Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β‘πΉ β π΄) β dom vol) | ||
Theorem | i1fima2 24965 | 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 24966 | Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ π΄ β (π΅ β {0})) β (volβ(β‘πΉ β {π΄})) β β) | ||
Theorem | i1fd 24967* | 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 24968 | 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 24969* | The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) = Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) | ||
Theorem | itg1val2 24970* | 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 24971 | Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (πΉ β dom β«1 β (β«1βπΉ) β β) | ||
Theorem | itg1ge0 24972 | Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ ((πΉ β dom β«1 β§ 0π βr β€ πΉ) β 0 β€ (β«1βπΉ)) | ||
Theorem | i1f0 24973 | The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (β Γ {0}) β dom β«1 | ||
Theorem | itg10 24974 | The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (β«1β(β Γ {0})) = 0 | ||
Theorem | i1f1lem 24975* | Lemma for i1f1 24976 and itg11 24977. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ πΉ = (π₯ β β β¦ if(π₯ β π΄, 1, 0)) β β’ (πΉ:ββΆ{0, 1} β§ (π΄ β dom vol β (β‘πΉ β {1}) = π΄)) | ||
Theorem | i1f1 24976* | 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 24977* | 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 24978* | 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 24979* | Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ ((π β§ π΄ β β) β (β‘(πΉ βf + πΊ) β {π΄}) = βͺ π¦ β ran πΊ((β‘πΉ β {(π΄ β π¦)}) β© (β‘πΊ β {π¦}))) | ||
Theorem | i1fmullem 24980* | Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) β β’ ((π β§ π΄ β (β β {0})) β (β‘(πΉ βf Β· πΊ) β {π΄}) = βͺ π¦ β (ran πΊ β {0})((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦}))) | ||
Theorem | i1fadd 24981 | 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 24982 | 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 24983* | Lemma for itg1add 24988. 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 24985 and itg1addlem5 24987. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) β β’ (π β πΌ:(β Γ β)βΆβ) | ||
Theorem | itg1addlem3 24984* | Lemma for itg1add 24988. (Contributed by Mario Carneiro, 26-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) β β’ (((π΄ β β β§ π΅ β β) β§ Β¬ (π΄ = 0 β§ π΅ = 0)) β (π΄πΌπ΅) = (volβ((β‘πΉ β {π΄}) β© (β‘πΊ β {π΅})))) | ||
Theorem | itg1addlem4 24985* | Lemma for itg1add 24988. (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 24986* | Obsolete version of itg1addlem4 24985. (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 24987* | Lemma for itg1add 24988. (Contributed by Mario Carneiro, 27-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β πΊ β dom β«1) & β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) & β’ π = ( + βΎ (ran πΉ Γ ran πΊ)) β β’ (π β (β«1β(πΉ βf + πΊ)) = ((β«1βπΉ) + (β«1βπΊ))) | ||
Theorem | itg1add 24988 | 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 24989 | Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.) |
β’ (π β πΉ β dom β«1) & β’ (π β π΄ β β) β β’ (((π β§ π΄ β 0) β§ π΅ β β) β (β‘((β Γ {π΄}) βf Β· πΉ) β {π΅}) = (β‘πΉ β {(π΅ / π΄)})) | ||
Theorem | i1fmulc 24990 | 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 24991 | 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 24992* | 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 24993* | 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 24994* | Deduction form of i1fposd 24994. (Contributed by Mario Carneiro, 6-Aug-2014.) |
β’ (π β (π₯ β β β¦ π΄) β dom β«1) β β’ (π β (π₯ β β β¦ if(0 β€ π΄, π΄, 0)) β dom β«1) | ||
Theorem | i1fsub 24995 | 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 24996 | 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 24997* | 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 24998* | 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 24999* | Approximate version of itg1le 25000. 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 25000 | 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βπΊ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |