| R3562: Real conditional variance partition into conditional moments |
| R3260: Weak law of large numbers for random real triangular arrays |
| R3645: Countable partition additivity of unsigned basic measure |
| R5073: Determinant of an upper triangular complex matrix |
| R5049: |
| R2798: Moments of an indicator random boolean number |
| R5545: Trace of conjugate transpose equals conjugate of trace |
| R1035: Power set is closed under intersections |
| R4849: Symmetry of simple mutual information |
| R4904: Derivative for real square function |
| R4845: Joint entropy formula for simple mutual information |
| R4206: Basic real golden ratio is a root of a quadratic basic real polynomial |
| R1856: Cardinality of the set of maps between finite sets |
| R508: Finite cartesian product of countable sets is countable |
| R5186: Unique global minimizer for a finite product of positive real numbers with a given sum of multiplicative inverses |
| R1975: Measure of set in backward orbit under measure-preserving endomorphism |
| R3883: Row-standardisation of row-independent random real triangular array |
| R24: Parallelogram identity |
| R2405: Characteristic function uniquely identifies the distribution of a random real number |
| R1540: Affine map preserves convex sets in images |
| R3516: Signed basic expectation of almost surely zero random number is zero |
| R5085: Eigenvalues of a symmetric real matrix are real-valued |
| R2410: I.I.D. real weak law of large numbers under finite second absolute moments |
| R4092: Real arithmetic expression for real harmonic mean |
| R800: Proof by principle of weak mathematical induction |
| R75: Intersection of closed sets is closed |
| R4503: Countable union of sets of measure zero is of measure zero |
| R3090: Scaling property of binomial coefficient |
| R2970: The four classes of real intervals are each closed under translation |
| R4836: Change of base formula for simple entropy |
| R2665: Characteristic function of gaussian random real number |
| R4867: Initial sum of powers of two |
| R5008: Random unsigned basic number almost surely finite if expectation is finite |
| R4055: Singleton map is injection from set to power set |
| R3514: Unsigned basic expectation over set of probability zero is zero |
| R4048: Number of binary relations on binary cartesian product |
| R2548: Constant map pulls back a bottom sigma-algebra |
| R5560: Characteristic polynomial for a triangular complex matrix |
| R4814: Markov chain triple iff reverse is a Markov chain triple |
| R3472: Maximum modulus principle |
| R5060: Product of a real square matrix and its adjugate is a constant diagonal matrix |
| R4804: Probability distribution function for geometric random positive integer |
| R5276: Probability to win an I.I.D. exponential race |
| R4740: Upper bound to the probability that two finite random euclidean real sums equal each other |
| R4782: Expectation of conditional expectation for a random real number |
| R5562: Characteristic polynomial for a lower triangular complex matrix |
| R3640: Conditional probability given independent sigma-algebra |
| R3921: Identically distributed random collection need not be stationary |
| R5234: Sample mean of independent gaussian random real numbers is a gaussian random real number |
| R5094: Number of boolean functions on a boolean cartesian product |
| R4598: Standard gaussian real density function is an even function |
| R4777: Expectation of bounded random real number is within the bounding interval |
| R4562: Basic integral over a set of measure zero is zero |
| R2483: Variance of Bernoulli random boolean number |
| R4468: Set of stationary measurable sets is a sigma-algebra |
| R5301: Random unsigned basic number has zero correlation with the empty indicator |
| R5561: Characteristic polynomial for an upper triangular complex matrix |
| R4931: |
| R3506: Finite union of countable sets is countable |
| R3938: Upper and lower bounds for codomain set of probability measure |
| R797: Principle of weak mathematical induction on the natural numbers |
| R2259: Variance of a finite sum of random real numbers |
| R5235: Sample mean of I.I.D. gaussian random real numbers is a gaussian random real number |
| R3381: Product of rational and irrational number is irrational |
| R5484: Columns of a real matrix which span the whole space need not be real-linearly independent |
| R5662: Reflection property of standard logarithm function for a single positive real number |
| R3512: Unsigned basic integral over set of measure zero is zero |
| R4262: Finite cartesian product with empty set is empty |
| R1839: Cardinality of power set of a finite set |
| R3679: Standardised I.I.D. real central limit theorem with the identity index sequence |
| R5673: Complex arithmetic expression for the multiplicative inverse of a complex number |
| R4899: |
| R2875: Cauchy's real mean value theorem |
| R4213: Countable set union is invariant under bijective shifting of indices |
| R4637: |
| R5251: Exponential random positive real number is a gamma random positive real number |
| R1566: Mean value theorem for Riemann integral |
| R756: Abelian group iff centre is whole group |
| R4308: Map composition need not be commutative |
| R2748: Finite sets are closed in metric space |
| R1903: Basic integral of almost everywhere zero function is zero |
| R5405: Standard I.I.D. real central limit theorem |
| R5643: Cardinality of the set of bytes |
| R4287: Finite product of even complex functions is even |
| R233: Whole space is closed |
| R5513: Real matrix determinant is homogeneous with respect to multiplying a row or a column by a constant |
| R292: Union is smallest upper bound |
| R2962: Characterisation of standard natural real exponential function by a differential equation |
| R5273: Finiteness of expectation in general does not imply finiteness of variance for random real number |
| R5644: Complement formula for the sum of initial natural numbers |
| R893: Cyclic group is Abelian |
| R4741: Probabilistic Chebyshov's inequality for square function |
| R5500: Transpose of real matrix inverse is inverse to the transpose |
| R3646: Countable partition additivity of probability measure |
| R3228: Bounded sequence need not be Cauchy |
| R4801: Probability mass function for cogeometric random basic natural number |
| R3738: Median need not be unique for a random real number |
| R1904: Isotonicity of finite real summation |
| R4329: Probability of countable intersection with an almost sure event |
| R4919: Measurable transformation preserves independent countable random collection |
| R5565: Eigenvalue sequence for a lower triangular complex matrix |
| R3517: Unsigned basic expectation zero iff random number almost surely zero |
| R2310: Distribution formula for unsigned basic integral |
| R1338: Probabilistic Borel-Cantelli lemma |
| R4607: Pushforward change of variables formula for unsigned basic integral |
| R4631: Cardinality of finite cartesian products is invariant under insertion of parentheses |
| R4970: |
| R5511: Interchanging two rows or two columns of a real square matrix switches the sign of the determinant |
| R5524: Complex arithmetic expression for the determinant of a 3-by-3 complex square matrix |
| R87: Convolution is commutative |
| R5619: |
| R2986: Lebesgue outer measure under scaling |
| R4811: Markov chain triple iff endpoints conditionally independent |
| R2313: Expectation with dual probability distribution function |
| R5237: Finite sum of uncorrelated identically distributed gaussian random real numbers is a gaussian random real number |
| R1232: Tonelli's theorem for sums and integrals |
| R4817: Data processing inequality for transformed endpoint |
| R979: Countable subadditivity of measure |
| R4929: Binary partition additivity of probability measure |
| R4149: Countable intersection is a lower bound to each set in the intersection |
| R4943: Real binomial theorem for exponent three |
| R4869: Characterisation of subconvex real functions |
| R2090: Isotonicity of probability measure |
| R5362: Probability that a continuous random real number takes value in the rational numbers is zero |
| R5173: Transpose of a product of three complex matrices |
| R4848: Probability of event conditional on complement |
| R5193: Maximal value for a directional derivative at a point |
| R3996: |
| R1372: Inner product is zero if either argument is zero |
| R4292: Finite cartesian product of finite sets is finite |
| R1577: Cauchy's theorem for a disc |
| R4926: Finite partition additivity of unsigned basic measure |
| R5285: Expectation of a gaussian random real number |
| R4333: Binary product of indicator functions equals indicator of intersection |
| R4189: |
| R2677: Law of total probability for a countable partition of events of positive probability |
| R4907: Strong derivative for constant euclidean real function |
| R4998: Limit of distribution function of geometric random positive integer scaled by reciprocal of index |
| R4325: Probability one if conditional probability one relative to event of probability one |
| R5532: Complex matrix determinant equals product of eigenvalues |
| R2750: Fourier transform of finite unsigned euclidean real Borel measure is uniformly bounded |
| R4706: Complex conjugate zero iff argument zero |
| R4601: Element in countable cartesian product iff components in images of canonical projections |
| R4805: Dual probability distribution function for geometric random positive integer |
| R4932: |
| R315: Composition of surjections is surjection |
| R4823: Conditional probability of the empty event |
| R1164: Translation invariance of Lebesgue measure |
| R2367: Law of total variance |
| R3784: Law of total probability for complex expectation in terms of pullback events of a discrete random variable |
| R4927: Binary partition additivity of unsigned basic measure |
| R4278: Expression for probability of event in terms of complement event |
| R5575: Traces of complex matrix gramians coincide |
| R4314: Number of boolean functions on a finite set |
| R4430: Probability of event in backward orbit under probability-preserving endomorphism |
| R1130: Intersection is largest lower bound |
| R3199: Finite sum of uncorrelated Bernoulli random numbers is a binomial random number |
| R293: Open set less closed set is open |
| R4729: Complex binomial inequality |
| R457: Fréchet space iff singletons are closed |
| R1166: Lebesgue measure under scaling |
| R716: Equivalence class is not empty |
| R4920: Measurable transformation preserves independent finite random collection |
| R1036: Power set is closed under complements |
| R3988: Expression for quadratic form of real square matrix in terms of symmetric part |
| R424: Euler's identity |
| R5086: Eigenvectors for a symmetric real matrix are orthogonal |
| R5284: Expectation of a Bernoulli random boolean number |
| R4279: Explicit algebraic expression for elements of generated subgroup with singleton generator set |
| R2955: Reciprocal positive integer sequence converges to zero |
| R4165: Superset of countable union iff superset of every set in the union |
| R2075: Image of empty set |
| R248: Binary subadditivity of basic real square root function |
| R4754: |
| R3547: Expectation minimises second central moment for random real number |
| R10: Binary cartesian product with empty set is empty |
| R47: Set difference is subset of the minuend |
| R4780: Real conditional expectation given independent sigma-algebra |
| R2963: Odd function equals its odd part |
| R3595: Probabilistic Tonelli's theorem |
| R3863: Signed basic integral with respect to a point measure |
| R371: Countable set iff injection to natural numbers |
| R5502: Real conditional expectation with respect to a constant random real number |
| R5508: Real square matrix invertible iff determinant nonzero |
| R5093: Total number of fixed-length sequences using a given number of labels |
| R2492: Independent event collection is pairwise independent |
| R5556: Squared eigenvalue is an eigenvalue for the square of a complex matrix |
| R354: Image of singleton set |
| R4093: Real harmonic and arithmetic means are multiplicative inverses when arguments are |
| R4338: Conditional probability of almost surely true event |
| R4689: Probabilistic Cavalieri principle |
| R4326: Probability of binary union with almost sure event |
| R74: Finite union of closed sets is closed |
| R4610: |
| R5180: Tight upper bound to directional derivative |
| R5188: |
| R3507: Binary union of countable sets is countable |
| R2463: Determinant of a real identity matrix |
| R263: Binary cartesian product of countable sets is countable |
| R1193: Finite product of indicator functions equals indicator of intersection |
| R5324: Conditional expectation of a random real number conditioned on itself |
| R5679: Given convex coefficient parameters, equal allocation maximizes uncorrelated finite Bernoulli product |
| R2160: Conditional expectation of known random complex number |
| R5624: Euclidean real dot product is symmetric |
| R4930: |
| R4470: Inverse image of countable union is union of inverse images |
| R4617: The standard mollifier integrates to one |
| R4639: Characteristic function for translated random real number |
| R26: Pythagorean theorem |
| R982: Sequential continuity of measure from below |
| R3908: Characteristic function of almost surely constant random euclidean real number |
| R4602: Element in finite cartesian product iff components in images of canonical projections |
| R5165: Central limit theorem for I.I.D. sample mean series |
| R4948: Gaussian approximation to standard binomial distribution |
| R5168: Infinite product of real numbers in right-closed unit interval vanishes iff infinite sum of duals diverges |
| R5559: Characteristic polynomial for a complex diagonal matrix |
| R3970: Measure of finite union finite iff measure of all sets in union finite |
| R5509: Cofactor partition for the determinant of a 3-by-3 real square matrix |
| R2588: Weak Stirling formula |
| R2168: Isotonicity of Lebesgue outer measure |
| R3601: Gaussian approximation to standard Poisson distribution |
| R4131: Markov lower bound on unsigned basic expectation |
| R1868: Composition of indicator function with set endomorphism |
| R4730: Riemann integral of a constant function on the closed unit interval |
| R4972: Bias-variance partition of mean square error for a random real column matrix |
| R1762: Closed set less open set is closed |
| R5520: Cofactor partition for a 2-by-2 complex square matrix |
| R4695: An infinite product of real numbers on the open unit interval need not converge to zero |
| R5175: Derivative function for standard natural real logarithm function |
| R4010: Polish space is first-countable |
| R5530: Determinant of a scaled real matrix |
| R4915: |
| R4732: |
| R5170: Expectation of conditional expectation for a random complex number |
| R301: Canonical identity map is an injection |
| R2950: Complex conjugation operation is an involution |
| R5070: Determinant of a diagonal complex matrix with constant diagonal |
| R2938: Vanishing sequence is necessary but not sufficient for finiteness of real series |
| R3954: Two almost surely equal random variables are identically distributed |
| R4277: Measure of measurable set complement |
| R1818: Isotonicity of real expectation |
| R5485: Columns of a real matrix need not span the whole space |
| R4483: Real number is zero iff equal to its reflection |
| R425: Euler's formulas for a real variable |
| R4118: Real arithmetic expression for unsigned real geometric mean |
| R4705: Inner product with repeating argument is a real number |
| R4787: |
| R4808: Affine transformations preserve independent real pairs |
| R1177: Constant map is always measurable |
| R102: Singletons are closed in a metric space |
| R5514: Determinant of a complex identity matrix |
| R2615: Empty set is cofinite within a finite set |
| R1076: Minimum element is unique |
| R5097: Power set is isomorphic to a set of boolean functions |
| R2220: Binary set intersection is commutative |
| R4328: Probability of finite union with an almost sure event |
| R5525: Complex square matrix which has a zero column or a zero row has determinant zero |
| R4215: Countable set intersection is invariant under bijective shifting of indices |
| R5291: Complex conjugate of a complex eigenvalue of a real matrix is an eigenvalue |
| R4141: Probabilistic Chernoff inequality |
| R5621: |
| R2164: Law of the excluded middle in probability calculus |
| R4145: Binary union is an upper bound to both sets in the union |
| R3896: Idempotence of real expectation |
| R2100: Triangle inequality for signed basic expectation |
| R5233: Finite sum of I.I.D. gaussian random real numbers is a gaussian random real number |
| R2223: Binary set union is commutative |
| R4261: Real binomial theorem for exponent two |
| R1514: Isotonicity of signed basic integral |
| R4437: Complement of stationary measurable set is stationary |
| R4368: Set of euclidean integers has Lebesgue measure zero |
| R4577: Countable indicator partition of complex expectation in terms of pullback events |
| R4390: Fourier transform characterises euclidean real probability measure |
| R1034: Power set is closed under unions |
| R2413: Complex conjugate of real number |
| R298: Identity map is continuous if topology on domain set is equal or stronger |
| R1064: Isotonicity of Lebesgue measure |
| R5379: Distribution of the real Wiener process at a given point is gaussian |
| R3912: Characteristic function of rademacher random integer |
| R2989: Unsigned basic Lebesgue integral under scaling |
| R648: Proportionally bounded linear map is Lipschitz |
| R1854: Cardinality of the set of injections between finite sets |
| R4996: |
| R5591: Real matrix gramians are positive semidefinite |
| R4627: |
| R4216: Finite set intersection is invariant under bijective shifting of indices |
| R4132: Strict version of probabilistic Markov inequality |
| R3600: Finite sum of independent Poisson random natural numbers is Poisson |
| R5544: Real matrix trace is preserved by transposing |
| R4538: Inclusion of image does not imply inclusion of inverse image |
| R3200: Characteristic function of Bernoulli random boolean number |
| R3633: Bessel-corrected sample variance is an unbiased estimator for the variance of uncorrelated identically distributed random real numbers |
| R4272: Absolute value function is not strictly antitone |
| R5308: Multiplying by the same random real number need not preserve equality in distribution |
| R4542: Map is inverse to its inverse |
| R2074: Isotonicity of inverse image |
| R76: Empty set is closed |
| R4802: Law of total probability for complement partition in terms of random variables |
| R2589: Trivial factorial upper bound |
| R5498: Inverse matrix is unique for real square matrix |
| R738: Left and right cosets coincide in Abelian group |
| R4822: Conditional probability of the sample space |
| R3611: |
| R4876: Interval length upper bound to variance of bounded random real number |
| R2966: Indicator function under scaling of the argument |
| R4267: Set intersection with empty set is empty |
| R3680: Characteristic function of standard gaussian random real number |
| R3231: Riemann integral analogue to infinite geometric series |
| R4786: Real conditional covariance partition into conditional moments |
| R1178: Continuous map is Borel measurable |
| R90: Complex function convolution is homogeneous to degree one |
| R3204: Characteristic function of geometric random positive integer |
| R2080: Union is upper bound for intersection |
| R5169: Infinite product of real numbers in right-closed unit interval does not vanish iff infinite sum of duals converges |
| R4387: Characteristic function of standard Poisson random natural number |
| R1236: Markov's inequality |
| R4800: Number of injections from a finite set to itself |
| R4900: |
| R1234: Borel-Cantelli lemma |
| R1406: Collection of sets ordered by inclusion contains a maximal element |
| R4007: Singletons are closed in Polish space |
| R4757: Young's inequality for two real numbers |
| R2556: Probability calculus expression for probability conditioned on event of nonzero probability |
| R1171: Isotonicity of Euclidean volume function |
| R5359: Reflection property of simple relative entropy |
| R4174: Proper contraction has at most a single fixed point |
| R4228: Real ordering is compatible with addition |
| R4971: |
| R2079: Isotonicity of set intersection |
| R88: Convolution is associative |
| R5059: Adjugate for a 2-by-2 real square matrix |
| R4151: Binary intersection is a lower bound to each set in the intersection |
| R3941: Slope function for standard real gaussian density function |
| R5299: Complex conjugate of a binary sum equals sum of complex conjugates |
| R270: Real arithmetic expression for sum of a finite real geometric sequence |
| R5127: Fundamental theorem of real trigonometry |
| R5322: Adding the same random real number need not preserve equality in distribution |
| R2441: Reflection invariance of Lebesgue outer measure |
| R1194: Indicator function with respect to set complement |
| R2754: Lipschitz map is Hölder continuous |
| R4913: Strong derivative for euclidean real quadratic form without translation |
| R3216: Characteristic function of an almost constant random real number |
| R4512: |
| R468: Lagrange's theorem |
| R4291: Vector space always has an inclusion-maximal linearly independent set |
| R2150: Expectation of conditional expectation for a random euclidean real number |
| R4568: Countable indicator partition of a random complex number |
| R4765: Reflection preserves euclidean real subset relation |
| R1371: Bilinear map is zero if either argument is zero |
| R80: Lipschitz map is continuous |
| R4583: |
| R5074: Determinant of a lower triangular complex matrix |
| R1073: Mean value theorem |
| R4826: Logarithm of a ratio |
| R5505: Cofactor matrix for a 2-by-2 real square matrix |
| R4855: Reflection property of standard logarithm function |
| R5568: Eigenvalue sequence for an identity complex matrix |
| R3602: Gaussian approximation to binomial distribution |
| R1160: Reflection invariance of Euclidean volume function |
| R590: Square root of two is irrational |
| R5160: Subconvex real function need not have a minimizer |
| R3559: Probability of random real number taking value in right-closed interval |
| R4825: Bit entropy of a standard bernoulli number is one bit |
| R5162: Minimizer need not be unique for a subconvex real function |
| R4832: Homomorphism property of standard logarithm function in the binary case |
| R3148: Sum of real telescoping series |
| R4263: Countable cartesian product with empty set is empty |
| R3869: Row-standardisation of row-independent random real standard triangular array |
| R5622: |
| R2440: Translation invariance of Lebesgue outer measure |
| R4596: Real calculus expression for moments of standard gaussian random real number |
| R4057: The set of boolean standard sequences is uncountable |
| R5631: Strong fundamental theorem of complex algebra for a quadratic complex polynomial |
| R5304: Complex-linearity of real expectation |
| R5336: Expectation of an indicator random boolean number |
| R4783: |
| R3670: Modulus sum upper bound to distance between two finite complex products for complex numbers in the unit disc |
| R3955: Components of standard gaussian random euclidean real number are standard gaussian random basic real numbers |
| R5232: Finite sum of independent gaussian random real numbers is a gaussian random real number |
| R3379: Product of irrational numbers is not necessarily irrational |
| R4838: Sum rule for simple marginal probability |
| R5183: Unique global maximizer for a finite product of unsigned real numbers with a given sum |
| R3969: Measure of intersection finite if measure of at least one set finite |
| R5185: Tight lower bound to a finite product of positive real numbers |
| R3626: Sample variance is a biased estimator for the variance of uncorrelated identically distributed random real numbers |
| R4895: Standard counting measure is a point-mass measure |
| R3401: Probability calculus expression for conditional expectation given disjoint non-null partition |
| R4107: Determinant of real diagonal matrix with constant diagonal |
| R4827: Entropy of a standard bernoulli number |
| R4148: Intersection is a lower bound to each set in the intersection |
| R4318: Inclusion-exclusion principle for unsigned basic measure of binary union |
| R4009: Metrisable topological space is Fréchet |
| R2929: Sum of odd functions is odd |
| R2641: Euclidean real martingale is constant in expectation |
| R4541: Open set is its own interior |
| R4567: Countable indicator partition of a random euclidean real number |
| R5677: Of all right triangles with a given perimeter, the isosceles triangle maximizes the area |
| R5420: Minimum and maximum of stopping times are stopping times for random real process |
| R708: Reverse triangle inequality for metric |
| R4310: Number of N-ary relations on a finite set |
| R4317: Inclusion-exclusion principle for unsigned basic measure of ternary union |
| R2060: Probability of set difference |
| R4841: Finite disjoint additivity of probability measure |
| R2746: Finite sets are closed in Fréchet space |
| R2262: Real variance partition into first and second moments |
| R5209: Of all rectangles with a given perimeter, the square maximizes the area |
| R4445: Inclusion-exclusion principle for probability of binary union |
| R5230: Bessel-corrected sample variance of I.I.D. gaussians is a transformed chi-squared random real number |
| R1165: Reflection invariance of Lebesgue measure |
| R4573: Complex expectation over a null event is zero |
| R4500: |
| R5363: A continuous random real number is almost surely an irrational number |
| R5115: Natural number factorial is an even number for numbers 2 or greater |
| R4330: Probability of finite intersection with an almost sure event |
| R5123: |
| R3385: Standard approximating sequence for the natural exponential function |
| R1159: Euclidean volume function under scaling |
| R4908: Strong derivative for affine euclidean real function |
| R1158: Translation invariance of Euclidean volume function |
| R2767: Identity map is an injection |
| R4391: Characteristic function uniquely identifies the distribution of a random euclidean real number |
| R5482: Columns of a real identity matrix span the whole space |
| R1083: Minimal element is minimum element in ordered set |
| R5282: Expectation of a random fraction need not equal fraction of expectations |
| R4829: Base inversion property of standard natural logarithm function |
| R347: Isotonicity of map image |
| R4167: Superset of binary union iff superset of both sets in the union |
| R3833: Uncorrelated random collection need not be independent |
| R4794: Independent minimums preserve exponential distribution |
| R1831: Real arithmetic expression for binomial coefficient |
| R2203: Expectation of a Poisson random natural number |
| R2876: Real mean value inequality |
| R2138: Translation invariance of unsigned basic Lebesgue integral |
| R5676: Variance of a squared standard gaussian real number |
| R2016: Probabilistic Markov's inequality |
| R2897: Fourier transform under scaling |
| R4737: |
| R4632: Cardinality of cartesian triple products is invariant under insertion of parentheses |
| R5518: Complex arithmetic expression for the determinant of a 2-by-2 complex square matrix |
| R5393: I.I.D. real empirical distribution measure converges to a probability for a fixed Borel set |
| R5300: Unsigned basic integral over an empty set equals zero |
| R4540: Inverse map is a bijection |
| R5376: Riemann integral of an exponential random positive real number density function |
| R4660: Real empirical probability distribution function converges pointwise to the true distribution function |
| R1074: Rolle's theorem |
| R4013: Polish space is Fréchet |
| R2091: Sequential continuity of probability measure from below |
| R1075: Basic real interior extremum theorem |
| R3531: Pointwise product with indicator function is lower bound for unsigned basic function |
| R4331: Probability of binary intersection with an almost sure event |
| R3215: Characteristic function of indicator random boolean number |
| R5576: Eigenvectors for a symmetric complex matrix are orthogonal |
| R4144: Finite union is an upper bound to each set in the union |
| R4038: Product of two finite real sums |
| R5519: Real arithmetic expression for the determinant of a 2-by-2 real square matrix |
| R5171: Real binomial theorem for exponent six |
| R2484: Moments of a Bernoulli random boolean number |
| R4455: |
| R4453: Probability of symmetric difference of event and subevent |
| R3568: Real AM-GM inequality |
| R5554: Real matrix trace is commutation invariant for two real matrices |
| R5297: Complex conjugate of a product of two complex numbers |
| R4687: Additivity of variance for a finite number of independent random real numbers |
| R4945: Real binomial theorem for exponent five |
| R4630: Bijection between parenthesis-sliced cartesian triple products |
| R3748: Finite real matrix is positive definite iff symmetric part is |
| R4831: Homomorphism property of standard logarithm function |
| R4609: |
| R4095: Real arithmetic expression for real arithmetic mean |
| R4871: Translation property of the standard real log-sum-exp function |
| R5081: Complex matrix determinant zero iff some nonzero vector is mapped to zero |
| R3384: Components of gaussian random euclidean real number are gaussian random basic real numbers |
| R5431: Growth class for the expectation of the absolute value of the standard integer random walk |
| R5404: I.I.D. real central limit theorem |
| R3461: Holomorphic function with vanishing derivative on complex domain is constant |
| R4649: Probability calculus expression for basic real conditional expectation given a countable partition of the sample space |
| R822: Group of prime order is cyclic |
| R4830: Change of base formula for logarithm function |
| R3583: Random basic number absolutisation equals sum of positive and negative parts |
| R4906: |
| R4846: Conditional simple entropy with respect to itself |
| R511: Natural number plane is countable |
| R4340: Bayes' theorem in the case of event and complement |
| R4961: |
| R5435: Expectation of a chi-squared random unsigned real number |
| R4467: Empty set is a stationary measurable set |
| R5104: Proof by principle of weak mathematical induction on the natural numbers |
| R5395: Factorization need not preserve equality in distribution |
| R4903: Strong derivative for affine basic real function |
| R5238: Sample mean of uncorrelated identically distributed gaussian random real numbers is a gaussian random real number |
| R2092: Sequential continuity of probability measure from above |
| R1846: Cardinality of set complement |
| R5091: Lindeberg central limit theorem for a standard triangular array |
| R4925: Probability calculus expression for conditional probability given disjoint non-null partition |
| R4171: Difference of set and countable union equals intersection of differences |
| R399: Injectivity is hereditary |
| R2621: Sum of binomial coefficients |
| R1851: Cardinality of set of permutations on finite set |
| R5172: Real binomial theorem for exponent seven |
| R4058: Boolean Cantor diagonal sequence is not a term in the sequence inducing it |
| R4473: Almost idempotency of conditional expectation of random complex number |
| R3205: Probability mass function for geometric random positive integer |
| R5190: Weighted Cauchy-Schwarz inequality for two real sequences |
| R3904: Characteristic function of a Poisson random natural number |
| R5174: Transpose of a product of two complex matrices |
| R5296: Complex conjugate of a product of two complex column matrices |
| R4309: Number of N-ary relations on a finite cartesian product |
| R3518: Partition of random basic number into positive and negative parts |
| R5537: Derivative function for euclidean real self-dot product function |
| R4469: Countable union of stationary measurable sets is stationary |
| R2343: Uncorrelated real weak law of large numbers |
| R4738: Finite subadditivity of probability measure |
| R3641: Conditional probability given independent random variable |
| R1864: Sum of Bell coefficients |
| R4290: Vector space always has a linearly independent subset |
| R2788: Real binomial theorem |
| R3513: Measurable subnull set has measure zero |
| R3582: Signed expectation finite iff absolutely integrable random basic number |
| R2093: Countable subadditivity of probability measure |
| R4186: Complement of a G-delta set is an F-sigma set |
| R5460: Sample variance is a biased estimator for the variance of I.I.D. random real numbers |
| R4370: Set of euclidean natural numbers has Lebesgue measure zero |
| R1564: Oriented complex curve integral of continuous function with a primitive on open set |
| R4781: Conditional expectation of known random real number |
| R5670: Pascal's rule in the upwards direction |
| R50: Set difference equals intersection with complement |
| R3201: Characteristic function of a binomial random natural number |
| R4285: Standard natural real exponential function maps zero to one |
| R5189: |
| R714: Element belongs to its own equivalence class |
| R2653: Real conditional expectation is absolutely integrable |
| R81: Bilipschitz map is continuous |
| R4912: Strong derivative for symmetric euclidean real quadratic form |
| R5647: Gibb's inequality for simple entropy |
| R4720: Conditional probability of complement event |
| R3939: Upper and lower bounds for codomain set of finite unsigned basic measure |
| R976: Finite disjoint additivity of unsigned basic measure |
| R4847: Probability of event conditional on itself |
| R4591: Binary additivity of transpose for real matrices |
| R755: Group centre is Abelian group |
| R4950: Real matrix with no real eigenvalues |
| R5526: Complex matrix determinant is homogeneous with respect to multiplying a row or a column by a constant |
| R3719: Probability of complement event |
| R4973: Bias-variance partition of mean square error for random basic real number |
| R4348: Two disjoint events are not necessarily independent |
| R678: Vector space of finite real matrices is isomorphic to a euclidean real vector space |
| R1170: Euclidean volume of singleton |
| R4662: Signed basic expectation with respect to a point probability measure |
| R4791: Probability for two independent standard Bernoulli random boolean numbers to coincide |
| R4341: Bayes' theorem in the case of two pullback events |
| R4638: Complex-linearity of complex matrix trace |
| R5210: Tight upper bound to a product of two unsigned real numbers |
| R2374: Borel-Cantelli zero-one law |
| R2757: Proper contraction map is continuous |
| R4733: Conditional expectation of known random euclidean real number |
| R221: Cartesian product is not associative |
| R4327: Probability of countable union with an almost sure event |
| R4369: Set of euclidean rational numbers has Lebesgue measure zero |
| R4011: Polish space is second-countable |
| R4537: Inclusion of inverse image does not imply inclusion of image |
| R4150: Finite intersection is a lower bound to each set in the intersection |
| R2071: Isotonicity of set union |
| R4857: Standard logarithm of a positive real number raised to an integer power |
| R4965: Relationship with the sum of initial natural numbers and the binomial coefficient |
| R3529: Tautological pointwise inequality from indicator functions on sublevel sets |
| R4743: Riemann integral average of vanishing unsigned basic real function vanishes |
| R4049: Number of binary relations on a finite set |
| R5141: Real log-sum-exp method |
| R4534: |
| R3380: Sum of rational and irrational number is irrational |
| R352: Inverse image of image |
| R3783: Law of total probability for complex expectation in terms of pullback events |
| R4485: Convergent sequence in metric space has unique limit point |
| R4693: Lower bound to the product of duals of a finite collection of real numbers in the left-closed unit interval |
| R2928: Finite sum of even euclidean real functions is even |
| R3649: Expectation of conditional probability |
| R2338: Finite sum of I.I.D. exponential random positive real numbers is a gamma random random positive real number |
| R4012: Polish space is Hausdorff |
| R3844: Characteristic function of a scaled random real number |
| R4543: Map inverse is invertible |
| R5126: Fundamental theorem of complex trigonometry |
| R4273: Absolute value function preserves zero |
| R4866: Generating a random real number with randomness from a standard uniform variable |
| R2764: Canonical singleton map is bijection |
| R5558: Characteristic polynomial for a complex diagonal matrix of constant diagonal |
| R2934: Isotonicity of unsigned basic real series |
| R5303: Real-linearity of complex expectation |
| R1557: Weighted real AM-GM inequality |
| R2690: Minimum and maximum of stopping times are stopping times |
| R3532: Tautological pointwise lower bound from indicator function on sublevel set |
| R2239: Expectation of exponential random positive real number |
| R3493: Empirical distribution function converges in probability to the true distribution function |
| R2525: Independence of sigma-algebras is hereditary |
| R4597: Centred gaussian real density function is an even function |
| R2436: Polar representation of complex conjugate |
| R4563: Complex integral over a set of measure zero is zero |
| R7: Empty set is subset of every set |
| R4982: Exchangeable random collection is identically distributed |
| R262: Countable union of countable sets is countable |
| R4315: Cardinality of a finite set raised to a finite power |
| R1149: Every point in open set is an interior point |
| R5046: Absolute moment inherits finiteness from greater exponents for random real number |
| R5068: Determinant of a scaled complex matrix |
| R4788: |
| R4157: Superadditivity of power set |
| R3972: Expression for random basic real sum of squares in terms of sample mean and variance |
| R4902: Strong derivative for constant real function |
| R1401: Orthogonality relation is a symmetric binary relation |
| R5144: Vanishing gradient identifies a minimizer for differentiable subconvex real function |
| R5563: Eigenvalue sequence for a triangular complex matrix |
| R4172: Difference of set and finite union equals intersection of differences |
| R5510: Real square matrix which has a zero column or a zero row has determinant zero |
| R5323: Conditional expectation need not preserve equality in distribution |
| R4659: Empirical probability distribution function is an unbiased estimator of the true distribution function |
| R5283: Expectation of a standard bernoulli random boolean number |
| R3618: Turning two unsigned real numbers into convex combination coefficients |
| R4513: |
| R2747: Finite sets are closed in Hausdorff space |
| R5531: Eigenvalue sequence exists for every complex square matrix |
| R244: Convergent sequence is Cauchy |
| R5243: Finite sum of uncorrelated identically distributed exponential random positive real numbers is a gamma random random positive real number |
| R5614: |
| R4673: Napier's constant equals a limit of products with factors nearing one |
| R4739: Binary subadditivity of probability measure |
| R1370: Multilinear map is zero if any argument is zero |
| R1544: Anova partition of orthogonal projection |
| R975: Isotonicity of unsigned basic measure |
| R4349: Two disjoint events independent iff one is of probability zero |
| R2802: Expectation of the absolute value of a centred gaussian random real number |
| R1077: Maximum element is unique |
| R1120: Antitonicity of minimum |
| R2295: Unit increment property of the gamma function |
| R4755: Inverse image of a reflected real set |
| R2062: Antitonicity of subtracting from the same set |
| R5197: Characterisation of natural real exponential function by a differential equation |
| R2959: Function even part is even |
| R1841: Indicator function operator is a bijection |
| R4944: Real binomial theorem for exponent four |
| R3060: Riemann integral of even real function over an interval symmetric abour zero |
| R5656: Real poisson process is increasing |
| R4143: Countable union is an upper bound to each set in the union |
| R4182: Isotonicity of sublevel probabilities for a random real number |
| R1276: Every map from discrete topological space is continuous |
| R4073: Probability of union with the impossible event |
| R5266: Real calculus expression for distribution function of standard exponential random positive real number |
| R5471: Real square matrix invertible iff transpose is |
| R3770: Product of real 2-by-2 matrix with its transpose |
| R5182: Tight upper bound to a finite product of unsigned real numbers |
| R5229: Bessel-corrected sample variance of independent standard gaussians is a transformed chi-squared random real number |
| R246: Cauchy sequence is bounded |
| R517: Singletons are closed in Hausdorff space |
| R4611: |
| R4560: Probability of complement of a null event |
| R3745: Real square matrix antisymmetric part is zero definite |
| R4173: Difference of set and binary union equals intersection of differences |
| R49: Isotonicity of subtracting same set |
| R5566: Eigenvalue sequence for a diagonal complex matrix |
| R4909: Derivative for euclidean real self-dot product function |
| R4443: Measure of symmetric difference of set and subset |
| R4666: Real GM-HM inequality |
| R978: Measure of set difference |
| R2964: Even function equals its even part |
| R5192: Cauchy-Schwarz inequality for two real sequences |
| R1275: Every map to trivial topological space is continuous |
| R2141: Reflection invariance of unsigned basic Lebesgue integral |
| R4898: |
| R4559: Probability of complement of an almost sure event |
| R4916: |
| R3232: Value of standard logarithm function at its parameter value |
| R4684: I.I.D. weak law of large numbers for random real numbers |
| R4166: Superset of finite union iff superset of every set in the union |
| R5242: Finite sum of uncorrelated identically distributed Poisson random natural numbers is Poisson |
| R2786: Complement property of binomial coefficient |
| R4188: Set cardinality in terms of finite ambient set |
| R1369: Jensen's inequality for expectation |
| R3316: Pointwise limit of continuous functions need not be continuous |
| R5211: Tight upper bound to a product of three unsigned real numbers |
| R5063: Cofactor partition for the determinant of a real square matrix |
| R1012: Monotonicity of real limits |
| R5567: Eigenvalue sequence for a diagonal complex matrix with constant diagonal |
| R4214: Finite set union is invariant under bijective shifting of indices |
| R3259: Weak law of large numbers for variance with weighted decay |
| R4928: Finite partition additivity of probability measure |
| R4550: |
| R403: Square of the imaginary number |
| R5241: Finite sum of I.I.D. Poisson random natural numbers is Poisson |
| R4873: |
| R4106: Determinant of real diagonal matrix |
| R3945: Set is a superset to its interior |
| R3885: Gaussian approximation to Poisson distribution |
| R5569: Determinant of reflected complex matrix |
| R1233: Finite additivity of unsigned basic integral |
| R1959: Young's inequality |
| R5061: Expression for a real matrix inverse in terms of adjugate |
| R2089: Unsigned basic expectation is compatible with probability measure |
| R2182: Isotonicity of real sublevel sets |
| R2377: Almost sure convergence implies convergence in probability |
| R3544: Endpoint bounds for real arithmetic mean |
| R3535: Riemann integral of unit semicircle |
| R4670: Real geometric mean is a right limit of basic real power means |
| R2787: Pascal's rule |
| R5399: Sample average of I.I.D. integrable random real numbers converges to expectation almost surely |
| R3587: Random basic number almost surely finite iff positive and negative parts are |
| R2933: Isotonicity of countably infinite real summation |
| R4595: Basic real calculus expression for moments of centred gaussian random basic real number |
| R4374: Integral factorisation on a binary product of basic real lebesgue measure spaces |
| R4844: Mutual information of a simple random variable with respect to itself |
| R3545: Endpoint bounds for real convex combination |
| R5194: |
| R4901: Probability density function for standard exponential random positive real number |
| R1973: Map composition is associative |
| R4756: |
| R4126: Almost surely bounded random complex number has all absolute moments finite |
| R5079: Characterisation of complex matrix eigenvalues in terms of characteristic polynomial |
| R3589: Random basic number almost surely finite if first absolute moment is finite |
| R5424: |
| R3757: Linearity of basic real matrix trace |
| R4947: Variance of standard Bernoulli random boolean number |
| R2491: Pairwise independent event collection need not be independent |
| R3404: Bayes' theorem in the case of two events |
| R2960: Function odd part is odd |
| R4997: |
| R5564: Eigenvalue sequence for an upper triangular complex matrix |
| R4962: Characteristic polynomial for a complex identity matrix |
