Home Metamath Proof ExplorerTheorem List (p. 237 of 322) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-21498) Hilbert Space Explorer (21499-23021) Users' Mathboxes (23022-32154)

Theorem List for Metamath Proof Explorer - 23601-23700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorempr01ssre 23601 The range of the indicator function is a subset of . (Contributed by Thierry Arnoux, 14-Aug-2017.)

Theoremind1 23602 Value of the indicator function where it is . (Contributed by Thierry Arnoux, 14-Aug-2017.)
D7ED;

Theoremind0 23603 Value of the indicator function where it is . (Contributed by Thierry Arnoux, 14-Aug-2017.)
D7ED;

Theoremind1a 23604 Value of the indicator function where it is . (Contributed by Thierry Arnoux, 22-Aug-2017.)
D7ED;

Theoremindpi1 23605 Preimage of the singleton by the indicator function. See i1f1lem 19044. (Contributed by Thierry Arnoux, 21-Aug-2017.)
D7ED;

Theoremindsum 23606* Finite sum of a product with the indicator function / cross-product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.)
D7ED;

Theoremindf1o 23607 The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.)
D7ED;

Theoremindpreima 23608 A function with range as an indicator of the preimage of (Contributed by Thierry Arnoux, 23-Aug-2017.)
D7ED;

Theoremindf1ofs 23609* The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.)
D7ED;

18.3.41  Probability Theory

Syntaxcprb 23610 Extend class notation to include the class of probability measures.
Prob

Definitiondf-prob 23611 Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016.)
Prob measures

Theoremelprob 23612 The property of being a probability measure (Contributed by Thierry Arnoux, 8-Dec-2016.)
Prob measures

Theoremdomprobmeas 23613 A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.)
Prob measures

Theoremdomprobsiga 23614 The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.)
Prob sigAlgebra

Theoremprobtot 23615 The Probbiliy of the universe set is 1 (Second axiom of Kolmogorov) (Contributed by Thierry Arnoux, 8-Dec-2016.)
Prob

Theoremprob01 23616 A Probbiliy is bounded in [ 0 , 1 ] (First axiom of Kolmogorov) (Contributed by Thierry Arnoux, 25-Dec-2016.)
Prob

Theoremprobnul 23617 The Probbiliy of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.)
Prob

Theoremunveldomd 23618 The universe is an element of the domain of the probability, the universe (entire probability space) being in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
Prob

Theoremunveldom 23619 The universe is an element of the domain of the probability, the universe (entire probability space) being in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
Prob

Theoremnuleldmp 23620 The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.)
Prob

Theoremprobcun 23621* 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 Disj Σ*

Theoremprobun 23622 The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.)
Prob

Theoremprobdif 23623 The probabiliy of the difference of two event sets (Contributed by Thierry Arnoux, 12-Dec-2016.)
Prob

Theoremprobinc 23624 A probabiliy law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.)
Prob

Theoremprobdsb 23625 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

Theoremprobmeasd 23626 A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.)
Prob       measures

Theoremprobvalrnd 23627 The value of a probability is a a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.)
Prob

Theoremprobtotrnd 23628 The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.)
Prob

Theoremtotprobd 23629* Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.)
Prob                                   Disj        Σ*

Theoremtotprob 23630* Law of total probability (Contributed by Thierry Arnoux, 25-Dec-2016.)
Prob Disj Σ*

TheoremprobfinmeasbOLD 23631* Build a probability measure from a finite measure (Contributed by Thierry Arnoux, 17-Dec-2016.)
measures /𝑒 Prob

Theoremprobfinmeasb 23632 Build a probability measure from a finite measure (Contributed by Thierry Arnoux, 31-Jan-2017.)
measures 𝑓/𝑐 /𝑒 Prob

Theoremprobmeasb 23633* Build a probability from a measure and a set with finite measure (Contributed by Thierry Arnoux, 25-Dec-2016.)
measures Prob

18.3.42  Conditional Probabilities

Syntaxccprob 23634 Extends class notation with the conditional probability builder.
cprob

Definitiondf-cndprob 23635* Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
cprob Prob

Theoremcndprobval 23636 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 cprob

Theoremcndprobin 23637 An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
Prob cprob

Theoremcndprob01 23638 The conditional probability has values in . (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
Prob cprob

Theoremcndprobtot 23639 The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
Prob cprob

Theoremcndprobnul 23640 The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
Prob cprob

Theoremcndprobprob 23641* The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
Prob cprob Prob

Theorembayesth 23642 Bayes Theorem (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
Prob cprob cprob

18.3.43  Real Valued Random Variables

Syntaxcrrv 23643 Extend class notation with the class of real valued random variables.
rRndVar

Definitiondf-rrv 23644 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 MblFnM 𝔅

Theoremrrvmbfm 23645 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 MblFnM 𝔅

Theoremisrrvv 23646* Elementhood to the set of real-valued random variables with respect to the probability . (Contributed by Thierry Arnoux, 25-Jan-2017.)
Prob       rRndVar 𝔅

Theoremrrvvf 23647 A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
Prob       rRndVar

Theoremrrvfn 23648 A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
Prob       rRndVar

Theoremrrvdm 23649 The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
Prob       rRndVar

Theoremrrvrnss 23650 The range of a random variable as a subset of . (Contributed by Thierry Arnoux, 6-Feb-2017.)
Prob       rRndVar

Theoremrrvf2 23651 A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
Prob       rRndVar

Theoremrrvdmss 23652 The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.)
Prob       rRndVar

Theoremrrvfinvima 23653* 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       𝔅

Theorem0rrv 23654* 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       rRndVar

Theoremrrvmulc 23655 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              𝑓/𝑐 rRndVar

18.3.44  Preimage set mapping operator

Syntaxcorvc 23656 Extend class notation to include the preimage set mapping operator.
RV/𝑐

Definitiondf-orvc 23657* 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/𝑐 , and keep a similar notation. Because with this notation RV/𝑐 is a set, we can also apply it to conditional probabilities, like in RV/𝑐 RV/𝑐 .

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/𝑐 cf. ideq 4836- elementhood: as RV/𝑐 cf. epel 4308- 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/𝑐

Theoremorvcval 23658* Value of the preimage mapping operator applied on a given random variable and constant (Contributed by Thierry Arnoux, 19-Jan-2017.)
RV/𝑐

Theoremorvcval2 23659* Another way to express the value of the preimage mapping operator (Contributed by Thierry Arnoux, 19-Jan-2017.)
RV/𝑐

Theoremelorvc 23660* Elementhood of a preimage (Contributed by Thierry Arnoux, 21-Jan-2017.)
RV/𝑐

Theoremorvcval4 23661* The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 23658 (Contributed by Thierry Arnoux, 21-Jan-2017.)
sigAlgebra              MblFnM sigaGen              RV/𝑐

Theoremorvcoel 23662* If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
sigAlgebra              MblFnM sigaGen                     RV/𝑐

Theoremorvccel 23663* If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
sigAlgebra              MblFnM sigaGen                     RV/𝑐

Theoremelorrvc 23664* Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.)
Prob       rRndVar              RV/𝑐

