Home | Metamath
Proof Explorer Theorem List (p. 328 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sibfof 32701 | Applying function operations on simple functions results in simple functions with regard to the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) & β’ πΆ = (BaseβπΎ) & β’ (π β π β TopSp) & β’ (π β + :(π΅ Γ π΅)βΆπΆ) & β’ (π β πΊ β dom (πsitgπ)) & β’ (π β πΎ β TopSp) & β’ (π β π½ β Fre) & β’ (π β ( 0 + 0 ) = (0gβπΎ)) β β’ (π β (πΉ βf + πΊ) β dom (πΎsitgπ)) | ||
Theorem | sitgfval 32702* | Value of the Bochner integral for a simple function πΉ. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) β β’ (π β ((πsitgπ)βπΉ) = (π Ξ£g (π₯ β (ran πΉ β { 0 }) β¦ ((π»β(πβ(β‘πΉ β {π₯}))) Β· π₯)))) | ||
Theorem | sitgclg 32703* | Closure of the Bochner integral on simple functions, generic version. See sitgclbn 32704 for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018.) (Proof shortened by AV, 12-Dec-2019.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) & β’ πΊ = (Scalarβπ) & β’ π· = ((distβπΊ) βΎ ((BaseβπΊ) Γ (BaseβπΊ))) & β’ (π β π β TopSp) & β’ (π β π β CMnd) & β’ (π β (Scalarβπ) β βExt ) & β’ ((π β§ π β (π» β (0[,)+β)) β§ π₯ β π΅) β (π Β· π₯) β π΅) β β’ (π β ((πsitgπ)βπΉ) β π΅) | ||
Theorem | sitgclbn 32704 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces, with additional conditions on its scalar field. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) & β’ (π β π β Ban) & β’ (π β (Scalarβπ) β βExt ) β β’ (π β ((πsitgπ)βπΉ) β π΅) | ||
Theorem | sitgclcn 32705 | Closure of the Bochner integral on a simple function. This version is specific to Banach spaces on the complex numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (sigaGenβπ½) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ π» = (βHomβ(Scalarβπ)) & β’ (π β π β π) & β’ (π β π β βͺ ran measures) & β’ (π β πΉ β dom (πsitgπ)) & β’ (π β π β Ban) & β’ (π β (Scalarβπ) = βfld) β β’ (π β ((πsitgπ)βπΉ) β π΅) | ||
Theorem | sitgclre 32706 | 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 32707 | 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 32708* | 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 32709 | 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 32710* | 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 32711 | 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 32712 | 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 32713 | 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 32714* |
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 24909. (Contributed by Thierry Arnoux, 13-Feb-2018.) |
β’ itgm = (π€ β V, π β βͺ ran measures β¦ (((metUnifβ(π€sitmπ))CnExt(UnifStβπ€))β(π€sitgπ))) | ||
Theorem | oddpwdc 32715* | Lemma for eulerpart 32743. 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 32716* | Lemma for eulerpart 32743: value of the πΉ function. (Contributed by Thierry Arnoux, 9-Sep-2017.) |
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} & β’ πΉ = (π₯ β π½, π¦ β β0 β¦ ((2βπ¦) Β· π₯)) β β’ (π β (π½ Γ β0) β (πΉβπ) = ((2β(2nd βπ)) Β· (1st βπ))) | ||
Theorem | eulerpartlemsv1 32717* | Lemma for eulerpart 32743. Value of the sum of a partition π΄. (Contributed by Thierry Arnoux, 26-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (πβπ΄) = Ξ£π β β ((π΄βπ) Β· π)) | ||
Theorem | eulerpartlemelr 32718* | Lemma for eulerpart 32743. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (π΄:ββΆβ0 β§ (β‘π΄ β β) β Fin)) | ||
Theorem | eulerpartlemsv2 32719* | Lemma for eulerpart 32743. Value of the sum of a finite partition π΄ (Contributed by Thierry Arnoux, 19-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (πβπ΄) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) | ||
Theorem | eulerpartlemsf 32720* | Lemma for eulerpart 32743. (Contributed by Thierry Arnoux, 8-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ π:((β0 βm β) β© π )βΆβ0 | ||
Theorem | eulerpartlems 32721* | Lemma for eulerpart 32743. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ ((π΄ β ((β0 βm β) β© π ) β§ π‘ β (β€β₯β((πβπ΄) + 1))) β (π΄βπ‘) = 0) | ||
Theorem | eulerpartlemsv3 32722* | Lemma for eulerpart 32743. Value of the sum of a finite partition π΄ (Contributed by Thierry Arnoux, 19-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ (π΄ β ((β0 βm β) β© π ) β (πβπ΄) = Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) | ||
Theorem | eulerpartlemgc 32723* | Lemma for eulerpart 32743. (Contributed by Thierry Arnoux, 9-Aug-2018.) |
β’ π = {π β£ (β‘π β β) β Fin} & β’ π = (π β ((β0 βm β) β© π ) β¦ Ξ£π β β ((πβπ) Β· π)) β β’ ((π΄ β ((β0 βm β) β© π ) β§ (π‘ β β β§ π β (bitsβ(π΄βπ‘)))) β ((2βπ) Β· π‘) β€ (πβπ΄)) | ||
Theorem | eulerpartleme 32724* | Lemma for eulerpart 32743. (Contributed by Mario Carneiro, 26-Jan-2015.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} β β’ (π΄ β π β (π΄:ββΆβ0 β§ (β‘π΄ β β) β Fin β§ Ξ£π β β ((π΄βπ) Β· π) = π)) | ||
Theorem | eulerpartlemv 32725* | Lemma for eulerpart 32743. (Contributed by Thierry Arnoux, 19-Aug-2018.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} β β’ (π΄ β π β (π΄:ββΆβ0 β§ (β‘π΄ β β) β Fin β§ Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π)) | ||
Theorem | eulerpartlemo 32726* | Lemma for eulerpart 32743: π is the set of odd partitions of π. (Contributed by Thierry Arnoux, 10-Aug-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} β β’ (π΄ β π β (π΄ β π β§ βπ β (β‘π΄ β β) Β¬ 2 β₯ π)) | ||
Theorem | eulerpartlemd 32727* | Lemma for eulerpart 32743: π· is the set of distinct part. of π. (Contributed by Thierry Arnoux, 11-Aug-2017.) |
β’ π = {π β (β0 βm β) β£ ((β‘π β β) β Fin β§ Ξ£π β β ((πβπ) Β· π) = π)} & β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} & β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} β β’ (π΄ β π· β (π΄ β π β§ (π΄ β β) β {0, 1})) | ||
Theorem | eulerpartlem1 32728* | Lemma for eulerpart 32743. (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 32729* | Lemma for eulerpart 32743. 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 32730* | Lemma for eulerpart 32743. (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 32731* | Lemma for eulerpart 32743: 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 32732* | Lemma for eulerpart 32743. (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 32733* | Lemma for eulerpart 32743: 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 32734* | Lemma for eulerpart 32743: 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 32735* | Lemma for eulerpart 32743. (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 32736* | Lemma for eulerpart 32743. (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 32737* | Lemma for eulerpart 32743: 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 32738* | Lemma for eulerpart 32743: Rewriting the π set for an odd partition Note that interestingly, this proof reuses marypha2lem2 9306. (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 32739* | Lemma for eulerpart 32743: 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 32740* | Lemma for eulerpart 32743: 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 32741* | Lemma for eulerpart 32743: 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 32742* | Lemma for eulerpart 32743. (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 32743* | 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 32744 | Sequences defined by strong recursion. |
class seqstr | ||
Definition | df-sseq 32745* | 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 32746 | Lemma for sseqp1 32756. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β π β V) & β’ (π β πΉ:β0βΆπ) & β’ (π β π β β0) β β’ (π β (πΉ βΎ (0..^π)) β Word π) | ||
Theorem | subiwrdlen 32747 | Length of a subword of an infinite word. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β π β V) & β’ (π β πΉ:β0βΆπ) & β’ (π β π β β0) β β’ (π β (β―β(πΉ βΎ (0..^π))) = π) | ||
Theorem | iwrdsplit 32748 | Lemma for sseqp1 32756. (Contributed by Thierry Arnoux, 25-Apr-2019.) (Proof shortened by AV, 14-Oct-2022.) |
β’ (π β π β V) & β’ (π β πΉ:β0βΆπ) & β’ (π β π β β0) β β’ (π β (πΉ βΎ (0..^(π + 1))) = ((πΉ βΎ (0..^π)) ++ β¨β(πΉβπ)ββ©)) | ||
Theorem | sseqval 32749* | 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 32750 | 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 32751 | 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 32752 | Lemma for sseqf 32753 amd sseqp1 32756. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β π β V) & β’ (π β π β Word π) & β’ π = (Word π β© (β‘β― β (β€β₯β(β―βπ)))) & β’ (π β πΉ:πβΆπ) β β’ (π β π β π) | ||
Theorem | sseqf 32753 | 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 32754 | 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 32755* | 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 32756 | 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 32757 | The Fibonacci sequence. |
class Fibci | ||
Definition | df-fib 32758 | 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 32759 | Lemma for fib0 32760, fib1 32761 and fibp1 32762. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π€ β (Word β0 β© (β‘β― β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))):(Word β0 β© (β‘β― β (β€β₯β(β―ββ¨β01ββ©))))βΆβ0 | ||
Theorem | fib0 32760 | Value of the Fibonacci sequence at index 0. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ0) = 0 | ||
Theorem | fib1 32761 | Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ1) = 1 | ||
Theorem | fibp1 32762 | Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (π β β β (Fibciβ(π + 1)) = ((Fibciβ(π β 1)) + (Fibciβπ))) | ||
Theorem | fib2 32763 | Value of the Fibonacci sequence at index 2. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ2) = 1 | ||
Theorem | fib3 32764 | Value of the Fibonacci sequence at index 3. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ3) = 2 | ||
Theorem | fib4 32765 | Value of the Fibonacci sequence at index 4. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ4) = 3 | ||
Theorem | fib5 32766 | Value of the Fibonacci sequence at index 5. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ5) = 5 | ||
Theorem | fib6 32767 | Value of the Fibonacci sequence at index 6. (Contributed by Thierry Arnoux, 25-Apr-2019.) |
β’ (Fibciβ6) = 8 | ||
Syntax | cprb 32768 | Extend class notation to include the class of probability measures. |
class Prob | ||
Definition | df-prob 32769 | 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 32770 | The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
β’ (π β Prob β (π β βͺ ran measures β§ (πββͺ dom π) = 1)) | ||
Theorem | domprobmeas 32771 | A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ (π β Prob β π β (measuresβdom π)) | ||
Theorem | domprobsiga 32772 | The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ (π β Prob β dom π β βͺ ran sigAlgebra) | ||
Theorem | probtot 32773 | The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
β’ (π β Prob β (πββͺ dom π) = 1) | ||
Theorem | prob01 32774 | 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 32775 | The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β Prob β (πββ ) = 0) | ||
Theorem | unveldomd 32776 | 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 32777 | 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 32778 | The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
β’ (π β Prob β β β dom π) | ||
Theorem | probcun 32779* | 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 32780 | 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 32781 | The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β (πβ(π΄ β π΅)) = ((πβπ΄) β (πβ(π΄ β© π΅)))) | ||
Theorem | probinc 32782 | A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.) |
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ π΄ β π΅) β (πβπ΄) β€ (πβπ΅)) | ||
Theorem | probdsb 32783 | 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 32784 | A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) β β’ (π β π β βͺ ran measures) | ||
Theorem | probvalrnd 32785 | The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π΄ β dom π) β β’ (π β (πβπ΄) β β) | ||
Theorem | probtotrnd 32786 | The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) β β’ (π β (πββͺ dom π) β β) | ||
Theorem | totprobd 32787* | Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β π β Prob) & β’ (π β π΄ β dom π) & β’ (π β π΅ β π« dom π) & β’ (π β βͺ π΅ = βͺ dom π) & β’ (π β π΅ βΌ Ο) & β’ (π β Disj π β π΅ π) β β’ (π β (πβπ΄) = Ξ£*π β π΅(πβ(π β© π΄))) | ||
Theorem | totprob 32788* | Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π β§ (βͺ π΅ = βͺ dom π β§ π΅ β π« dom π β§ (π΅ βΌ Ο β§ Disj π β π΅ π))) β (πβπ΄) = Ξ£*π β π΅(πβ(π β© π΄))) | ||
Theorem | probfinmeasb 32789 | Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+) β (π βf/c /π (πββͺ π)) β Prob) | ||
Theorem | probfinmeasbALTV 32790* | Alternate version of probfinmeasb 32789. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.) |
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+) β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β Prob) | ||
Theorem | probmeasb 32791* | Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π β§ (πβπ΄) β β+) β (π₯ β π β¦ ((πβ(π₯ β© π΄)) / (πβπ΄))) β Prob) | ||
Syntax | ccprob 32792 | Extends class notation with the conditional probability builder. |
class cprob | ||
Definition | df-cndprob 32793* | Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ cprob = (π β Prob β¦ (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ)))) | ||
Theorem | cndprobval 32794 | 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 32795 | 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 32796 | 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 32797 | 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 32798 | 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 32799* | 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 32800 | Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (πβπ΄) β 0 β§ (πβπ΅) β 0) β ((cprobβπ)ββ¨π΄, π΅β©) = ((((cprobβπ)ββ¨π΅, π΄β©) Β· (πβπ΄)) / (πβπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |