R463 Law of the excluded middle is a propositional tautology
R4962 Characteristic polynomial for a complex identity matrix
R4292 Finite cartesian product of finite sets is finite
R4931
R5183 Unique global maximizer for a finite product of unsigned real numbers with a given sum
R5632 Derivative function for a real matrix quadratic form
R5070 Determinant of a diagonal complex matrix with constant diagonal
R1022 Partition of basic function into positive and negative parts
R4086 Real arithmetic expressions for AND boolean logic gate
R5175 Derivative function for standard natural real logarithm function
R3201 Characteristic function of a binomial random natural number
R2082 Binary set union with empty set
R4206 Basic real golden ratio is a root of a quadratic basic real polynomial
R5099 Sum of initial cubed natural numbers
R3547 Expectation minimises second central moment for random real number
R4675 Standard real logarithm function grows linearly near 1
R4467 Empty set is a stationary measurable set
R176 Canonical set epimorphism is surjection
R4672 First-degree polynomial approximation for a standard natural basic real exponential function near zero
R2966 Indicator function under scaling of the argument
R2505 Real covariance partition into first moments
R2093 Countable subadditivity of probability measure
R5483 Columns of a real matrix span the whole space if real-linearly independent
R4611
R5094 Number of boolean functions on a boolean cartesian product
R3626 Sample variance is an unbiased estimator for the variance of uncorrelated identically distributed random real numbers
R978 Measure of set difference
R5260 Slope function for standard natural real logarithm function
R2811 Distance between expectation and median of a random real number is no more than one standard deviation
R3507 Binary union of countable sets is countable
R4657 Probability calculus expression for conditional probability given a finite partition of the sample space
R4271 Absolute value function is not strictly isotone
R4825 Bit entropy of a standard bernoulli number is one bit
R5366 The standard Cantor set is standard Borel
R5261 Slope function for standard real sine function
R2751 Fourier transform of absolutely integrable function is bounded
R2221 Set intersection is invariant under bijective shifting of indices
R1162 Lebesgue sigma-algebra is closed under reflections
R4929 Binary partition additivity of probability measure
R3232 Value of standard logarithm function at its parameter value
R5299 Complex conjugate of a binary sum equals sum of complex conjugates
R3921 Identically distributed random collection need not be stationary
R447 Zorn's lemma
R4788
R3401 Probability calculus expression for conditional expectation given disjoint non-null partition
R5136 Minimax inequality
R5465 Known random complex number behaves like a constant in conditional expectation
R5438 Chi random unsigned real number coincides in distribution with euclidean length of a standard multivariate gaussian
R3512 Unsigned basic integral over set of measure zero is zero
R3518 Partition of random basic number into positive and negative parts
R3058 Integer powers of the imaginary number
R4688 Second moment upper bound to real variance
R3432 Standard I.I.D. law of the iterated logarithm
R5188
R24 Parallelogram identity
R4270 Set union with empty set
R4596 Real calculus expression for moments of standard gaussian random real number
R4676
R5104 Proof by principle of weak mathematical induction on the natural numbers
R477 Set finiteness is hereditary
R5289 Real arithmetic expression for the value of geometric mean of a telescroping fintie real sequence
R4150 Finite intersection is a lower bound to each set in the intersection
R4776 Hoeffding's lemma
R2370 Real arithmetic expression for cardinality of countable set
R4007 Singletons are closed in Polish space
R2960 Function odd part is odd
R1818 Isotonicity of real expectation
R2074 Isotonicity of inverse image
R4010 Polish space is first-countable
R2744 Square root of prime is irrational
R4323
R1202 Dominated convergence theorem for signed basic integral
R5484 Columns of a real matrix which span the whole space need not be real-linearly independent
R2343 Uncorrelated real weak law of large numbers
R4332
R5174 Transpose of a product of two complex matrices
R4485 Convergent sequence in metric space has unique limit point
R1164 Translation invariance of Lebesgue measure
R2754 Lipschitz map is Hölder continuous
R2466 Real matrix determinant is multiplicative
R1502 Complex-linearity of complex integral
R2313 Expectation with dual probability distribution function
R4804 Probability distribution function for geometric random positive integer
R432 Set of natural numbers is countable
R5189
R4500
R4260 Real square root function is strictly isotone
R5447 Growth rate of the expectation of the absolute value of a standard real Wiener process
R4141 Probabilistic Chernoff inequality
R4263 Countable cartesian product with empty set is empty
R4174 Proper contraction has at most a single fixed point
R2929 Sum of odd functions is odd
R4845 Joint entropy formula for simple mutual information
R5591 Real matrix gramians are positive semidefinite
R4283 Standard natural basic real logarithm function escapes to positive infinity at positive infinity
R1530 Inverse image preserves set difference
R1149 Every point in open set is an interior point
R4172 Difference of set and finite union equals intersection of differences
R4013 Polish space is Fréchet
R4732
R4659 Empirical probability distribution function is an unbiased estimator of the true distribution function
R399 Injectivity is hereditary
R1089 Characterisation of convergent sequences in metric space
R2441 Reflection invariance of Lebesgue outer measure
R4087 Real arithmetic expressions for OR boolean logic gate
R4900
R4972 Bias-variance partition of mean square error for a random real column matrix
R5086 Eigenvectors for a symmetric real matrix are orthogonal
R5412
R4151 Binary intersection is a lower bound to each set in the intersection
R4638 Complex-linearity of complex matrix trace
R5517 Cofactor partition for a complex square matrix
R4314 Number of boolean functions on a finite set
R2677 Law of total probability for a countable partition of events of positive probability
R4443 Measure of symmetric difference of set and subset
R1869 Characterisation of equality of maps
R4945 Real binomial theorem for exponent five
R4348 Two disjoint events are not necessarily independent
R3517 Unsigned basic expectation zero iff random number almost surely zero
R4847 Probability of event conditional on itself
R3944 Open set iff equal to interior
R5068 Determinant of a scaled complex matrix
R219 Difference of set and intersection equals union of differences
R5621
R5081 Complex matrix determinant zero iff some nonzero vector is mapped to zero
R2367 Law of total variance
R3192 I.I.D. sequence of standard gaussian random real numbers is standard gaussian random euclidean real number
R4670 Real geometric mean is a right limit of basic real power means
R3833 Uncorrelated random collection need not be independent
R2067 Subtracting empty set from set
R5424
R3195 Components of Gaussian random Euclidean number are independent iff uncorrelated
R2485 Expectation of geometric random basic positive integer
R4702
R4349 Two disjoint events independent iff one is of probability zero
R4163 Subset of binary intersection iff subset of both sets in the intersection
R1856 Cardinality of the set of maps between finite sets
R1232 Tonelli's theorem for sums and integrals
R4265 Finite set intersection with empty set is empty
R1564 Oriented complex curve integral of continuous function with a primitive on open set
R76 Empty set is closed
R2091 Sequential continuity of probability measure from below
R4060 Appropriately parenthesised cartesian products are isomorphic
R4567 Countable indicator partition of a random euclidean real number
R4920 Measurable transformation preserves independent finite random collection
R4131 Markov lower bound on unsigned basic expectation
R5524 Complex arithmetic expression for the determinant of a 3-by-3 complex square matrix
R4704
R4049 Number of binary relations on a finite set
R4287 Finite product of even complex functions is even
R3969 Measure of intersection finite if measure of at least one set finite
R5301 Random unsigned basic number has zero correlation with the empty indicator
R4591 Binary additivity of transpose for real matrices
R4538 Inclusion of image does not imply inclusion of inverse image
R2955 Reciprocal positive integer sequence converges to zero
R4899
R2295 Unit increment property of the gamma function
R1214 Isotonicity of unsigned basic integral
R4317 Inclusion-exclusion principle for unsigned basic measure of ternary union
R2014 Triangle inequality for signed basic integral
R3605 Subadditivity of basic real square root function
R4079 Modus tollendo ponens in propositional logic
R4463 Strongly mixing probability-preserving system is weakly mixing
R1650 Interior point of set iff has open neighbourhood contained in set
R3471 Open complex mapping theorem
R4444 Superset differenced from set equals empty set
R4836 Change of base formula for simple entropy
R797 Principle of weak mathematical induction on the natural numbers
R4559 Probability of complement of an almost sure event
R2407 Measurable transformation preserves independence
R4473 Almost idempotency of conditional expectation of random complex number
R4058 Boolean Cantor diagonal sequence is not a term in the sequence inducing it
R5448 Expectation of the absolute value of a standard real wiener process at a given point
R5074 Determinant of a lower triangular complex matrix
R5529 Complex matrix determinant is additive with respect to row or column addition
R5534 Complex matrix invertible iff every eigenvalue nonzero
R5570 Special coefficients of complex matrix characteristic polynomial
R5166 Series converges for real numbers in the left-closed unit interval iff infinite product of duals does not vanish
R4338 Conditional probability of almost surely true event
R4610
R3633 Bessel-corrected sample variance is an unbiased estimator for the variance of uncorrelated identically distributed random real numbers
R1160 Reflection invariance of Euclidean volume function
R5233 Finite sum of I.I.D. gaussian random real numbers is a gaussian random real number
R5186 Unique global minimizer for a finite product of positive real numbers with a given sum of multiplicative inverses
R1406 Collection of sets ordered by inclusion contains a maximal element
R3304 Approximating sequence for the natural exponential function
R4714 Sufficient condition for the existence of density function for a random euclidean real number
R4601 Element in countable cartesian product iff components in images of canonical projections
R3500 Homomorphism property of the standard natural real exponential function
R5442 Variance of a standard gaussian random real number
R3508 Fermat's last theorem
R4694
R4167 Superset of binary union iff superset of both sets in the union
R3416 Absolute value bounds for a basic real number
R3863 Signed basic integral with respect to a point measure
R4902 Strong derivative for constant real function
R4782 Expectation of conditional expectation for a random real number
R1070 Extreme value theorem for basic real calculus
R3516 Signed basic expectation of almost surely zero random number is zero
R5045 Real matrix multiplied by column matrix from the right
R3844 Characteristic function of a scaled random real number
R4285 Standard natural real exponential function maps zero to one
R4669 Diagonalizable complex matrix is symmetric
R4308 Map composition need not be commutative
R4829 Base inversion property of standard natural logarithm function
R1076 Minimum element is unique
R2745 The only subset of finite set with same cardinality is the ambient set itself
R4173 Difference of set and binary union equals intersection of differences
R2168 Isotonicity of Lebesgue outer measure
R5124 Modulus of complex number polar representation
R5302 Idempotence of complex expectation
R3514 Unsigned basic expectation over set of probability zero is zero
R5135 Derivative of the two-dimensional softmax function
R2802 Expectation of the absolute value of a centred gaussian random real number
R3582 Signed expectation finite iff absolutely integrable random basic number
R4873
R4211 Basic real golden ratio is limit of successive terms in the Fibonacci natural number sequence
R5498 Inverse matrix is unique for real square matrix
R4171 Difference of set and countable union equals intersection of differences
R1577 Cauchy's theorem for a disc
R464 Ex falso sequitur quodlibet
R2092 Sequential continuity of probability measure from above
R1213 Linearity of unsigned basic integral
R3719 Probability of complement event
R5193 Maximal value for a directional derivative at a point
R4168 Difference of set and countable intersection equals union of differences
R4325 Probability one if conditional probability one relative to event of probability one
R3908 Characteristic function of almost surely constant random euclidean real number
R4580 Empty set union equals the empty set
R4289 Vector space always has a basis
R3649 Expectation of conditional probability
R2223 Binary set union is commutative
R3204 Characteristic function of geometric random positive integer
R5242 Finite sum of uncorrelated identically distributed Poisson random natural numbers is Poisson
R5460 Sample variance is an unbiased estimator for the variance of I.I.D. random real numbers
R3429 Complex conjugation is a multiplicative operation
R4602 Element in finite cartesian product iff components in images of canonical projections
R5180 Tight upper bound to directional derivative
R4834
R1236 Markov's inequality
R3325 Banach fixed point theorem
R1372 Inner product is zero if either argument is zero
R5590 Complex matrix gramians are positive semidefinite
R2741 Set equality iff inclusion in both directions
R5409 Expectation of the absolute value of a centred standard gaussian random real number
R2060 Probability of set difference
R3869 Row-standardisation of row-independent random real standard triangular array
R4626 Strict isotonicity of basic Riemann integral
R3601 Gaussian approximation to standard Poisson distribution
R831 Second group isomorphism theorem
R3462 Goursat's theorem for circles
R4495 Superconvex and superconvex basic real functions on open basic real interval are continuous
R5176 Cauchy-schwarz inequality for real pairs
R5319 Conditional probabilities need not preserve equality in probability
R3774 Probability distribution function for exponential random positive real number
R5063 Cofactor partition for the determinant of a real square matrix
R4264 Cartesian product with empty set is empty
R1903 Basic integral of almost everywhere zero function is zero
R4268 Finite set union with empty set
R4674
R5185 Tight lower bound to a finite product of positive real numbers
R3885 Gaussian approximation to Poisson distribution
R5474 Complex square matrix invertible iff conjugate transpose is
R5080 Complex matrix determinant nonzero iff kernel is trivial
R4930
R4266 Countable set intersection with empty set is empty
R2786 Complement property of binomial coefficient
R4800 Number of injections from a finite set to itself
R3404 Bayes' theorem in the case of two events
R221 Cartesian product is not associative
R3778 Probability density function for exponential random positive real number
R5091 Lindeberg central limit theorem for a standard triangular array
R1906 Isotonicity of limits of real sequences
R4309 Number of N-ary relations on a finite cartesian product
R5595 Positive definite complex square matrix is conjugate symmetric
R1975 Measure of set in backward orbit under measure-preserving endomorphism
R716 Equivalence class is not empty
R5075 Complex matrix determinant is multiplicative
R4621 Standard mollifier is an approximate identity for complex Lebesgue convolution
R3586 Basic function is finite almost everywhere iff positive and negative parts are
R3166 Fourier transform of absolutely integrable function vanishes at infinity
R4925 Probability calculus expression for conditional probability given disjoint non-null partition
R3262 Dilations of unsigned tail probability converge to zero
R4169 Difference of set and finite intersection equals union of differences
R4113 Strong fundamental theorem of real algebra
R237 Intersection distributes over union
R90 Complex function convolution is homogeneous to degree one
R2539 Probabilistic Chebyshov's inequality
R5142 Subconvex real function iff first-order Taylor approximates underestimates function globally
R5201 Real arithmetic expression for the value of a telescoping finite real product
R4667 Real function which is differentiable only at a single point
R3971 Intersection of sets of infinite measure need not have infinite measure
R4887 Cardinality of binary cartesian product of finite sets
R1603 De Moivre's theorem
R4687 Additivity of variance for a finite number of independent random real numbers
R2747 Finite sets are closed in Hausdorff space
R4598 Standard gaussian real density function is an even function
R3504 Erdős discrepancy problem
R4486 Metric space is Hausdorff
R4089 Real arithmetic expressions for NAND boolean logic gate
R1817 Complex-linearity of complex expectation
R678 Vector space of finite real matrices is isomorphic to a euclidean real vector space
R4503 Countable union of sets of measure zero is of measure zero
R1204 Fatou's lemma for unsigned basic integral
R2963 Odd function equals its odd part
R4770 Inclusion-exclusion lower bound to probability of binary intersection
R4374 Integral factorisation on a binary product of basic real lebesgue measure spaces
R3479 Conformal complex function iff holomorphic bijection
R2681 Weak fundamental theorem of complex algebra
R4148 Intersection is a lower bound to each set in the intersection
R5577 Complex matrix eigenvectors corresponding to distinct eigenvalues are linearly independent
R4743 Riemann integral average of vanishing unsigned basic real function vanishes
R5323 Conditional expectation need not preserve equality in distribution
R5405 Standard I.I.D. real central limit theorem
R4340 Bayes' theorem in the case of event and complement
R3789 Absolute value strictly less than real number iff in symmetric open interval
R4663 Real square root function is superconvex
R4876 Interval length upper bound to variance of bounded random real number
R1841 Indicator function operator is a bijection
R4965 Relationship with the sum of initial natural numbers and the binomial coefficient
R5433 Variance of the standard integer random walk after a given number of steps
R5207 Basel approximating sequence to Pi
R355 Inverse image of singleton set
R5066 Inverse of symmetric complex matrix is symmetric
R5049
R3531 Pointwise product with indicator function is lower bound for unsigned basic function
R3412 Euclidean real arithmetic mean minimises Euclidean distance
R2491 Pairwise independent event collection need not be independent
R893 Cyclic group is Abelian
R5291 Complex conjugate of a complex eigenvalue of a real matrix is an eigenvalue
R4971
R3832 Mode maximizes expected number of correct guesses for a finite identically distributed sequence of discrete random real numbers
R125 Subset relation is reflexive
R4618 Riemann integral of standard basic real gaussian function on the real line
R2150 Expectation of conditional expectation for a random euclidean real number
R5566 Eigenvalue sequence for a diagonal complex matrix
R4159 Power set is not empty
R4684 I.I.D. weak law of large numbers for random real numbers
R1077 Maximum element is unique
R5509 Cofactor partition for the determinant of a 3-by-3 real square matrix
R5306 Conditional expectation of a random complex matrix given minimal information
R3559 Probability of random real number taking value in right-closed interval
R88 Convolution is associative
R2138 Translation invariance of unsigned basic Lebesgue integral
R982 Sequential continuity of measure from below
R3562 Real conditional variance partition into conditional moments
R2261 Variance of a Poisson random natural number
R4456
R3685 Modulus sum upper bound to distance between two finite complex products
R4543 Map inverse is invertible
R3652 Cramér-Wold theorem
R4903 Strong derivative for affine basic real function
R25 Cauchy-Schwarz inequality
R3384 Components of gaussian random euclidean real number are gaussian random basic real numbers
R4866 Generating a random real number with randomness from a standard uniform variable
R5545 Trace of conjugate transpose equals conjugate of trace
R4310 Number of N-ary relations on a finite set
R4293 Power set of a finite set is finite
R4916
R3748 Finite real matrix is positive definite iff symmetric part is
R4511 Two complex numbers distinct iff difference distinct from zero
R4583
R2100 Triangle inequality for signed basic expectation
R2089 Unsigned basic expectation is compatible with probability measure
R5514 Determinant of a complex identity matrix
R4909 Derivative for euclidean real self-dot product function
R5050 Derivative for real matrix function quadratic form
R5008 Random unsigned basic number almost surely finite if expectation is finite
R2950 Complex conjugation operation is an involution
R4747
R5508 Real square matrix invertible iff determinant nonzero
R4139 Mill's inequalities
R3953 Two almost surely equal random real numbers are identically distributed
R3506 Finite union of countable sets is countable
R2799 Variance of an indicator random boolean number
R560 Division theorem in the ring of basic integers
R5255 Slope function for pointwise product of two differentiable real functions
R26 Pythagorean theorem
R2690 Minimum and maximum of stopping times are stopping times
R468 Lagrange's theorem
R1450 Explicit algebraic expression for elements of generated subgroup
R4125 Two random real numbers identical in distribution have identical absolute moments
R1487 Ring is a subring of itself
R4383 Euclidean real Fourier transform is uniformly bounded
R4998 Limit of distribution function of geometric random positive integer scaled by reciprocal of index
R5500 Transpose of real matrix inverse is inverse to the transpose
R5563 Eigenvalue sequence for a triangular complex matrix
R370 Countable set iff surjection from natural numbers
R5369 Shannon entropy of a geometric random positive integer
R4042 Rearrangement inequality for finite real summation
R5378 Distribution of the standard real Wiener process at a given point is gaussian
R5085 Eigenvalues of a symmetric real matrix are real-valued
R5636 Derivative function for a real matrix trace function
R5259 Slope function for pointwise sum of two differentiable real functions
R5561 Characteristic polynomial for an upper triangular complex matrix
R5564 Eigenvalue sequence for an upper triangular complex matrix
R517 Singletons are closed in Hausdorff space
R4692 Series diverges for real numbers in the left-closed unit interval iff infinite product of duals vanishes
R2164 Law of the excluded middle in probability calculus
R2589 Trivial factorial upper bound
R4550
R5562 Characteristic polynomial for a lower triangular complex matrix
R3568 Real AM-GM inequality
R3935 Superset iff equal to union with subset
R5362 Probability that a continuous random real number takes value in the rational numbers is zero
R4092 Real arithmetic expression for real harmonic mean
R263 Binary cartesian product of countable sets is countable
R5416
R3738 Median need not be unique for a random real number
R4801 Probability mass function for cogeometric random basic natural number
R2422 Complex-linearity of Fourier transform
R4754
R4118 Real arithmetic expression for unsigned real geometric mean
R2224 Set union is associative
R5552 Complex matrix trace is commutation invariant for two complex matrices
R249 Cauchy-Schwarz inequality for finite real sequences
R5575 Traces of complex matrix gramians coincide
R2411 Characteristic function of exponential random positive real number
R1514 Isotonicity of signed basic integral
R4540 Inverse map is a bijection
R4228 Real ordering is compatible with addition
R5060 Product of a real square matrix and its adjugate is a constant diagonal matrix
R981 Countably infinite measurable cover has measurable subcover
R3923 Standard gaussian random real number is symmetric about zero
R2353 Volume of an open ball in Euclidean space
R220 Difference of set and union equals intersection of differences
R2732 Kolmogorov zero-one law
R2740 Splitting a Riemann integral over an implicit interval partition
R4764
R4919 Measurable transformation preserves independent countable random collection
R4991 Complex matrix multiplied from the right by a diagonal matrix
R5254 Slope function for standard natural real exponential function
R5459 Sample mean of identically distributed random real numbers is an unbiased estimator for expectation
R3676 Characteristic function for sum of independent random euclidean real numbers
R2788 Real binomial theorem
R4290 Vector space always has a linearly independent subset
R5262 Slope function for standard real cosine function
R5363 A continuous random real number is almost surely an irrational number
R4701
R5497 Inverse matrix is unique for complex square matrix
R4277 Measure of measurable set complement
R2750 Fourier transform of finite unsigned euclidean real Borel measure is uniformly bounded
R5272 Reciprocal real function on on the positive reals is antitone
R4703
R4262 Finite cartesian product with empty set is empty
R2588 Weak Stirling formula
R2656 De Moivre-Laplace theorem
R5431 Growth class for the expectation of the absolute value of the standard integer random walk
R4808 Affine transformations preserve independent real pairs
R4604 Density partition for natural number moment of a random real number
R4039 Product of two finite real sums with equal number of summands
R4368 Set of euclidean integers has Lebesgue measure zero
R1275 Every map to trivial topological space is continuous
R2757 Proper contraction map is continuous
R1012 Monotonicity of real limits
R4817 Data processing inequality for transformed endpoint
R5525 Complex square matrix which has a zero column or a zero row has determinant zero
R5197 Characterisation of natural real exponential function by a differential equation
R2986 Lebesgue outer measure under scaling
R1744 Finite union of finite sets is finite
R3747 Transpose of finite product of real matrices
R4827 Entropy of a standard bernoulli number
R2535 Chebyshov's inequality
R1566 Mean value theorem for Riemann integral
R3988 Expression for quadratic form of real square matrix in terms of symmetric part
R4509 Two real numbers distinct iff difference distinct from zero
R2158 Conditional expectation given independent sigma-algebra
R5231 Sample mean of uncorrelated gaussian random real numbers is a gaussian random real number
R4737
R4926 Finite partition additivity of unsigned basic measure
R4090 Real arithmetic expressions for XOR boolean logic gate
R4698 Unsigned basic integral with respect to a point measure
R3206 Probability mass function for binomial random natural number
R5594 Positive definite real matrix need not be symmetric
R2615 Empty set is cofinite within a finite set
R2062 Antitonicity of subtracting from the same set
R4729 Complex binomial inequality
R5284 Expectation of a Bernoulli random boolean number
R246 Cauchy sequence is bounded
R1959 Young's inequality
R5139 Expectation preserves random real number stochastic ordering relation
R5009 Bernoulli random boolean integer from a uniform random real number
R5507 Real square matrix invertible iff determinant is
R1074 Rolle's theorem
R5147 Reflection of standard natural real logarithm function is subconvex
R4843 Conditional entropy formula for simple mutual information
R3424 Complex exponential function preserves complex conjugation
R5419 Wald's first equation
R4275 Absolute value function is an even basic real function
R2080 Union is upper bound for intersection
R5340 Mean-median-mode inequality for a gaussian random real number
R4849 Symmetry of simple mutual information
R425 Euler's formulas for a real variable
R4369 Set of euclidean rational numbers has Lebesgue measure zero
R5245 Euclidean real number is zero iff equal to its reflection
R4997
R4502 Difference of almost everywhere equal euclidean complex functions is almost everywhere zero
R4755 Inverse image of a reflected real set
R5585 Invertible complex matrix need not be diagonalizable
R4328 Probability of finite union with an almost sure event
R1170 Euclidean volume of singleton
R1276 Every map from discrete topological space is continuous
R3385 Standard approximating sequence for the natural exponential function
R4693 Lower bound to the product of duals of a finite collection of real numbers in the left-closed unit interval
R4088 Peirce basic boolean logic gate iff complement of maximum function on basic boolean ordered pairs
R4875 Popoviciu's inequality
R3904 Characteristic function of a Poisson random natural number
R3231 Riemann integral analogue to infinite geometric series
R3954 Two almost surely equal random variables are identically distributed
R4162 Subset of finite intersection iff subset of every set in the intersection
R4329 Probability of countable intersection with an almost sure event
R3598 Wald's first equation under independence
R4562 Basic integral over a set of measure zero is zero
R648 Proportionally bounded linear map is Lipschitz
R4091 Biconditional boolean logic gate iff complement of trivial distance function on basic boolean ordered pairs
R5126 Fundamental theorem of complex trigonometry
R1159 Euclidean volume function under scaling
R3529 Tautological pointwise inequality from indicator functions on sublevel sets
R3984 Subcollection of independent random collection is independent
R4796 Probability for two independent exponential random positive real numbers to be smaller than the other
R3032 Set of real numbers is uncountable
R4774
R1178 Continuous map is Borel measurable
R4673 Napier's constant equals a limit of products with factors nearing one
R2016 Probabilistic Markov's inequality
R4615 Sufficient conditions to qualify as an approximate identity to complex Lebesgue convolution
R4370 Set of euclidean natural numbers has Lebesgue measure zero
R3843 I.I.D. real central limit theorem with the identity index sequence
R1488 Group is a subgroup of itself
R4142 Union is an upper bound to each set in the union
R2464 Determinant is preserved under transpose of complex matrix
R4627
R4466 Whole space is a stationary measurable set
R3783 Law of total probability for complex expectation in terms of pullback events
R1904 Isotonicity of finite real summation
R2270 Sigma-algebra is closed under symmetric differences
R5256 Slope function for composition of two differentiable real functions
R5614
R3645 Countable partition additivity of unsigned basic measure
R5357 An uncountable set can have Lebesgue measure zero
R4637
R4170 Difference of set and binary intersection equals union of differences
R2653 Real conditional expectation is absolutely integrable
R2641 Euclidean real martingale is constant in expectation
R4606 Stieltjes integral calculus expression for natural number moment of a random real number
R3695 Standardised Lindeberg central limit theorem
R2337 Density function for binary sum of independent random basic real numbers
R2954 Standard real harmonic series diverges
R2975 Lebesgue sigma-algebra is closed under reflections, translations, and scaling
R4908 Strong derivative for affine euclidean real function
R112 Cavalieri principle
R3494 Glivenko-Cantelli theorem
R5273 Finiteness of expectation in general does not imply finiteness of variance for random real number
R3215 Characteristic function of indicator random boolean number
R5190 Weighted Cauchy-Schwarz inequality for two real sequences
R5296 Complex conjugate of a product of two complex column matrices
R49 Isotonicity of subtracting same set
R4320 Set of singletons is subset of power set
R5329 Real arithmetic expression for ReLU function in terms of the maximum operation
R5531 Eigenvalue sequence exists for every complex square matrix
R2783 Arithmetic expression for sum of initial squared natural numbers
R4648 Union of sigma-algebras need not be a sigma-algebra
R4805 Dual probability distribution function for geometric random positive integer
R4464
R4152
R5305 Conditional expectation of a random complex matrix given maximal information
R2833 Nonempty set is singleton iff all elements equal each other
R3259 Weak law of large numbers for variance with weighted decay
R3960 Identically distributed random variables need not be almost surely equal
R5350 Differential Shannon entropy of a uniform random real number
R4992 Complex matrix multiplied from the left by a diagonal matrix
R5415 Variance of a gamma random positive real number
R2090 Isotonicity of probability measure
R4738 Finite subadditivity of probability measure
R233 Whole space is closed
R3498 Homomorphism property of the standard natural logarithm
R2222 Set union is invariant under bijective shifting of indices
R3920 Sublevel events do not necessarily coincide for identically distributed random variables
R2377 Almost sure convergence implies convergence in probability
R5414 Expectation of a gamma random positive real number
R1854 Cardinality of the set of injections between finite sets
R4536 Map image empty iff underlying set empty
R2483 Variance of Bernoulli random boolean number
R4106 Determinant of real diagonal matrix
R2970 The four classes of real intervals are each closed under translation
R4748
R714 Element belongs to its own equivalence class
R4009 Metrisable topological space is Fréchet
R5504 Constant random variable pulls back a bottom sigma-algebra
R5230 Bessel-corrected sample variance of I.I.D. gaussians is a transformed chi-squared random real number
R3896 Idempotence of real expectation
R3440 Uniformly continuous map preserves Cauchy sequences
R5173 Transpose of a product of three complex matrices
R4763 Set complement of map inverse image
R4730 Riemann integral of a constant function on the closed unit interval
R2492 Independent event collection is pairwise independent
R2556 Probability calculus expression for probability conditioned on event of nonzero probability
R368 Image of countable set is countable
R2338 Finite sum of I.I.D. exponential random positive real numbers is a gamma random random positive real number
R5208 Sum of initial cubed natural numbers equals sum of initial natural numbers squared
R4838 Sum rule for simple marginal probability
R3515 Unsigned basic integral zero iff function almost everywhere zero
R5119 Binary homomorphism property of standard natural complex exponential function
R5308 Multiplying by the same random real number need not preserve equality in distribution
R977 Ambient set is union of subset and complement of subset
R5172 Real binomial theorem for exponent seven
R2506 Independent random real collection is uncorrelated
R309 Left-invertible map iff injection
R2302 Memorylessness property of exponential random positive real number
R5303 Real-linearity of complex expectation
R268 Basel problem
R3415 Necessary and sufficient conditions for convergence of geometric complex series
R2938 Vanishing sequence is necessary but not sufficient for finiteness of real series
R2972 The four classes of real intervals are each closed under dilation
R2876 Real mean value inequality
R4391 Characteristic function uniquely identifies the distribution of a random euclidean real number
R4213 Countable set union is invariant under bijective shifting of indices
R2914 Cantor-Bernstein theorem
R4777 Expectation of bounded random real number is within the bounding interval
R4541 Open set is its own interior
R5129 Standard complex cosine function expressed in terms of complex exponential function
R5348 Differential Shannon entropy for a gaussian random real number
R2780 Upper bound for number of arrows in finite digraph
R5285 Expectation of a gaussian random real number
R3942 Derivative of gaussian basic real density function
R590 Square root of two is irrational
R4769
R2525 Independence of sigma-algebras is hereditary
R3901 Domain of map to monoid equals union of kernel and support
R2798 Moments of an indicator random boolean number
R4848 Probability of event conditional on complement
R5211 Tight upper bound to a product of three unsigned real numbers
R3974 Sum of independedent standard chi-squard random real numbers is chi-squared
R2386 Characterisation of almost sure convergence using limit superior and limit inferior
R1036 Power set is closed under complements
R2962 Characterisation of standard natural real exponential function by a differential equation
R4128 Two random real numbers identical in distribution have identical moments
R4671 First-degree polynomial approximation for a standard basic real exponential function near zero
R5263 Slope function for standard real tangent function
R4438 Equivalent characterisations of ergodicity for probability-preserving system
R4453 Probability of symmetric difference of event and subevent
R5235 Sample mean of I.I.D. gaussian random real numbers is a gaussian random real number
R5482 Columns of a real identity matrix span the whole space
R5210 Tight upper bound to a product of two unsigned real numbers
R5320 Absolute value function preserves equality in distribution for random real numbers
R4767
R5370 Geometric random positive integer is the maximum Shannon entropy random positive integer for a given expectation
R4607 Pushforward change of variables formula for unsigned basic integral
R102 Singletons are closed in a metric space
R255 Power set of empty set
R4662 Signed basic expectation with respect to a point probability measure
R4387 Characteristic function of standard Poisson random natural number
R708 Reverse triangle inequality for metric
R5408 I.I.D. real strong law of large numbers
R5160 Subconvex real function need not have a minimizer
R822 Group of prime order is cyclic
R4513
R4470 Inverse image of countable union is union of inverse images
R4350 Finite superadditivity of finite set cardinality
R5128 Standard complex sine function expressed in terms of complex exponential function
R4757 Young's inequality for two real numbers
R5576 Eigenvectors for a symmetric complex matrix are orthogonal
R3581 Absolute moment inherits finiteness from greater exponents for random complex number
R4273 Absolute value function preserves zero
R5418 Counterexample to Wald's first equation when independence not satisfied
R4331 Probability of binary intersection with an almost sure event
R4871 Translation property of the standard real log-sum-exp function
R4811 Markov chain triple iff endpoints conditionally independent
R4869 Characterisation of subconvex real functions
R47 Set difference is subset of the minuend
R4011 Polish space is second-countable
R2373 Second probabilistic Borel-Cantelli lemma
R1885 Absolute value of basic function equals sum of positive and negative parts
R4802 Law of total probability for complement partition in terms of random variables
R1868 Composition of indicator function with set endomorphism
R3681 Mean-deviance standardisation of a random real number
R4012 Polish space is Hausdorff
R5520 Cofactor partition for a 2-by-2 complex square matrix
R3544 Endpoint bounds for real arithmetic mean
R4483 Real number is zero iff equal to its reflection
R5549 Complex matrix gramians are conjugate symmetric
R4947 Variance of standard Bernoulli random boolean number
R1075 Basic real interior extremum theorem
R1960 Characterisation of measure-preserving transformations by signed integral
R5364 A finite real set is standard Borel
R298 Identity map is continuous if topology on domain set is equal or stronger
R5571 Complex algebra expression for the characteristic polynomial of a 2-by-2 complex square matrix
R3970 Measure of finite union finite iff measure of all sets in union finite
R5171 Real binomial theorem for exponent six
R3261 Probability for two independent Bernoulli random numbers to coincide
R2665 Characteristic function of gaussian random real number
R4934 Real conditional expectation given maximal information
R2497 Reflection property of the standard Wiener process
R4149 Countable intersection is a lower bound to each set in the intersection
R2120 Bounded continuous function is Riemann integrable on a real interval
R4274 Absolute value function escapes to positive infinity in both directions
R5232 Finite sum of independent gaussian random real numbers is a gaussian random real number
R4147 Not all subsets of a cartesian product need be cylinder sets
R4898
R4165 Superset of countable union iff superset of every set in the union
R10 Binary cartesian product with empty set is empty
R4948 Gaussian approximation to standard binomial distribution
R4888 Isotonicity of set cardinality
R4326 Probability of binary union with almost sure event
R3680 Characteristic function of standard gaussian random real number
R4982 Exchangeable random collection is identically distributed
R3996
R5622
R4215 Countable set intersection is invariant under bijective shifting of indices
R4577 Countable indicator partition of complex expectation in terms of pullback events
R3958 Intersecting subtrahend with minuend preserves set difference
R4097 Real arithmetic expression for real matrix determinant
R4183 Alternative basic real arithmetic expressions for Catalan sequence
R3595 Probabilistic Tonelli's theorem
R5487 Dimension of a vector space of finite real matrices
R4566 Countable indicator partition of a complex function
R983 Sequential continuity of measure from above
R3956 Expectation of random unsigned basic number by integrating tail probabilities
R4654 Probability calculus expression for basic real conditional expectation given a complement partition of the sample space
R5092 Probability of binary intersection with a null event
R457 Fréchet space iff singletons are closed
R4649 Probability calculus expression for basic real conditional expectation given a countable partition of the sample space
R5162 Minimizer need not be unique for a subconvex real function
R3289 Sequence in product space is Cauchy iff each component sequence is Cauchy
R4996
R4823 Conditional probability of the empty event
R2680 The Quadratic Formula
R4851 Tight upper bound to simple entropy
R4661 Integer power recurrence of basic real golden ratio
R3646 Countable partition additivity of probability measure
R5170 Expectation of conditional expectation for a random complex number
R4857 Standard logarithm of a positive real number raised to an integer power
R4333 Binary product of indicator functions equals indicator of intersection
R5532 Complex matrix determinant equals product of eigenvalues
R431 Set of integers is countable
R3945 Set is a superset to its interior
R5631 Strong fundamental theorem of complex algebra for a quadratic complex polynomial
R4921 Affine transformations preserve independent countable real collection
R4126 Almost surely bounded random complex number has all absolute moments finite
R3983 Subcollection of independent collection of sigma-algebras is independent
R315 Composition of surjections is surjection
R2203 Expectation of a Poisson random natural number
R4639 Characteristic function for translated random real number
R3955 Components of standard gaussian random euclidean real number are standard gaussian random basic real numbers
R5165 Central limit theorem for I.I.D. sample mean series
R3776 Probability to win an exponential race
R3946 Interior is an open set
R3148 Sum of real telescoping series
R3972 Expression for random basic real sum of squares in terms of sample mean and variance
R4318 Inclusion-exclusion principle for unsigned basic measure of binary union
R4915
R4188 Set cardinality in terms of finite ambient set
R1131 Image of inverse image
R4295 Power set of a countable set need not be countable
R2687 Approximating function for the natural exponential function
R2034 Weighted Hölder's inequality for real power means in the case of two real sequences
R4520 Complex conditional expectation is absolutely integrable
R1130 Intersection is largest lower bound
R3770 Product of real 2-by-2 matrix with its transpose
R4780 Real conditional expectation given independent sigma-algebra
R7 Empty set is subset of every set
R4867 Initial sum of powers of two
R4261 Real binomial theorem for exponent two
R5238 Sample mean of uncorrelated identically distributed gaussian random real numbers is a gaussian random real number
R2767 Identity map is an injection
R3873 Expectation of stopping time for I.I.D. sum of standard uniform random basic real numbers
R1035 Power set is closed under intersections
R4830 Change of base formula for logarithm function
R4445 Inclusion-exclusion principle for probability of binary union
R3228 Bounded sequence need not be Cauchy
R1540 Affine map preserves convex sets in images
R4679 Independent countable random real collection is uncorrelated
R3612 Standard natural basic real logarithm function is strictly isotone
R4140 Standardised Mill's inequalities
R2239 Expectation of exponential random positive real number
R5102 Count of boolean functions on initial positive integers with given sum
R322 Image of projection map
R4145 Binary union is an upper bound to both sets in the union
R4534
R3898 Distribution of sum of two random euclidean real numbers is convolution of distribution measures
R108 Inclusion iff reverse inclusion of complements
R4895 Standard counting measure is a point-mass measure
R4279 Explicit algebraic expression for elements of generated subgroup with singleton generator set
R2719 Affine majorant for the standard natural logarithm
R5537 Derivative function for euclidean real self-dot product function
R3205 Probability mass function for geometric random positive integer
R5318 Unions need not preserve equality in probabilities for events
R5420 Minimum and maximum of stopping times are stopping times for random real process
R4437 Complement of stationary measurable set is stationary
R1851 Cardinality of set of permutations on finite set
R5266 Real calculus expression for distribution function of standard exponential random positive real number
R3912 Characteristic function of rademacher random integer
R4844 Mutual information of a simple random variable with respect to itself
R371 Countable set iff injection to natural numbers
R4286 Standard natural basic real logarithm function maps one to zero
R4656 Probability calculus expression for conditional probability given a countable partition of the sample space
R4276 Triangle inequality for absolute value function
R3919 Probability measure need not be an injection
R1171 Isotonicity of Euclidean volume function
R4699
R2259 Variance of a finite sum of random real numbers
R4304 Nonempty finite poset contains a minimal element
R3611
R2989 Unsigned basic Lebesgue integral under scaling
R4327 Probability of countable union with an almost sure event
R1838 Cardinality of finite set union of finite sets
R5283 Expectation of a standard bernoulli random boolean number
R4746 Superadditivity and subadditivity of limit superior and limit inferior for unsigned basic integral
R2897 Fourier transform under scaling
R5325 Conditional expectation of random real number conditioned on an independent random real number
R4144 Finite union is an upper bound to each set in the union
R5298 Complex conjugatation is an additive operation
R5586 Diagonalizable complex matrix need not be invertible
R4431
R4794 Independent minimums preserve exponential distribution
R5533 Complex matrix trace equals sum of eigenvalues
R1565 Goursat's theorem
R4913 Strong derivative for euclidean real quadratic form without translation
R5485 Columns of a real matrix need not span the whole space
R1743 Intersection of finite sets is finite
R2748 Finite sets are closed in metric space
R5506 Inverse for a 2-by-2 real square matrix
R5359 Reflection property of simple relative entropy
R4756
R5229 Bessel-corrected sample variance of independent standard gaussians is a transformed chi-squared random real number
R4593 Expectation of a standard gaussian random real number
R17 Bijection from the set of natural numbers to the set of integers
R3583 Random basic number absolutisation equals sum of positive and negative parts
R4932
R3642 Law of total probability for complement partition
R1234 Borel-Cantelli lemma
R5379 Distribution of the real Wiener process at a given point is gaussian
R2437 Euclidean real Fourier inversion theorem
R5079 Characterisation of complex matrix eigenvalues in terms of characteristic polynomial
R403 Square of the imaginary number
R310 Right-invertible map iff surjection
R1064 Isotonicity of Lebesgue measure
R5127 Fundamental theorem of real trigonometry
R5072 Determinant of a triangular complex matrix
R975 Isotonicity of unsigned basic measure
R5400 Lévy characterisation of the standard real Wiener process
R2141 Reflection invariance of unsigned basic Lebesgue integral
R5394 Finite summation need not preserve equality in distribution
R1544 Anova partition of orthogonal projection
R4631 Cardinality of finite cartesian products is invariant under insertion of parentheses
R3745 Real square matrix antisymmetric part is zero definite
R3183 First fundamental theorem of Riemann integral calculus
R3198 Finite sum of uncorrelated Poisson random natural numbers is Poisson
R4269 Countable set union with empty set
R800 Proof by principle of weak mathematical induction
R4728
R1193 Finite product of indicator functions equals indicator of intersection
R4303 Nonempty finite poset contains a maximal element
R4680 I.I.D. strong law of large numbers for random real numbers of finite fourth moments
R30 Inverse image of intersection is intersection of inverse images
R4809 Affine transformations preserve independent finite real collection
R2219 Set intersection is associative
R3670 Modulus sum upper bound to distance between two finite complex products for complex numbers in the unit disc
R4214 Finite set union is invariant under bijective shifting of indices
R4904 Derivative for real square function
R4512
R1832 Cardinality of a finite cartesian product of finite sets
R5623 Euclidean complex dot product is conjugate symmetric
R4928 Finite partition additivity of probability measure
R508 Finite cartesian product of countable sets is countable
R4455
R4711 Probability of complement of event which is not the whole sample space need not be nonzero
R3513 Measurable subnull set has measure zero
R4660 Real empirical probability distribution function converges pointwise to the true distribution function
R1902 Signed basic integral of almost everywhere equal functions
R2875 Cauchy's real mean value theorem
R1233 Finite additivity of unsigned basic integral
R4272 Absolute value function is not strictly antitone
R2086 Finite inclusion-exclusion principle for unsigned basic measure
R5513 Real matrix determinant is homogeneous with respect to multiplying a row or a column by a constant
R5182 Tight upper bound to a finite product of unsigned real numbers
R5097 Power set is isomorphic to a set of boolean functions
R4720 Conditional probability of complement event
R2537 Real exponentiation function with positive exponent is strictly isotone on positive reals
R3020 Complex Lebesgue integral under scaling
R5360 Probability that a continuous random real number takes value in a countable set is zero
R5234 Sample mean of independent gaussian random real numbers is a gaussian random real number
R4565 Countable indicator partition of a euclidean real function
R3200 Characteristic function of Bernoulli random boolean number
R1030 Sigma-algebra is closed under countable intersections
R5444 Expectation of a squared standard gaussian random real number
R5528 Determinant zero if a complex square matrix contains two identical rows or two identical columns
R248 Binary subadditivity of basic real square root function
R5471 Real square matrix invertible iff transpose is
R4603
R5358 Gibbs' inequality for simple relative entropy
R4390 Fourier transform characterises euclidean real probability measure
R4853 Tight lower bound to simple mutual information
R4781 Conditional expectation of known random real number
R1165 Reflection invariance of Lebesgue measure
R292 Union is smallest upper bound
R1846 Cardinality of set complement
R4112 Strong fundamental theorem of complex algebra
R4107 Determinant of real diagonal matrix with constant diagonal
R4219 Dirichlet's theorem
R4468 Set of stationary measurable sets is a sigma-algebra
R3316 Pointwise limit of continuous functions need not be continuous
R5077 Injection from the natural number plane to the set of natural numbers
R1034 Power set is closed under unions
R4786 Real conditional covariance partition into conditional moments
R4073 Probability of union with the impossible event
R1194 Indicator function with respect to set complement
R5244 Complex number is zero iff equal to its reflection
R5558 Characteristic polynomial for a complex diagonal matrix of constant diagonal
R2081 Binary set intersection with empty set is empty
R1762 Closed set less open set is closed
R4616 The standard mollifier satisfies sufficient conditions required of an approximate identity
R5322 Adding the same random real number need not preserve equality in distribution
R1839 Cardinality of power set of a finite set
R2522 Real conditional expectation given minimal information
R4322 Cardinality of finite set union of disjoint sets
R3414 Necessary and sufficient condition for convergence of real harmonic series
R5441 Variance of a gaussian random real number
R5439 Expectation of a chi random unsigned real number
R4510 Two complex numbers equal iff difference equals zero
R4609
R5519 Real arithmetic expression for the determinant of a 2-by-2 real square matrix
R5125 Euler's formulas
R5556 Squared eigenvalue is an eigenvalue for the square of a complex matrix
R5512 Determinant zero if a real square matrix contains two identical rows or two identical columns
R3545 Endpoint bounds for real convex combination
R4447
R3367 Characterisation of convergence of geometric basic real series
R2623 Indicator function operator on set of N-subsets is bijection
R5620
R5111 Number of injections is proportional to number of subsets of given size
R4912 Strong derivative for symmetric euclidean real quadratic form
R5168 Infinite product of real numbers in right-closed unit interval vanishes iff infinite sum of duals diverges
R1558 Second fundamental theorem of complex integral calculus
R4187 Complement of an F-sigma set is a G-delta set
R4832 Homomorphism property of standard logarithm function in the binary case
R5502 Real conditional expectation with respect to a constant random real number
R2405 Characteristic function uniquely identifies the distribution of a random real number
R262 Countable union of countable sets is countable
R4430 Probability of event in backward orbit under probability-preserving endomorphism
R2079 Isotonicity of set intersection
R5093 Total number of fixed-length sequences using a given number of labels
R3060 Riemann integral of even real function over an interval symmetric abour zero
R4267 Set intersection with empty set is empty
R5177 Young's inequality for two real numbers with standard conjugate exponents
R5413
R5297 Complex conjugate of a product of two complex numbers
R4901 Probability density function for standard exponential random positive real number
R4282 Standard natural basic real exponential function vanishes at negative infinity
R3959 Affine coefficients which minimize expectation of squared distance from a target random real number
R4783
R4048 Number of binary relations on binary cartesian product
R4597 Centred gaussian real density function is an even function
R3038 Closed graph theorem
R5324 Conditional expectation of a random real number conditioned on itself
R2764 Canonical singleton map is bijection
R3184 Second fundamental theorem of Riemann integral calculus
R3694 Lindeberg central limit theorem
R2964 Even function equals its even part
R5292 Complex conjugate of a complex eigenvalue of a complex matrix is an eigenvalue for the conjugate matrix
R4560 Probability of complement of a null event
R5064 Cofactor partition for a real square matrix
R4831 Homomorphism property of standard logarithm function
R5251 Exponential random positive real number is a gamma random positive real number
R4907 Strong derivative for constant euclidean real function
R5526 Complex matrix determinant is homogeneous with respect to multiplying a row or a column by a constant
R4822 Conditional probability of the sample space
R1368 Jensen's inequality
R3757 Linearity of basic real matrix trace
R979 Countable subadditivity of measure
R4695 An infinite product of real numbers on the open unit interval need not converge to zero
R4518 Equivalent characterisations of finiteness of variance for a random real number
R4573 Complex expectation over a null event is zero
R1166 Lebesgue measure under scaling
R5237 Finite sum of uncorrelated identically distributed gaussian random real numbers is a gaussian random real number
R3931 Subtracting set from empty set
R104 Set of rational numbers is countable
R4814 Markov chain triple iff reverse is a Markov chain triple
R3260 Weak law of large numbers for random real triangular arrays
R5073 Determinant of an upper triangular complex matrix
R4208
R5376 Riemann integral of an exponential random positive real number density function
R4132 Strict version of probabilistic Markov inequality
R3784 Law of total probability for complex expectation in terms of pullback events of a discrete random variable
R4944 Real binomial theorem for exponent four
R4689 Probabilistic Cavalieri principle
R1371 Bilinear map is zero if either argument is zero
R5432 Expectation of the standard integer random walk after a given number of steps
R2484 Moments of a Bernoulli random boolean number
R4741 Probabilistic Chebyshov's inequality for square function
R4705 Inner product with repeating argument is a real number
R4943 Real binomial theorem for exponent three
R4186 Complement of a G-delta set is an F-sigma set
R5123
R3472 Maximum modulus principle
R301 Canonical identity map is an injection
R424 Euler's identity
R4961
R2076 Inverse image of empty set
R5518 Complex arithmetic expression for the determinant of a 2-by-2 complex square matrix
R4666 Real GM-HM inequality
R4158 Power set is multiplicative
R2981 Riemann integral is particular case of Lebesgue integral
R4143 Countable union is an upper bound to each set in the union
R5141 Real log-sum-exp method
R4398
R4489 Sigma-algebra is closed under limit superiors and limit inferiors
R4074 Arbitrary intersection of subsets is subset
R5521 Signs of length-2 standard permutations
R4280 Standard natural basic real exponential function is strictly isotone
R3852 Transforming random real number to a uniform random real number
R3640 Conditional probability given independent sigma-algebra
R3746 Transpose of binary product of real matrices
R4182 Isotonicity of sublevel probabilities for a random real number
R4508 Two real numbers equal iff difference equals zero
R4057 The set of boolean standard sequences is uncountable
R4161 Subset of countable intersection iff subset of every set in the intersection
R5209 Of all rectangles with a given perimeter, the square maximizes the area
R5486 Dimension of a euclidean real vector space
R3897 Distribution of random finite euclidean real sum is convolution of distribution measures
R5429 Maximum likelihood estimator for the common parameter of I.I.D. exponential random positive real numbers
R3589 Random basic number almost surely finite if first absolute moment is finite
R4469 Countable union of stationary measurable sets is stationary
R796 Principle of weak mathematical induction
R5567 Eigenvalue sequence for a diagonal complex matrix with constant diagonal
R4914 Derivative for an affine real matrix function
R4000 Empty set is clopen
R2262 Real variance partition into first and second moments
R2440 Translation invariance of Lebesgue outer measure
R4826 Logarithm of a ratio
R3 Stirling formula
R2463 Determinant of a real identity matrix
R5499 Dimension of a euclidean complex vector space
R5076 Bijection from the natural number plane to the set of natural numbers
R5555 Complex arithmetic expression for a complex matrix quadratic form
R3243 Constant random variable is independent of any other random variable
R4632 Cardinality of cartesian triple products is invariant under insertion of parentheses
R5435 Expectation of a chi-squared random unsigned real number
R3939 Upper and lower bounds for codomain set of finite unsigned basic measure
R1083 Minimal element is minimum element in ordered set
R3641 Conditional probability given independent random variable
R2871 Equivalent characterisations of a Schwartz function
R2113 Riemann integral of a constant function
R1824 Birkhoff ergodic theorem
R5395 Factorization need not preserve equality in distribution
R5334 Mode maximizes expected number of correct guesses for a finite sequence of discrete random real numbers
R4315 Cardinality of a finite set raised to a finite power
R3911 Probability density function for standard gaussian random real number
R3922 Gaussian random real number is symmetric about its expectation
R5150 Global minimizer of subconvex real function iff zero is a subgradient
R5375 Riemann integral of decaying standard natural real exponential function over the positive real line
R3207 Probability density function for a chi-squared random unsigned real number
R5317 Intersections need not preserve equality in probabilities for events
R3602 Gaussian approximation to binomial distribution
R4950 Real matrix with no real eigenvalues
R5239 Expectation of standard unsigned uniform random real number
R4189
R2599 Cantor's theorem
R2395 Subset of empty set is empty
R5059 Adjugate for a 2-by-2 real square matrix
R5589 Eigenvalues of a complex matrix left gramian are unsigned real numbers
R4537 Inclusion of inverse image does not imply inclusion of image
R4164 Superset of union iff superset of every set in the union
R4628 Map to empty set is a surjection
R828 First group isomorphism theorem
R5146 Standard natural logarithm is superconvex
R4739 Binary subadditivity of probability measure
R2787 Pascal's rule
R2182 Isotonicity of real sublevel sets
R3493 Empirical distribution function converges in probability to the true distribution function
R2806 Standardising a gaussian random real number
R3600 Finite sum of independent Poisson random natural numbers is Poisson
R5505 Cofactor matrix for a 2-by-2 real square matrix
R5511 Interchanging two rows or two columns of a real square matrix switches the sign of the determinant
R1973 Map composition is associative
R5624 Euclidean real dot product is symmetric
R2436 Polar representation of complex conjugate
R1176 Inverse image of a constant map is either empty or equal to the domain set
R354 Image of singleton set
R5554 Real matrix trace is commutation invariant for two real matrices
R50 Set difference equals intersection with complement
R4284 Standard natural basic real logarithm function escapes to negative infinity at zero
R4127 Real exponentiation function with unsigned exponent is isotone on unsigned reals
R5267 Probability density function for gaussian random real number
R5559 Characteristic polynomial for a complex diagonal matrix
R2220 Binary set intersection is commutative
R5046 Absolute moment inherits finiteness from greater exponents for random real number
R2658 Standard natural real logarithm function grows linearly near 1
R81 Bilipschitz map is continuous
R4773 Inclusion-exclusion lower bound to probability of ternary intersection
R4973 Bias-variance partition of mean square error for random basic real number
R4740
R4157 Superadditivity of power set
R466 Principle of double-negation is a propositional tautology
R5192 Cauchy-Schwarz inequality for two real sequences
R3941 Slope function for standard real gaussian density function
R3535 Riemann integral of unit semicircle
R5282 Expectation of a random fraction need not equal fraction of expectations
R4630 Bijection between parenthesis-sliced cartesian triple products
R5523 Permutation sign sum for complex matrix determinant over the columns
R2160 Conditional expectation of known random complex number
R1848 Bijection between parenthesis-sliced cartesian products
R4095 Real arithmetic expression for real arithmetic mean
R5349 Differential Shannon entropy for an exponential random positive real number
R4330 Probability of finite intersection with an almost sure event
R1242 Unsigned basic integral is compatible with measure
R2595 Convolution identity for binomial coefficient
R3587 Random basic number almost surely finite iff positive and negative parts are
R1158 Translation invariance of Euclidean volume function
R5560 Characteristic polynomial for a triangular complex matrix
R4542 Map is inverse to its inverse
R5565 Eigenvalue sequence for a lower triangular complex matrix
R4733 Conditional expectation of known random euclidean real number
R1567 Positive real geometric mean expressed in terms of real arithmetic mean
R5194
R4686 Probabilistic Chebyshov's inequality for an exponentiation function
R4093 Real harmonic and arithmetic means are multiplicative inverses when arguments are
R5393 I.I.D. real empirical distribution measure converges to a probability for a fixed Borel set
R5466 Linear slope which minimizes expectation of squared distance from a target random real number
R5276 Probability to win an I.I.D. exponential race
R4668 Transpose of a finite product of complex matrices
R293 Open set less closed set is open
R5430 Growth rate for the expectation of the absolute value of the standard integer random walk
R755 Group centre is Abelian group
R4697 Simple integral of a measurable simple function with respect to a point measure
R2746 Finite sets are closed in Fréchet space
R5304 Complex-linearity of real expectation
R1073 Mean value theorem
R2254 Riemann integral of standard real gaussian function
R2928 Finite sum of even euclidean real functions is even
R3744 Real arithmetic expression for a real matrix quadratic form
R4294 Set difference with finite minuend is finite
R3532 Tautological pointwise lower bound from indicator function on sublevel set
R4160 Subset of intersection iff subset of every set in the intersection
R5243 Finite sum of uncorrelated identically distributed exponential random positive real numbers is a gamma random random positive real number
R756 Abelian group iff centre is whole group
R4906
R4321 Set and set complement are disjoint
R5530 Determinant of a scaled real matrix
R4339 Conditional probability of almost surely false event
R5219 Mean-value theorem applied to the standard unit semicircle function
R2071 Isotonicity of set union
R3679 Standardised I.I.D. real central limit theorem with the identity index sequence
R5627 Complex matrix multiplied by a complex column matrix from the right
R4461
R4166 Superset of finite union iff superset of every set in the union
R5643 Cardinality of the set of bytes
R3938 Upper and lower bounds for codomain set of probability measure
R5404 I.I.D. real central limit theorem
R4038 Product of two finite real sums
R976 Finite disjoint additivity of unsigned basic measure
R3061 Real Riemann integral over a reflected interval
R244 Convergent sequence is Cauchy
R3749 Partition of real square matrix into sum of symmetric and antisymmetric parts
R2548 Constant map pulls back a bottom sigma-algebra
R4378 Independent random basic real pair iff distribution functions factorise
R5557 Complex matrix characteristic polynomial is a monic polynomial with degree equal to row and column dimensions
R4905 Derivative for standard natural real logarithm function
R3461 Holomorphic function with vanishing derivative on complex domain is constant
R2959 Function even part is even
R2410 I.I.D. real weak law of large numbers under finite second absolute moments
R2782 Arithmetic expression for sum of initial natural numbers
R352 Inverse image of image
R2812 Finite variance implies finite expectation for random real number
R4281 Standard natural basic real exponential function is escapes to positive infinity at positive infinity
R4341 Bayes' theorem in the case of two pullback events
R4291 Vector space always has an inclusion-maximal linearly independent set
R4617 The standard mollifier integrates to one
R1120 Antitonicity of minimum
R4207
R2933 Isotonicity of countably infinite real summation
R4055 Singleton map is injection from set to power set
R4691 Expectation of random natural number by summing tail probabilities
R4568 Countable indicator partition of a random complex number
R2112 Isotonicity of Riemann integral
R5535 Reciprocals form an eigenvalue sequence for complex matrix inverse
R3995 Complex binomial theorem
R4795 Real calculus expression for distribution function of exponential random positive real number
R2055 Cavalieri principle for basic real Riemann integral calculus
R984 Transforming an isotone sequence of sets into pairwise disjoint sequence with common limit
R3618 Turning two unsigned real numbers into convex combination coefficients
R4791 Probability for two independent standard Bernoulli random boolean numbers to coincide
R4563 Complex integral over a set of measure zero is zero
R2310 Distribution formula for unsigned basic integral
R5490 Real matrix injective iff kernel trivial
R5144 Vanishing gradient identifies a minimizer for differentiable subconvex real function
R5399 Sample average of I.I.D. integrable random real numbers converges to expectation almost surely
R738 Left and right cosets coincide in Abelian group
R2075 Image of empty set
R507 Empty set is countable
R5226 Tight lower bound on the probability for two independent Bernoulli random boolean numbers to coincide
R4970
R2934 Isotonicity of unsigned basic real series
R2339 Finite sum of uncorrelated gaussian random real numbers is a gaussian random real number
R75 Intersection of closed sets is closed
R4595 Basic real calculus expression for moments of centred gaussian random basic real number
R5568 Eigenvalue sequence for an identity complex matrix
R5115 Natural number factorial is an even number for numbers 2 or greater
R5327 Expectation of a standard exponential random positive real number
R5569 Determinant of reflected complex matrix
R2413 Complex conjugate of real number
R3883 Row-standardisation of row-independent random real triangular array
R1401 Orthogonality relation is a symmetric binary relation
R4765 Reflection preserves euclidean real subset relation
R270 Real arithmetic expression for sum of a finite real geometric sequence
R2374 Borel-Cantelli zero-one law
R2368 I.I.D. real strong law of large numbers with the identity index sequence
R5365 A singleton real set is standard Borel
R1831 Real arithmetic expression for binomial coefficient
R4001 Whole space is clopen
R511 Natural number plane is countable
R5361 A countable real set is standard Borel
R3503 Data processing inequality
R4278 Expression for probability of event in terms of complement event
R5061 Expression for a real matrix inverse in terms of adjugate
R4787
R4222 Quotienting a set reduces its cardinality
R5619
R5336 Expectation of an indicator random boolean number
R4216 Finite set intersection is invariant under bijective shifting of indices
R5510 Real square matrix which has a zero column or a zero row has determinant zero
R4927 Binary partition additivity of unsigned basic measure
R1177 Constant map is always measurable
R5069 Determinant of a diagonal complex matrix
R3874
R3617 Turning a finite number of unsigned real numbers into convex combination coefficients
R5368 Uniform distribution is the maximum simple Shannon entropy distribution for fixed alphabet
R4665 Weighted real GM-HM inequality
R4334 Every nonempty finite graph contains a bipartite subgraph with at least half the edges
R4841 Finite disjoint additivity of probability measure
R3621 Standard natural exponential function equals powers of Napier's constant
R1575 Goursat's theorem for rectangles
R347 Isotonicity of map image
R4288
R465 De Morgan's laws are propositional tautologies
R4855 Reflection property of standard logarithm function
R5241 Finite sum of I.I.D. Poisson random natural numbers is Poisson
R4989 Information inequality for simple relative entropy
R74 Finite union of closed sets is closed
R5536 Eigenvalues of a conjugate symmetric complex matrix are real
R4599 Density partition for expectation of a random real number
R4685 I.I.D. weak law of large numbers for random real numbers of finite first absolute moments
R5300 Unsigned basic integral over an empty set equals zero
R5423 Wald's second equation under independence
R1338 Probabilistic Borel-Cantelli lemma
R4846 Conditional simple entropy with respect to itself
R1370 Multilinear map is zero if any argument is zero
R4706 Complex conjugate zero iff argument zero
R5169 Infinite product of real numbers in right-closed unit interval does not vanish iff infinite sum of duals converges
R5527 Interchanging two rows or two columns of a complex square matrix switches the sign of the determinant
R80 Lipschitz map is continuous
R87 Convolution is commutative
R5544 Real matrix trace is preserved by transposing
R4372 Independent random real pair is uncorrelated
R1557 Weighted real AM-GM inequality
R4678 Independent finite random real collection is uncorrelated
R1369 Jensen's inequality for expectation
R4594 Real calculus expression for central moments of gaussian random real number about expectation
R4886 Characterisation of a quotient set by proper set partitions