Theoremorrvcval4 23665* The value of the preimage mapping operator can be restricted to preimages of subsets of RR. (Contributed by Thierry Arnoux, 21-Jan-2017.)
Prob       rRndVar              RV/𝑐

Theoremorrvcoel 23666* If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
Prob       rRndVar                     RV/𝑐

Theoremorrvccel 23667* If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
Prob       rRndVar                     RV/𝑐

Theoremorvcgteel 23668 Preimage maps produced by the "greater than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
Prob       rRndVar              RV/𝑐

18.3.45  Distribution Functions

Theoremorvcelval 23669 Preimage maps produced by the "elementhood" relation (Contributed by Thierry Arnoux, 6-Feb-2017.)
Prob       rRndVar       𝔅       RV/𝑐

Theoremorvcelel 23670 Preimage maps produced by the "elementhood" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
Prob       rRndVar       𝔅       RV/𝑐

Theoremdstrvval 23671* The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.)
Prob       rRndVar       𝔅 RV/𝑐        𝔅

Theoremdstrvprob 23672* The distribution of a random variable is a probability law (TODO: could be shortened using dstrvval 23671) (Contributed by Thierry Arnoux, 10-Feb-2017.)
Prob       rRndVar       𝔅 RV/𝑐        Prob

18.3.46  Cumulative Distribution Functions

Theoremorvclteel 23673 Preimage maps produced by the "lower than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017.)
Prob       rRndVar              RV/𝑐

Theoremdstfrvel 23674 Elementhood of preimage maps produced by the "lower than or equal" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.)
Prob       rRndVar                            RV/𝑐

Theoremdstfrvunirn 23675* The limit of all preimage maps by the "lower than or equal" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017.)
Prob       rRndVar       RV/𝑐

Theoremorvclteinc 23676 Preimage maps produced by the "lower than or equal" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
Prob       rRndVar                            RV/𝑐 RV/𝑐

Theoremdstfrvinc 23677* A cumulative distribution function is non-decreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
Prob       rRndVar       RV/𝑐

Theoremdstfrvclim1 23678* 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/𝑐

18.3.47  Probabilities - example

Theoremcoinfliplem 23679 Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017.)
𝑓/𝑐               𝑓/𝑐 /𝑒

Theoremcoinflipprob 23680 The we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017.)
𝑓/𝑐               Prob

Theoremcoinflipspace 23681 The space of our coin-flip probability (Contributed by Thierry Arnoux, 15-Jan-2017.)
𝑓/𝑐

Theoremcoinflipuniv 23682 The universe of our coin-flip probability is . (Contributed by Thierry Arnoux, 15-Jan-2017.)
𝑓/𝑐

Theoremcoinfliprv 23683 The we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.)
𝑓/𝑐               rRndVar

Theoremcoinflippv 23684 The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-Jan-2017.)
𝑓/𝑐

Theoremcoinflippvt 23685 The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.)
𝑓/𝑐

18.4  Mathbox for Mario Carneiro

18.4.1  Miscellaneous stuff

Theoremquartfull 23686 The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015.)
; ; ; ;; ; ; ; ;; ; ; ;;        ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;;        ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;;

18.4.2  Zeta function

Syntaxczeta 23687 The Riemann zeta function.

Definitiondf-zeta 23688* Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except , but going from the alternating zeta function to the regular zeta function requires dividing by , which has zeroes other than . To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.)

Theoremzetacvg 23689* The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.)

18.4.3  Gamma function

Syntaxclgam 23690 Logarithm of the Gamma function.

Syntaxcgam 23691 The Gamma function.

Definitiondf-lgam 23692* Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to because the branch cuts are placed differently (we do have , though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers , where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)

Definitiondf-gam 23693 Define the Gamma function. See df-lgam 23692 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.)

Theoremeldmgm 23694 Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.)

Theoremdmgmaddn0 23695 If is not a nonpositive integer, then is nonzero for any nonnegative integer . (Contributed by Mario Carneiro, 12-Jul-2014.)

Theoremdmgmseqn0 23696* If is not a nonpositive integer, then is nonzero for any . (Contributed by Mario Carneiro, 12-Jul-2014.)

18.4.4  Derangements and the Subfactorial

Theoremderanglem 23697* Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.)

Theoremderangval 23698* Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015.)

Theoremderangf 23699* The derangement number is a function from finite sets to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)

Theoremderang0 23700* The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.)