![]() |
Metamath
Proof Explorer Theorem List (p. 338 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cprb 33701 | Extend class notation to include the class of probability measures. |
class Prob | ||
Definition | df-prob 33702 | 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 33703 | The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
β’ (π β Prob β (π β βͺ ran measures β§ (πββͺ dom π) = 1)) | ||
Theorem | domprobmeas 33704 | A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ (π β Prob β π β (measuresβdom π)) | ||
Theorem | domprobsiga 33705 | The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ (π β Prob β dom π β βͺ ran sigAlgebra) | ||
Theorem | probtot 33706 | The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016.) |
β’ (π β Prob β (πββͺ dom π) = 1) | ||
Theorem | prob01 33707 | 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 33708 | The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β Prob β (πββ ) = 0) | ||
Theorem | unveldomd 33709 | 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 33710 | 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 33711 | The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
β’ (π β Prob β β β dom π) | ||
Theorem | probcun 33712* | 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 33713 | 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 33714 | The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β (πβ(π΄ β π΅)) = ((πβπ΄) β (πβ(π΄ β© π΅)))) | ||
Theorem | probinc 33715 | A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.) |
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ π΄ β π΅) β (πβπ΄) β€ (πβπ΅)) | ||
Theorem | probdsb 33716 | 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 33717 | A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) β β’ (π β π β βͺ ran measures) | ||
Theorem | probvalrnd 33718 | The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π΄ β dom π) β β’ (π β (πβπ΄) β β) | ||
Theorem | probtotrnd 33719 | The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
β’ (π β π β Prob) β β’ (π β (πββͺ dom π) β β) | ||
Theorem | totprobd 33720* | Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ (π β π β Prob) & β’ (π β π΄ β dom π) & β’ (π β π΅ β π« dom π) & β’ (π β βͺ π΅ = βͺ dom π) & β’ (π β π΅ βΌ Ο) & β’ (π β Disj π β π΅ π) β β’ (π β (πβπ΄) = Ξ£*π β π΅(πβ(π β© π΄))) | ||
Theorem | totprob 33721* | Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β Prob β§ π΄ β dom π β§ (βͺ π΅ = βͺ dom π β§ π΅ β π« dom π β§ (π΅ βΌ Ο β§ Disj π β π΅ π))) β (πβπ΄) = Ξ£*π β π΅(πβ(π β© π΄))) | ||
Theorem | probfinmeasb 33722 | Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+) β (π βf/c /π (πββͺ π)) β Prob) | ||
Theorem | probfinmeasbALTV 33723* | Alternate version of probfinmeasb 33722. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.) |
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+) β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β Prob) | ||
Theorem | probmeasb 33724* | Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
β’ ((π β (measuresβπ) β§ π΄ β π β§ (πβπ΄) β β+) β (π₯ β π β¦ ((πβ(π₯ β© π΄)) / (πβπ΄))) β Prob) | ||
Syntax | ccprob 33725 | Extends class notation with the conditional probability builder. |
class cprob | ||
Definition | df-cndprob 33726* | Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
β’ cprob = (π β Prob β¦ (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ)))) | ||
Theorem | cndprobval 33727 | 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 33728 | 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 33729 | 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 33730 | 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 33731 | 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 33732* | 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 33733 | 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 33734 | Extend class notation with the class of real-valued random variables. |
class rRndVar | ||
Definition | df-rrv 33735 | 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 33736 | 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 33737* | 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 33738 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β π:βͺ dom πβΆβ) | ||
Theorem | rrvfn 33739 | A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β π Fn βͺ dom π) | ||
Theorem | rrvdm 33740 | The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β dom π = βͺ dom π) | ||
Theorem | rrvrnss 33741 | The range of a random variable as a subset of β. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β ran π β β) | ||
Theorem | rrvf2 33742 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β π:dom πβΆβ) | ||
Theorem | rrvdmss 33743 | The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β βͺ dom π β dom π) | ||
Theorem | rrvfinvima 33744* | For a real-value random variable π, any open interval in β is the image of a measurable set. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β βπ¦ β π β (β‘π β π¦) β dom π) | ||
Theorem | 0rrv 33745* | The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017.) (Revised by Thierry Arnoux, 30-Jan-2017.) |
β’ (π β π β Prob) β β’ (π β (π₯ β βͺ dom π β¦ 0) β (rRndVarβπ)) | ||
Theorem | rrvadd 33746 | The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π β (rRndVarβπ)) β β’ (π β (π βf + π) β (rRndVarβπ)) | ||
Theorem | rrvmulc 33747 | A random variable multiplied by a constant is a random variable. (Contributed by Thierry Arnoux, 17-Jan-2017.) (Revised by Thierry Arnoux, 22-May-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β πΆ β β) β β’ (π β (π βf/c Β· πΆ) β (rRndVarβπ)) | ||
Theorem | rrvsum 33748 | An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017.) |
β’ (π β π β Prob) & β’ (π β π:ββΆ(rRndVarβπ)) & β’ ((π β§ π β β) β π = (seq1( βf + , π)βπ)) β β’ ((π β§ π β β) β π β (rRndVarβπ)) | ||
Syntax | corvc 33749 | Extend class notation to include the preimage set mapping operator. |
class βRV/ππ | ||
Definition | df-orvc 33750* |
Define the preimage set mapping operator. In probability theory, the
notation π(π = π΄) denotes the probability that a
random variable
π takes the value π΄. We
introduce here an operator which
enables to write this in Metamath as (πβ(πβRV/π I π΄)), and
keep a similar notation. Because with this notation (πβRV/π I π΄)
is a set, we can also apply it to conditional probabilities, like in
(πβ(πβRV/π I π΄) β£ (πβRV/π I π΅))).
The oRVC operator transforms a relation π into an operation taking a random variable π and a constant πΆ, and returning the preimage through π of the equivalence class of πΆ. The most commonly used relations are: - equality: {π = π΄} as (πβRV/π I π΄) cf. ideq 5853- elementhood: {π β π΄} as (πβRV/π E π΄) cf. epel 5584- less-than: {π β€ π΄} as (πβRV/π β€ π΄) Even though it is primarily designed to be used within probability theory and with random variables, this operator is defined on generic functions, and could be used in other fields, e.g., for continuous functions. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
β’ βRV/ππ = (π₯ β {π₯ β£ Fun π₯}, π β V β¦ (β‘π₯ β {π¦ β£ π¦π π})) | ||
Theorem | orvcval 33751* | Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
β’ (π β Fun π) & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β (πβRV/ππ π΄) = (β‘π β {π¦ β£ π¦π π΄})) | ||
Theorem | orvcval2 33752* | Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
β’ (π β Fun π) & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β (πβRV/ππ π΄) = {π§ β dom π β£ (πβπ§)π π΄}) | ||
Theorem | elorvc 33753* | Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β Fun π) & β’ (π β π β π) & β’ (π β π΄ β π) β β’ ((π β§ π§ β dom π) β (π§ β (πβRV/ππ π΄) β (πβπ§)π π΄)) | ||
Theorem | orvcval4 33754* | The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 33751. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β π β βͺ ran sigAlgebra) & β’ (π β π½ β Top) & β’ (π β π β (πMblFnM(sigaGenβπ½))) & β’ (π β π΄ β π) β β’ (π β (πβRV/ππ π΄) = (β‘π β {π¦ β βͺ π½ β£ π¦π π΄})) | ||
Theorem | orvcoel 33755* | If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β π β βͺ ran sigAlgebra) & β’ (π β π½ β Top) & β’ (π β π β (πMblFnM(sigaGenβπ½))) & β’ (π β π΄ β π) & β’ (π β {π¦ β βͺ π½ β£ π¦π π΄} β π½) β β’ (π β (πβRV/ππ π΄) β π) | ||
Theorem | orvccel 33756* | If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β π β βͺ ran sigAlgebra) & β’ (π β π½ β Top) & β’ (π β π β (πMblFnM(sigaGenβπ½))) & β’ (π β π΄ β π) & β’ (π β {π¦ β βͺ π½ β£ π¦π π΄} β (Clsdβπ½)) β β’ (π β (πβRV/ππ π΄) β π) | ||
Theorem | elorrvc 33757* | Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β π) β β’ ((π β§ π§ β βͺ dom π) β (π§ β (πβRV/ππ π΄) β (πβπ§)π π΄)) | ||
Theorem | orrvcval4 33758* | The value of the preimage mapping operator can be restricted to preimages of subsets of β. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β π) β β’ (π β (πβRV/ππ π΄) = (β‘π β {π¦ β β β£ π¦π π΄})) | ||
Theorem | orrvcoel 33759* | If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β π) & β’ (π β {π¦ β β β£ π¦π π΄} β (topGenβran (,))) β β’ (π β (πβRV/ππ π΄) β dom π) | ||
Theorem | orrvccel 33760* | If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β π) & β’ (π β {π¦ β β β£ π¦π π΄} β (Clsdβ(topGenβran (,)))) β β’ (π β (πβRV/ππ π΄) β dom π) | ||
Theorem | orvcgteel 33761 | Preimage maps produced by the "greater than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β β) β β’ (π β (πβRV/πβ‘ β€ π΄) β dom π) | ||
Theorem | orvcelval 33762 | Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β π β) β β’ (π β (πβRV/π E π΄) = (β‘π β π΄)) | ||
Theorem | orvcelel 33763 | Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β π β) β β’ (π β (πβRV/π E π΄) β dom π) | ||
Theorem | dstrvval 33764* | The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π· = (π β π β β¦ (πβ(πβRV/π E π)))) & β’ (π β π΄ β π β) β β’ (π β (π·βπ΄) = (πβ(β‘π β π΄))) | ||
Theorem | dstrvprob 33765* | The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval 33764). (Contributed by Thierry Arnoux, 10-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π· = (π β π β β¦ (πβ(πβRV/π E π)))) β β’ (π β π· β Prob) | ||
Theorem | orvclteel 33766 | Preimage maps produced by the "less than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β β) β β’ (π β (πβRV/π β€ π΄) β dom π) | ||
Theorem | dstfrvel 33767 | Elementhood of preimage maps produced by the "less than or equal to" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β β) & β’ (π β π΅ β βͺ dom π) & β’ (π β (πβπ΅) β€ π΄) β β’ (π β π΅ β (πβRV/π β€ π΄)) | ||
Theorem | dstfrvunirn 33768* | The limit of all preimage maps by the "less than or equal to" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) β β’ (π β βͺ ran (π β β β¦ (πβRV/π β€ π)) = βͺ dom π) | ||
Theorem | orvclteinc 33769 | Preimage maps produced by the "less than or equal to" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (πβRV/π β€ π΄) β (πβRV/π β€ π΅)) | ||
Theorem | dstfrvinc 33770* | A cumulative distribution function is nondecreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β πΉ = (π₯ β β β¦ (πβ(πβRV/π β€ π₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (πΉβπ΄) β€ (πΉβπ΅)) | ||
Theorem | dstfrvclim1 33771* | The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.) |
β’ (π β π β Prob) & β’ (π β π β (rRndVarβπ)) & β’ (π β πΉ = (π₯ β β β¦ (πβ(πβRV/π β€ π₯)))) β β’ (π β πΉ β 1) | ||
Theorem | coinfliplem 33772 | Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
β’ π» β V & β’ π β V & β’ π» β π & β’ π = ((β― βΎ π« {π», π}) βf/c / 2) & β’ π = {β¨π», 1β©, β¨π, 0β©} β β’ π = ((β― βΎ π« {π», π}) βf/c /π 2) | ||
Theorem | coinflipprob 33773 | The π we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
β’ π» β V & β’ π β V & β’ π» β π & β’ π = ((β― βΎ π« {π», π}) βf/c / 2) & β’ π = {β¨π», 1β©, β¨π, 0β©} β β’ π β Prob | ||
Theorem | coinflipspace 33774 | The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
β’ π» β V & β’ π β V & β’ π» β π & β’ π = ((β― βΎ π« {π», π}) βf/c / 2) & β’ π = {β¨π», 1β©, β¨π, 0β©} β β’ dom π = π« {π», π} | ||
Theorem | coinflipuniv 33775 | The universe of our coin-flip probability is {π», π}. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
β’ π» β V & β’ π β V & β’ π» β π & β’ π = ((β― βΎ π« {π», π}) βf/c / 2) & β’ π = {β¨π», 1β©, β¨π, 0β©} β β’ βͺ dom π = {π», π} | ||
Theorem | coinfliprv 33776 | The π we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
β’ π» β V & β’ π β V & β’ π» β π & β’ π = ((β― βΎ π« {π», π}) βf/c / 2) & β’ π = {β¨π», 1β©, β¨π, 0β©} β β’ π β (rRndVarβπ) | ||
Theorem | coinflippv 33777 | The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
β’ π» β V & β’ π β V & β’ π» β π & β’ π = ((β― βΎ π« {π», π}) βf/c / 2) & β’ π = {β¨π», 1β©, β¨π, 0β©} β β’ (πβ{π»}) = (1 / 2) | ||
Theorem | coinflippvt 33778 | The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
β’ π» β V & β’ π β V & β’ π» β π & β’ π = ((β― βΎ π« {π», π}) βf/c / 2) & β’ π = {β¨π», 1β©, β¨π, 0β©} β β’ (πβ{π}) = (1 / 2) | ||
Theorem | ballotlemoex 33779* | π is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} β β’ π β V | ||
Theorem | ballotlem1 33780* | The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} β β’ (β―βπ) = ((π + π)Cπ) | ||
Theorem | ballotlemelo 33781* | Elementhood in π. (Contributed by Thierry Arnoux, 17-Apr-2017.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} β β’ (πΆ β π β (πΆ β (1...(π + π)) β§ (β―βπΆ) = π)) | ||
Theorem | ballotlem2 33782* | The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) β β’ (πβ{π β π β£ Β¬ 1 β π}) = (π / (π + π)) | ||
Theorem | ballotlemfval 33783* | The value of πΉ. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ (π β πΆ β π) & β’ (π β π½ β β€) β β’ (π β ((πΉβπΆ)βπ½) = ((β―β((1...π½) β© πΆ)) β (β―β((1...π½) β πΆ)))) | ||
Theorem | ballotlemfelz 33784* | (πΉβπΆ) has values in β€. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ (π β πΆ β π) & β’ (π β π½ β β€) β β’ (π β ((πΉβπΆ)βπ½) β β€) | ||
Theorem | ballotlemfp1 33785* | If the π½ th ballot is for A, (πΉβπΆ) goes up 1. If the π½ th ballot is for B, (πΉβπΆ) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ (π β πΆ β π) & β’ (π β π½ β β) β β’ (π β ((Β¬ π½ β πΆ β ((πΉβπΆ)βπ½) = (((πΉβπΆ)β(π½ β 1)) β 1)) β§ (π½ β πΆ β ((πΉβπΆ)βπ½) = (((πΉβπΆ)β(π½ β 1)) + 1)))) | ||
Theorem | ballotlemfc0 33786* | πΉ takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ (π β πΆ β π) & β’ (π β π½ β β) & β’ (π β βπ β (1...π½)((πΉβπΆ)βπ) β€ 0) & β’ (π β 0 < ((πΉβπΆ)βπ½)) β β’ (π β βπ β (1...π½)((πΉβπΆ)βπ) = 0) | ||
Theorem | ballotlemfcc 33787* | πΉ takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ (π β πΆ β π) & β’ (π β π½ β β) & β’ (π β βπ β (1...π½)0 β€ ((πΉβπΆ)βπ)) & β’ (π β ((πΉβπΆ)βπ½) < 0) β β’ (π β βπ β (1...π½)((πΉβπΆ)βπ) = 0) | ||
Theorem | ballotlemfmpn 33788* | (πΉβπΆ) finishes counting at (π β π). (Contributed by Thierry Arnoux, 25-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) β β’ (πΆ β π β ((πΉβπΆ)β(π + π)) = (π β π)) | ||
Theorem | ballotlemfval0 33789* | (πΉβπΆ) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) β β’ (πΆ β π β ((πΉβπΆ)β0) = 0) | ||
Theorem | ballotleme 33790* | Elements of πΈ. (Contributed by Thierry Arnoux, 14-Dec-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} β β’ (πΆ β πΈ β (πΆ β π β§ βπ β (1...(π + π))0 < ((πΉβπΆ)βπ))) | ||
Theorem | ballotlemodife 33791* | Elements of (π β πΈ). (Contributed by Thierry Arnoux, 7-Dec-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} β β’ (πΆ β (π β πΈ) β (πΆ β π β§ βπ β (1...(π + π))((πΉβπΆ)βπ) β€ 0)) | ||
Theorem | ballotlem4 33792* | If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} β β’ (πΆ β π β (Β¬ 1 β πΆ β Β¬ πΆ β πΈ)) | ||
Theorem | ballotlem5 33793* | If A is not ahead throughout, there is a π where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π β β’ (πΆ β (π β πΈ) β βπ β (1...(π + π))((πΉβπΆ)βπ) = 0) | ||
Theorem | ballotlemi 33794* | Value of πΌ for a given counting πΆ. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π & β’ πΌ = (π β (π β πΈ) β¦ inf({π β (1...(π + π)) β£ ((πΉβπ)βπ) = 0}, β, < )) β β’ (πΆ β (π β πΈ) β (πΌβπΆ) = inf({π β (1...(π + π)) β£ ((πΉβπΆ)βπ) = 0}, β, < )) | ||
Theorem | ballotlemiex 33795* | Properties of (πΌβπΆ). (Contributed by Thierry Arnoux, 12-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π & β’ πΌ = (π β (π β πΈ) β¦ inf({π β (1...(π + π)) β£ ((πΉβπ)βπ) = 0}, β, < )) β β’ (πΆ β (π β πΈ) β ((πΌβπΆ) β (1...(π + π)) β§ ((πΉβπΆ)β(πΌβπΆ)) = 0)) | ||
Theorem | ballotlemi1 33796* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π & β’ πΌ = (π β (π β πΈ) β¦ inf({π β (1...(π + π)) β£ ((πΉβπ)βπ) = 0}, β, < )) β β’ ((πΆ β (π β πΈ) β§ Β¬ 1 β πΆ) β (πΌβπΆ) β 1) | ||
Theorem | ballotlemii 33797* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π & β’ πΌ = (π β (π β πΈ) β¦ inf({π β (1...(π + π)) β£ ((πΉβπ)βπ) = 0}, β, < )) β β’ ((πΆ β (π β πΈ) β§ 1 β πΆ) β (πΌβπΆ) β 1) | ||
Theorem | ballotlemsup 33798* | The set of zeroes of πΉ satisfies the conditions to have a supremum. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π & β’ πΌ = (π β (π β πΈ) β¦ inf({π β (1...(π + π)) β£ ((πΉβπ)βπ) = 0}, β, < )) β β’ (πΆ β (π β πΈ) β βπ§ β β (βπ€ β {π β (1...(π + π)) β£ ((πΉβπΆ)βπ) = 0} Β¬ π€ < π§ β§ βπ€ β β (π§ < π€ β βπ¦ β {π β (1...(π + π)) β£ ((πΉβπΆ)βπ) = 0}π¦ < π€))) | ||
Theorem | ballotlemimin 33799* | (πΌβπΆ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π & β’ πΌ = (π β (π β πΈ) β¦ inf({π β (1...(π + π)) β£ ((πΉβπ)βπ) = 0}, β, < )) β β’ (πΆ β (π β πΈ) β Β¬ βπ β (1...((πΌβπΆ) β 1))((πΉβπΆ)βπ) = 0) | ||
Theorem | ballotlemic 33800* | If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.) |
β’ π β β & β’ π β β & β’ π = {π β π« (1...(π + π)) β£ (β―βπ) = π} & β’ π = (π₯ β π« π β¦ ((β―βπ₯) / (β―βπ))) & β’ πΉ = (π β π β¦ (π β β€ β¦ ((β―β((1...π) β© π)) β (β―β((1...π) β π))))) & β’ πΈ = {π β π β£ βπ β (1...(π + π))0 < ((πΉβπ)βπ)} & β’ π < π & β’ πΌ = (π β (π β πΈ) β¦ inf({π β (1...(π + π)) β£ ((πΉβπ)βπ) = 0}, β, < )) β β’ ((πΆ β (π β πΈ) β§ Β¬ 1 β πΆ) β (πΌβπΆ) β πΆ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |