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