![]() |
Metamath
Proof Explorer Theorem List (p. 340 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 | sitgclre 33901 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) & β’ (π β π β Ban) & β’ (π β (Scalarβπ) = βfld) β β’ (π β ((πsitgπ)βπΉ) β π΅) | ||
Theorem | sitg0 33902 | The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β π β TopSp) & β’ (π β π β Mnd) β β’ (π β ((πsitgπ)β(βͺ dom π Γ { 0 })) = 0 ) | ||
Theorem | sitgf 33903* | The integral for simple functions is itself a function. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ ((π β§ π β dom (πsitgπ)) β ((πsitgπ)βπ) β π΅) β β’ (π β (πsitgπ):dom (πsitgπ)βΆπ΅) | ||
Theorem | sitgaddlemb 33904 | Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-2019.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β π β TopSp) & β’ (π β (π βΎv (π» β (0[,)+β))) β SLMod) & β’ (π β π½ β Fre) & β’ (π β πΉ β dom (πsitgπ)) & β’ (π β πΊ β dom (πsitgπ)) & β’ (π β (Scalarβπ) β βExt ) & β’ + = (+gβπ) β β’ ((π β§ π β ((ran πΉ Γ ran πΊ) β {β¨ 0 , 0 β©})) β ((π»β(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) Β· (2nd βπ)) β π΅) | ||
Theorem | sitmval 33905* | Value of the simple function integral metric for a given space π and measure π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π· = (distβπ) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) β β’ (π β (πsitmπ) = (π β dom (πsitgπ), π β dom (πsitgπ) β¦ (((β*π βΎs (0[,]+β))sitgπ)β(π βf π·π)))) | ||
Theorem | sitmfval 33906 | Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π· = (distβπ) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) & β’ (π β πΊ β dom (πsitgπ)) β β’ (π β (πΉ(πsitmπ)πΊ) = (((β*π βΎs (0[,]+β))sitgπ)β(πΉ βf π·πΊ))) | ||
Theorem | sitmcl 33907 | Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
β’ (π β π β Mnd) & β’ (π β π β βMetSp) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) & β’ (π β πΊ β dom (πsitgπ)) β β’ (π β (πΉ(πsitmπ)πΊ) β (0[,]+β)) | ||
Theorem | sitmf 33908 | The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ (π β π β Mnd) & β’ (π β π β βMetSp) & β’ (π β π β βͺ ran measures) β β’ (π β (πsitmπ):(dom (πsitgπ) Γ dom (πsitgπ))βΆ(0[,]+β)) | ||
Definition | df-itgm 33909* |
Define the Bochner integral as the extension by continuity of the
Bochnel integral for simple functions.
Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric (π€sitmπ). He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 25539. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
β’ itgm = (π€ β V, π β βͺ ran measures β¦ (((metUnifβ(π€sitmπ))CnExt(UnifStβπ€))β(π€sitgπ))) | ||
Theorem | oddpwdc 33910* | Lemma for eulerpart 33938. The function πΉ that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.) |
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) β β’ πΉ:(π½ Γ β0)β1-1-ontoββ | ||
Theorem | oddpwdcv 33911* | Lemma for eulerpart 33938: value of the πΉ function. (Contributed by Thierry Arnoux, 9-Sep-2017.) |
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) β β’ (π β (π½ Γ β0) β (πΉβπ) = ((2β(2nd βπ)) Β· (1st βπ))) | ||
Theorem | eulerpartlemsv1 33912* | Lemma for eulerpart 33938. Value of the sum of a partition π΄. (Contributed by Thierry Arnoux, 26-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (πβπ΄) = Ξ£π β β ((π΄βπ) Β· π)) | ||
Theorem | eulerpartlemelr 33913* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (π΄:ββΆβ0 β§ (β‘π΄ β β) β Fin)) | ||
Theorem | eulerpartlemsv2 33914* | Lemma for eulerpart 33938. Value of the sum of a finite partition π΄ (Contributed by Thierry Arnoux, 19-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (πβπ΄) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) | ||
Theorem | eulerpartlemsf 33915* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ π:((β0 βm β) β© π )βΆβ0 | ||
Theorem | eulerpartlems 33916* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ ((π΄ β ((β0 βm β) β© π ) β§ π‘ β (β€β₯β((πβπ΄) + 1))) β (π΄βπ‘) = 0) | ||
Theorem | eulerpartlemsv3 33917* | Lemma for eulerpart 33938. Value of the sum of a finite partition π΄ (Contributed by Thierry Arnoux, 19-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (πβπ΄) = Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) | ||
Theorem | eulerpartlemgc 33918* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 9-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ ((π΄ β ((β0 βm β) β© π ) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β ((2βπ) Β· π‘) β€ (πβπ΄)) | ||
Theorem | eulerpartleme 33919* | Lemma for eulerpart 33938. (Contributed by Mario Carneiro, 26-Jan-2015.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} β β’ (π΄ β π β (π΄:ββΆβ0 β§ (β‘π΄ β β) β Fin β§ Ξ£π β β ((π΄βπ) Β· π) = π)) | ||
Theorem | eulerpartlemv 33920* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 19-Aug-2018.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} β β’ (π΄ β π β (π΄:ββΆβ0 β§ (β‘π΄ β β) β Fin β§ Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π)) | ||
Theorem | eulerpartlemo 33921* | Lemma for eulerpart 33938: π is the set of odd partitions of π. (Contributed by Thierry Arnoux, 10-Aug-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} β β’ (π΄ β π β (π΄ β π β§ βπ β (β‘π΄ β β) Β¬ 2 β₯ π)) | ||
Theorem | eulerpartlemd 33922* | Lemma for eulerpart 33938: π· is the set of distinct part. of π. (Contributed by Thierry Arnoux, 11-Aug-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} β β’ (π΄ β π· β (π΄ β π β§ (π΄ β β) β {0, 1})) | ||
Theorem | eulerpartlem1 33923* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) β β’ π:π»β1-1-ontoβ(π« (π½ Γ β0) β© Fin) | ||
Theorem | eulerpartlemb 33924* | Lemma for eulerpart 33938. The set of all partitions of π is finite. (Contributed by Mario Carneiro, 26-Jan-2015.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) β β’ π β Fin | ||
Theorem | eulerpartlemt0 33925* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} β β’ (π΄ β (π β© π ) β (π΄ β (β0 βm β) β§ (β‘π΄ β β) β Fin β§ (β‘π΄ β β) β π½)) | ||
Theorem | eulerpartlemf 33926* | Lemma for eulerpart 33938: Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} β β’ ((π΄ β (π β© π ) β§ π‘ β (β β π½)) β (π΄βπ‘) = 0) | ||
Theorem | eulerpartlemt 33927* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} β β’ ((β0 βm π½) β© π ) = ran (π β (π β© π ) β¦ (π βΎ π½)) | ||
Theorem | eulerpartgbij 33928* | Lemma for eulerpart 33938: The πΊ function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) β β’ πΊ:(π β© π )β1-1-ontoβ(({0, 1} βm β) β© π ) | ||
Theorem | eulerpartlemgv 33929* | Lemma for eulerpart 33938: value of the function πΊ. (Contributed by Thierry Arnoux, 13-Nov-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) β β’ (π΄ β (π β© π ) β (πΊβπ΄) = ((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))) | ||
Theorem | eulerpartlemr 33930* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 13-Nov-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) β β’ π = ((π β© π ) β© π) | ||
Theorem | eulerpartlemmf 33931* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 30-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) β β’ (π΄ β (π β© π ) β (bits β (π΄ βΎ π½)) β π») | ||
Theorem | eulerpartlemgvv 33932* | Lemma for eulerpart 33938: value of the function πΊ evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) β β’ ((π΄ β (π β© π ) β§ π΅ β β) β ((πΊβπ΄)βπ΅) = if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π΅, 1, 0)) | ||
Theorem | eulerpartlemgu 33933* | Lemma for eulerpart 33938: Rewriting the π set for an odd partition Note that interestingly, this proof reuses marypha2lem2 9451. (Contributed by Thierry Arnoux, 10-Aug-2018.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) & β’ π = βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β β’ (π΄ β (π β© π ) β π = {β¨π‘, πβ© β£ (π‘ β ((β‘π΄ β β) β© π½) β§ π β ((bits β π΄)βπ‘))}) | ||
Theorem | eulerpartlemgh 33934* | Lemma for eulerpart 33938: The πΉ function is a bijection on the π subsets. (Contributed by Thierry Arnoux, 15-Aug-2018.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) & β’ π = βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β β’ (π΄ β (π β© π ) β (πΉ βΎ π):πβ1-1-ontoβ{π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) | ||
Theorem | eulerpartlemgf 33935* | Lemma for eulerpart 33938: Images under πΊ have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) β β’ (π΄ β (π β© π ) β (β‘(πΊβπ΄) β β) β Fin) | ||
Theorem | eulerpartlemgs2 33936* | Lemma for eulerpart 33938: The πΊ function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β (π β© π ) β (πβ(πΊβπ΄)) = (πβπ΄)) | ||
Theorem | eulerpartlemn 33937* | Lemma for eulerpart 33938. (Contributed by Thierry Arnoux, 30-Aug-2018.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} & β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) & β’ π» = {π β ((π« β0 β© Fin) βm π½) β£ (π supp β ) β Fin} & β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) & β’ π = {π β£ (β‘π β β) β Fin} & β’ π = {π β (β0 βm β) β£ (β‘π β β) β π½} & β’ πΊ = (π β (π β© π ) β¦ ((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (πΊ βΎ π):πβ1-1-ontoβπ· | ||
Theorem | eulerpart 33938* | Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let π be the set of all partitions of π, represented as multisets of positive integers, which is to say functions from β to β0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals π. Then the set π of all partitions that only consist of odd numbers and the set π· of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} β β’ (β―βπ) = (β―βπ·) | ||
Syntax | csseq 33939 | Sequences defined by strong recursion. |
class seqstr | ||
Definition | df-sseq 33940* | Define a builder for sequences by strong recursion, i.e., by computing the value of the n-th element of the sequence from all preceding elements and not just the previous one. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
β’ seqstr = (π β V, π β V β¦ (π βͺ (lastS β seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πβπ₯)ββ©)), (β0 Γ {(π ++ β¨β(πβπ)ββ©)}))))) | ||
Theorem | subiwrd 33941 | Lemma for sseqp1 33951. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β π β V) & β’ (π β πΉ:β0βΆπ) & β’ (π β π β β0) β β’ (π β (πΉ βΎ (0..^π)) β Word π) | ||
Theorem | subiwrdlen 33942 | Length of a subword of an infinite word. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β π β V) & β’ (π β πΉ:β0βΆπ) & β’ (π β π β β0) β β’ (π β (β―β(πΉ βΎ (0..^π))) = π) | ||
Theorem | iwrdsplit 33943 | Lemma for sseqp1 33951. (Contributed by Thierry Arnoux, 25-Apr-2019.) (Proof shortened by AV, 14-Oct-2022.) |
β’ (π β π β V) & β’ (π β πΉ:β0βΆπ) & β’ (π β π β β0) β β’ (π β (πΉ βΎ (0..^(π + 1))) = ((πΉ βΎ (0..^π)) ++ β¨β(πΉβπ)ββ©)) | ||
Theorem | sseqval 33944* | Value of the strong sequence builder function. The set π represents here the words of length greater than or equal to the lenght of the initial sequence π. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) β β’ (π β (πseqstrπΉ) = (π βͺ (lastS β seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0 Γ {(π ++ β¨β(πΉβπ)ββ©)}))))) | ||
Theorem | sseqfv1 33945 | Value of the strong sequence builder function at one of its initial values. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) & β’ (π β π β (0..^(β―βπ))) β β’ (π β ((πseqstrπΉ)βπ) = (πβπ)) | ||
Theorem | sseqfn 33946 | A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) β β’ (π β (πseqstrπΉ) Fn β0) | ||
Theorem | sseqmw 33947 | Lemma for sseqf 33948 amd sseqp1 33951. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) β β’ (π β π β π) | ||
Theorem | sseqf 33948 | A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.) (Proof shortened by AV, 7-Mar-2022.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) β β’ (π β (πseqstrπΉ):β0βΆπ) | ||
Theorem | sseqfres 33949 | The first elements in the strong recursive sequence are the sequence initializer. (Contributed by Thierry Arnoux, 23-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) β β’ (π β ((πseqstrπΉ) βΎ (0..^(β―βπ))) = π) | ||
Theorem | sseqfv2 33950* | Value of the strong sequence builder function. (Contributed by Thierry Arnoux, 21-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) & β’ (π β π β (β€β₯β(β―βπ))) β β’ (π β ((πseqstrπΉ)βπ) = (lastSβ(seq(β―βπ)((π₯ β V, π¦ β V β¦ (π₯ ++ β¨β(πΉβπ₯)ββ©)), (β0 Γ {(π ++ β¨β(πΉβπ)ββ©)}))βπ))) | ||
Theorem | sseqp1 33951 | Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) & β’ (π β π β (β€β₯β(β―βπ))) β β’ (π β ((πseqstrπΉ)βπ) = (πΉβ((πseqstrπΉ) βΎ (0..^π)))) | ||
Syntax | cfib 33952 | The Fibonacci sequence. |
class Fibci | ||
Definition | df-fib 33953 | Define the Fibonacci sequence, where that each element is the sum of the two preceding ones, starting from 0 and 1. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ Fibci = (β¨β01ββ©seqstr(π€ β (Word β0 β© (β‘β― β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) | ||
Theorem | fiblem 33954 | Lemma for fib0 33955, fib1 33956 and fibp1 33957. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π€ β (Word β0 β© (β‘β― β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))):(Word β0 β© (β‘β― β (β€β₯β(β―ββ¨β01ββ©))))βΆβ0 | ||
Theorem | fib0 33955 | Value of the Fibonacci sequence at index 0. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ0) = 0 | ||
Theorem | fib1 33956 | Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ1) = 1 | ||
Theorem | fibp1 33957 | Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β β β (Fibciβ(π + 1)) = ((Fibciβ(π β 1)) + (Fibciβπ))) | ||
Theorem | fib2 33958 | Value of the Fibonacci sequence at index 2. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ2) = 1 | ||
Theorem | fib3 33959 | Value of the Fibonacci sequence at index 3. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ3) = 2 | ||
Theorem | fib4 33960 | Value of the Fibonacci sequence at index 4. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ4) = 3 | ||
Theorem | fib5 33961 | Value of the Fibonacci sequence at index 5. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ5) = 5 | ||
Theorem | fib6 33962 | Value of the Fibonacci sequence at index 6. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ6) = 8 | ||
Syntax | cprb 33963 | Extend class notation to include the class of probability measures. |
class Prob | ||
Definition | df-prob 33964 | Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016.) |
β’ Prob = {π β βͺ ran measures β£ (πββͺ dom π) = 1} | ||
Theorem | elprob 33965 | The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
β’ (π β Prob β (π β βͺ ran measures β§ (πββͺ dom π) = 1)) | ||
Theorem | domprobmeas 33966 | A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ (π β Prob β π β (measuresβdom π)) | ||
Theorem | domprobsiga 33967 | The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ (π β Prob β dom π β βͺ ran sigAlgebra) | ||
Theorem | probtot 33968 | The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
β’ (π β Prob β (πββͺ dom π) = 1) | ||
Theorem | prob01 33969 | A probability is an element of [ 0 , 1 ]. First axiom of Kolmogorov. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π) β (πβπ΄) β (0[,]1)) | ||
Theorem | probnul 33970 | The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β Prob β (πββ ) = 0) | ||
Theorem | unveldomd 33971 | The universe is an element of the domain of the probability, the universe (entire probability space) being βͺ dom π in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
β’ (π β π β Prob) β β’ (π β βͺ dom π β dom π) | ||
Theorem | unveldom 33972 | The universe is an element of the domain of the probability, the universe (entire probability space) being βͺ dom π in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
β’ (π β Prob β βͺ dom π β dom π) | ||
Theorem | nuleldmp 33973 | The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
β’ (π β Prob β β β dom π) | ||
Theorem | probcun 33974* | The probability of the union of a countable disjoint set of events is the sum of their probabilities. (Third axiom of Kolmogorov) Here, the Ξ£ construct cannot be used as it can handle infinite indexing set only if they are subsets of β€, which is not the case here. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β Prob β§ π΄ β π« dom π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯)) β (πββͺ π΄) = Ξ£*π₯ β π΄(πβπ₯)) | ||
Theorem | probun 33975 | The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β ((π΄ β© π΅) = β β (πβ(π΄ βͺ π΅)) = ((πβπ΄) + (πβπ΅)))) | ||
Theorem | probdif 33976 | The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β (πβ(π΄ β π΅)) = ((πβπ΄) β (πβ(π΄ β© π΅)))) | ||
Theorem | probinc 33977 | A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.) |
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ π΄ β π΅) β (πβπ΄) β€ (πβπ΅)) | ||
Theorem | probdsb 33978 | The probability of the complement of a set. That is, the probability that the event π΄ does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π) β (πβ(βͺ dom π β π΄)) = (1 β (πβπ΄))) | ||
Theorem | probmeasd 33979 | A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) β β’ (π β π β βͺ ran measures) | ||
Theorem | probvalrnd 33980 | The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π΄ β dom π) β β’ (π β (πβπ΄) β β) | ||
Theorem | probtotrnd 33981 | The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) β β’ (π β (πββͺ dom π) β β) | ||
Theorem | totprobd 33982* | Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β π β Prob) & β’ (π β π΄ β dom π) & β’ (π β π΅ β π« dom π) & β’ (π β βͺ π΅ = βͺ dom π) & β’ (π β π΅ βΌ Ο) & β’ (π β Disj π β π΅ π) β β’ (π β (πβπ΄) = Ξ£*π β π΅(πβ(π β© π΄))) | ||
Theorem | totprob 33983* | Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π β§ (βͺ π΅ = βͺ dom π β§ π΅ β π« dom π β§ (π΅ βΌ Ο β§ Disj π β π΅ π))) β (πβπ΄) = Ξ£*π β π΅(πβ(π β© π΄))) | ||
Theorem | probfinmeasb 33984 | Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+) β (π βf/c /π (πββͺ π)) β Prob) | ||
Theorem | probfinmeasbALTV 33985* | Alternate version of probfinmeasb 33984. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.) |
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+) β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β Prob) | ||
Theorem | probmeasb 33986* | Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π β§ (πβπ΄) β β+) β (π₯ β π β¦ ((πβ(π₯ β© π΄)) / (πβπ΄))) β Prob) | ||
Syntax | ccprob 33987 | Extends class notation with the conditional probability builder. |
class cprob | ||
Definition | df-cndprob 33988* | Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ cprob = (π β Prob β¦ (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ)))) | ||
Theorem | cndprobval 33989 | The value of the conditional probability , i.e. the probability for the event π΄, given π΅, under the probability law π. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β ((cprobβπ)ββ¨π΄, π΅β©) = ((πβ(π΄ β© π΅)) / (πβπ΅))) | ||
Theorem | cndprobin 33990 | An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (πβπ΅) β 0) β (((cprobβπ)ββ¨π΄, π΅β©) Β· (πβπ΅)) = (πβ(π΄ β© π΅))) | ||
Theorem | cndprob01 33991 | The conditional probability has values in [0, 1]. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (πβπ΅) β 0) β ((cprobβπ)ββ¨π΄, π΅β©) β (0[,]1)) | ||
Theorem | cndprobtot 33992 | The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ ((π β Prob β§ π΄ β dom π β§ (πβπ΄) β 0) β ((cprobβπ)ββ¨βͺ dom π, π΄β©) = 1) | ||
Theorem | cndprobnul 33993 | The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ ((π β Prob β§ π΄ β dom π β§ (πβπ΄) β 0) β ((cprobβπ)ββ¨β , π΄β©) = 0) | ||
Theorem | cndprobprob 33994* | The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ ((π β Prob β§ π΅ β dom π β§ (πβπ΅) β 0) β (π β dom π β¦ ((cprobβπ)ββ¨π, π΅β©)) β Prob) | ||
Theorem | bayesth 33995 | Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (πβπ΄) β 0 β§ (πβπ΅) β 0) β ((cprobβπ)ββ¨π΄, π΅β©) = ((((cprobβπ)ββ¨π΅, π΄β©) Β· (πβπ΄)) / (πβπ΅))) | ||
Syntax | crrv 33996 | Extend class notation with the class of real-valued random variables. |
class rRndVar | ||
Definition | df-rrv 33997 | In its generic definition, a random variable is a measurable function from a probability space to a Borel set. Here, we specifically target real-valued random variables, i.e. measurable function from a probability space to the Borel sigma-algebra on the set of real numbers. (Contributed by Thierry Arnoux, 20-Sep-2016.) (Revised by Thierry Arnoux, 25-Jan-2017.) |
β’ rRndVar = (π β Prob β¦ (dom πMblFnMπ β)) | ||
Theorem | rrvmbfm 33998 | A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) β β’ (π β (π β (rRndVarβπ) β π β (dom πMblFnMπ β))) | ||
Theorem | isrrvv 33999* | Elementhood to the set of real-valued random variables with respect to the probability π. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) β β’ (π β (π β (rRndVarβπ) β (π:βͺ dom πβΆβ β§ βπ¦ β π β (β‘π β π¦) β dom π))) | ||
Theorem | rrvvf 34000 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β π:βͺ dom πβΆβ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |