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