ProbabilityTheory.IsBrownianRealstructureMathlib.Probability.BrownianMotion.Basic, predicateEnglish
Let $X$ be a function from elements of $\mathrm{NNReal}$ and elements of $x$ to real numbers. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_IsBrownianReal\_\_\_auto\_1}$. Then we can say that $\operatorname{IsBrownianReal}$ holds for $X$ and $P$.
ProbabilityTheory.IsPreBrownianRealstructureMathlib.Probability.BrownianMotion.Basic, predicateEnglish
Let $X$ be a function from elements of $\mathrm{NNReal}$ and elements of $x$ to real numbers. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_IsPreBrownianReal\_\_\_auto\_1}$. Then we can say that $\operatorname{IsPreBrownianReal}$ holds for $X$ and $P$.
ProbabilityTheory.BrownianReal.covMatrixdefMathlib.Probability.BrownianMotion.GaussianProjectiveFamily, function or constantEnglish
Let $I$ be a finite set of $\mathrm{NNReal}$. Then there is a matrix of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ and $\Real$. Proof. Let $I$ be arbitrary. Let $s_{1}$ be arbitrary. Let $t_{1}$ be arbitrary. By s1. By NNReal__toReal. By t1. By NNReal__toReal. By Min__min. By Matrix__of__app.
ProbabilityTheory.BrownianReal.projectiveFamilydefMathlib.Probability.BrownianMotion.GaussianProjectiveFamily, function or constantWording
the projective family of I (from the name)
English
Let $I$ be a finite set of $\mathrm{NNReal}$. Then the projective family of $I$ is a measure of the set of functions from elements of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ to real numbers defined as the map of $\operatorname{coe}$ applied to the inverse of $\operatorname{toLp}$ applied to $2$ and the set of functions from elements of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {I}{x_{1}})}$ to real numbers and $\operatorname{multivariateGaussian}$ applied to $0$ and $\operatorname{covMatrix}$ applied to $I$.
ProbabilityTheory.cdfdefMathlib.Probability.CDF, function or constantWording
the cumulative distribution function of x (from the name)
English
Let $x$ be a measure of $\Real$. Then the cumulative distribution function of $x$ is a Stieltjes function of $\Real$ defined as the conditional cumulative distribution function of the product of the Dirac of $\operatorname{unit}$ and $x$ and $\operatorname{unit}$.
SimpleGraph.binomialRandomdefMathlib.Probability.Combinatorics.BinomialRandomGraph.Defs, function or constantEnglish
Let $V$ be a set. Let $p$ be an element of the unit interval. Then $\operatorname{binomialRandom}$ applied to $V$ and $p$ is a measure of the set of simple graphs of $V$ defined as the preimage of $\operatorname{edgeSet}$ and $\operatorname{setBernoulli}$ applied to the complement of the diagonal set and $p$.
ProbabilityTheory.condVardefMathlib.Probability.CondVar, function or constantWording
the conditional variable of x2 and x3 (from the name)
English
Assume that $x$ is a measurable space. Let $X$ be a function from elements of $x$ to real numbers. Let $x_{2}$ be a measure of $x$. Let $x_{3}$ be an element of $x$. Then the conditional variable of $x_{2}$ and $x_{3}$ is a real number defined as the conditional exponential of the exponentiation of the difference between $X$ and $\operatorname{condExp}$ applied to $X$ to $2$ and $x_{3}$.
ProbabilityTheory.conddefMathlib.Probability.ConditionalProbability, function or constantWording
the conditional probability measure of measure of x1 and s (from the docstring)
English
Let $x_{1}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then the conditional probability measure of measure of $x_{1}$ and $s$ is a measure of $x$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (x_{1} (s))}{\operatorname{restrict} (x_{1} , s)}$.
ProbabilityTheory.HasArgminEstimatorstructureMathlib.Probability.Decision.BayesEstimator, predicateEnglish
Let $x_{6}$ be a function from elements of $x$ and elements of $x_{4}$ to elements of $\mathrm{ENNReal}$. Let $P$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a measure of $x$. Then we can say that $\operatorname{HasArgminEstimator}$ holds for $x_{6}$, $P$ and $x_{7}$.
ProbabilityTheory.HasArgminEstimator.argminEstimatordefMathlib.Probability.Decision.BayesEstimator, function or constantWording
the argmin estimator of h4 and x8 (from the name)
English
Assume that $\operatorname{HasArgminEstimator}$ holds for $x_{6}$, $P$ and $x_{7}$. Let $x_{8}$ be an element of $x_{1}$. Then the argmin estimator of $h_{4}$ and $x_{8}$ is an element of $x_{2}$ defined as $\operatorname{choose}$ applied to $\mathrm{ProbabilityTheory\_\_HasArgminEstimator\_\_exists\_isArgminEstimator}$ applied to $h_{4}$ and $x_{8}$.
ProbabilityTheory.IsArgminEstimatorstructureMathlib.Probability.Decision.BayesEstimator, predicateEnglish
Let $x_{6}$ be a function from elements of $x$ and elements of $x_{4}$ to elements of $\mathrm{ENNReal}$. Let $P$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a measure of $x$. Let $f$ be a function from elements of $x_{1}$ to elements of $x_{4}$. Then we can say that $\operatorname{IsArgminEstimator}$ holds for $x_{6}$, $P$, $x_{7}$ and $f$.
ProbabilityTheory.IsArgminEstimator.kerneldefMathlib.Probability.Decision.BayesEstimator, function or constantWording
the kernel of h4 (from the name)
English
Assume that $\operatorname{IsArgminEstimator}$ holds for $x_{6}$, $P$, $x_{7}$ and $f$. Then the kernel of $h_{4}$ is a kernel of $x_{1}$ and $x_{2}$ defined as $\operatorname{deterministic}$ applied to $f$ and $\operatorname{measurable}$ applied to $h_{4}$.
ProbabilityTheory.IsBayesEstimatordefMathlib.Probability.Decision.BayesEstimator, predicateEnglish
Let $x_{6}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{ENNReal}$. Let $P$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a kernel of $x_{1}$ and $x_{2}$. Let $x_{8}$ be a measure of $x$. Then $\operatorname{IsBayesEstimator}$ holds for $x_{6}$, $P$, $x_{7}$ and $x_{8}$, if $\EqtMACRoH {\operatorname{avgRisk} (x_{6} , P , x_{7} , x_{8})}{\operatorname{bayesRisk} (x_{6} , P , x_{8})}$.
ProbabilityTheory.avgRiskdefMathlib.Probability.Decision.Risk.Defs, function or constantEnglish
Let $x_{6}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{ENNReal}$. Let $P$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a kernel of $x_{1}$ and $x_{2}$. Let $x_{8}$ be a measure of $x$. Then $\operatorname{avgRisk}$ applied to $x_{6}$, $P$, $x_{7}$ and $x_{8}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{lintegral}$ applied to $x_{8}$ and the function that maps $x_{9}$ to $\operatorname{lintegral}$ applied to $\operatorname{comp}$ applied to $x_{7}$, $P$ and $x_{9}$ and the function that maps $y$ to $x_{6}$ applied to $x_{9}$ and $y$.
ProbabilityTheory.bayesRiskdefMathlib.Probability.Decision.Risk.Defs, function or constantEnglish
Let $x_{6}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{ENNReal}$. Let $P$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a measure of $x$. Then $\operatorname{bayesRisk}$ applied to $x_{6}$, $P$ and $x_{7}$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $x_{8}$ to the infimum of the function that maps $h$ to $\operatorname{avgRisk}$ applied to $x_{6}$, $P$, $x_{8}$ and $x_{7}$.
ProbabilityTheory.minimaxRiskdefMathlib.Probability.Decision.Risk.Defs, function or constantEnglish
Let $x_{6}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{ENNReal}$. Let $P$ be a kernel of $x$ and $x_{1}$. Then $\operatorname{minimaxRisk}$ applied to $x_{6}$ and $P$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $x_{7}$ to the infimum of the function that maps $h$ to the supremum of the function that maps $x_{8}$ to $\operatorname{lintegral}$ applied to $\operatorname{comp}$ applied to $x_{7}$, $P$ and $x_{8}$ and the function that maps $y$ to $x_{6}$ applied to $x_{8}$ and $y$.
ProbabilityTheory.riskIncreasedefMathlib.Probability.Decision.Risk.RiskIncrease, function or constantEnglish
Let $x_{6}$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{ENNReal}$. Let $P$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a measure of $x$. Then $\operatorname{riskIncrease}$ applied to $x_{6}$, $P$ and $x_{7}$ is an element of $\mathrm{ENNReal}$ defined as the difference between $\operatorname{bayesRisk}$ applied to $x_{6}$, the composition of $\operatorname{discard}$ applied to $x_{1}$ and $P$ and $x_{7}$ and $\operatorname{bayesRisk}$ applied to $x_{6}$, $P$ and $x_{7}$.
MeasureTheory.HasPDFclassMathlib.Probability.Density, predicateEnglish
Let $X$ be a function from elements of $x$ to elements of $E$. Let $x_{2}$ be a measure of $x$. Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{MeasureTheory\_\_HasPDF\_\_\_auto\_1}$. Then we can say that $\operatorname{HasPDF}$ holds for $X$, $x_{2}$ and $x_{3}$.
MeasureTheory.pdfdefMathlib.Probability.Density, function or constantWording
the probability density function of x4 and x5 (from the name)
English
Let $X$ be a function from elements of $x$ to elements of $E$. Let $x_{3}$ be a measure of $x$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{MeasureTheory\_\_pdf\_\_\_auto\_1}$. Let $x_{5}$ be an element of $E$. Then the probability density function of $x_{4}$ and $x_{5}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{rnDeriv}$ applied to the map of $X$ and $x_{3}$, $x_{4}$ and $x_{5}$.
ProbabilityTheory.bernoulliMeasuredefMathlib.Probability.Distributions.Bernoulli, function or constantWording
the Bernoulli measure of y and p (from the name)
English
Let $x_{1}$ and $y$ be elements of $X$. Let $p$ be an element of the unit interval. Then the Bernoulli measure of $y$ and $p$ is a measure of $X$ defined as $\HSMulhSMulMACRoAL {\operatorname{toNNReal} (p)}{\operatorname{dirac} (x_{1})}+ \HSMulhSMulMACRoAL {\operatorname{toNNReal} (\operatorname{symm} (p))}{\operatorname{dirac} (y)}$.
ProbabilityTheory.betadefMathlib.Probability.Distributions.Beta, function or constantWording
the normalizing constant in the beta distribution of x and x1 (from the docstring)
English
Let $x$ and $x_{1}$ be real numbers. Then the normalizing constant in the beta distribution of $x$ and $x_{1}$ is a real number defined as the quotient of the product of the Gamma of $x$ and the Gamma of $x_{1}$ and the Gamma of $x + x_{1}$.
ProbabilityTheory.betaMeasuredefMathlib.Probability.Distributions.Beta, function or constantWording
the Beta measure of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be real numbers. Then the Beta measure of $x$ and $x_{1}$ is a measure of $\Real$ defined as $\operatorname{withDensity}$ applied to the volume and $\operatorname{betaPDF}$ applied to $x_{1}$.
ProbabilityTheory.betaPDFdefMathlib.Probability.Distributions.Beta, function or constantWording
the Beta probability density function of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be real numbers. Then the Beta probability density function of $x_{1}$ and $x_{2}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofReal}$ applied to $\operatorname{betaPDFReal}$ applied to $x$, $x_{1}$ and $x_{2}$.
ProbabilityTheory.betaPDFRealdefMathlib.Probability.Distributions.Beta, function or constantEnglish
Let $x$, $x_{1}$ and $x_{2}$ be elements of $\Real$. Then $\operatorname{betaPDFReal}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{and} (\mathrm{Lt} (0 , x_{2}), \mathrm{Lt} (x_{2} , 1))}{(\frac{ 1}{\operatorname{beta} (x , x_{1})}\times x_{2} ^ {(x - 1)}\times (1 - x_{2})^ {(x_{1} - 1)})}{0}$.
ProbabilityTheory.binomialdefMathlib.Probability.Distributions.Binomial, function or constantEnglish
Let $n$ be a natural number. Let $p$ be an element of the unit interval. Then $\operatorname{binomial}$ applied to $n$ and $p$ is a measure of $\Natural$ defined as the map of $\operatorname{ncard}$ and $\operatorname{setBernoulli}$ applied to $\operatorname{Iio}$ applied to $n$ and $p$.
ProbabilityTheory.cauchyMeasuredefMathlib.Probability.Distributions.Cauchy, function or constantWording
the Cauchy measure of x and x1 (from the name)
English
Let $x$ be an element of $\Real$. Let $x_{1}$ be an element of $\mathrm{NNReal}$. Then the Cauchy measure of $x$ and $x_{1}$ is a measure of $\Real$ defined as $\iteMACRoG {(\EqtMACRoH {x_{1}}{0})}{\operatorname{dirac} (x)}{\operatorname{withDensity} (\operatorname{volume} , \operatorname{cauchyPDF} (x_{1}))}$.
ProbabilityTheory.cauchyPDFdefMathlib.Probability.Distributions.Cauchy, function or constantWording
the Cauchy probability density function of x1 and x2 (from the name)
English
Let $x$ and $x_{2}$ be real numbers. Let $x_{1}$ be an element of $\mathrm{NNReal}$. Then the Cauchy probability density function of $x_{1}$ and $x_{2}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofReal}$ applied to $\operatorname{cauchyPDFReal}$ applied to $x$, $x_{1}$ and $x_{2}$.
ProbabilityTheory.cauchyPDFRealdefMathlib.Probability.Distributions.Cauchy, function or constantEnglish
Let $x$ and $x_{2}$ be real numbers. Let $x_{1}$ be an element of $\mathrm{NNReal}$. Then $\operatorname{cauchyPDFReal}$ applied to $x$, $x_{1}$ and $x_{2}$ is a real number defined as the product of $\operatorname{inv}$ applied to the product, $\operatorname{toReal}$ applied to $x_{1}$ and $\operatorname{inv}$ applied to $(x_{2} - x)^ {2}+ \operatorname{toReal} (x_{1})^ {2}$.
ProbabilityTheory.expMeasuredefMathlib.Probability.Distributions.Exponential, function or constantWording
the exponential measure of r (from the name)
English
Let $r$ be a real number. Then the exponential measure of $r$ is a measure of $\Real$ defined as the Gamma measure of $1$ and $r$.
ProbabilityTheory.exponentialPDFdefMathlib.Probability.Distributions.Exponential, function or constantWording
the exponential probability density function of r and x (from the name)
English
Let $r$ and $x$ be real numbers. Then the exponential probability density function of $r$ and $x$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofReal}$ applied to $\operatorname{exponentialPDFReal}$ applied to $r$ and $x$.
ProbabilityTheory.exponentialPDFRealdefMathlib.Probability.Distributions.Exponential, function or constantEnglish
Let $r$ and $x$ be real numbers. Then $\operatorname{exponentialPDFReal}$ applied to $r$ and $x$ is a real number defined as $\operatorname{gammaPDFReal}$ applied to $1$, $r$ and $x$.
ContinuousLinearMap.rotationdefMathlib.Probability.Distributions.Fernique, function or constantWording
the rotation in x2 (from the docstring)
English
Let $x_{2}$ be a real number. Then the rotation in $x_{2}$ is a continuous linear map of $\mathrm{Prod}$ applied to $E$ and $E$ and $\mathrm{Prod}$ applied to $E$ and $E$.
ProbabilityTheory.Fernique.logRatiodefMathlib.Probability.Distributions.Fernique, function or constantWording
the logarithm ratio of c (from the name)
English
Let $c$ be an element of $\mathrm{ENNReal}$. Then the logarithm ratio of $c$ is a real number defined as the quotient of the logarithm of $\frac{ \operatorname{toReal} (c)}{\operatorname{toReal} (1 - c)}$ and the product of $8$ and the exponentiation of the sum of $1$ and the square root of $2$ to $2$.
ProbabilityTheory.Fernique.normThresholddefMathlib.Probability.Distributions.Fernique, function or constantWording
the norm threshold of a and x (from the name)
English
Let $a$ be a real number. Let $x$ be a natural number. Then the norm threshold of $a$ and $x$ is a real number defined as $\mathrm{arithGeom}$ applied to the square root of $2$, $a$, $a$ and $x$.
ProbabilityTheory.gammaMeasuredefMathlib.Probability.Distributions.Gamma, function or constantWording
the Gamma measure of a and r (from the name)
English
Let $a$ and $r$ be real numbers. Then the Gamma measure of $a$ and $r$ is a measure of $\Real$ defined as $\operatorname{withDensity}$ applied to the volume and $\operatorname{gammaPDF}$ applied to $r$.
ProbabilityTheory.gammaPDFdefMathlib.Probability.Distributions.Gamma, function or constantWording
the Gamma probability density function of r and x (from the name)
English
Let $a$, $r$ and $x$ be real numbers. Then the Gamma probability density function of $r$ and $x$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofReal}$ applied to $\operatorname{gammaPDFReal}$ applied to $a$, $r$ and $x$.
ProbabilityTheory.gammaPDFRealdefMathlib.Probability.Distributions.Gamma, function or constantEnglish
Let $a$, $r$ and $x$ be elements of $\Real$. Then $\operatorname{gammaPDFReal}$ applied to $a$, $r$ and $x$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Leq} (0 , x)}{(\frac{ r ^ {a}}{\operatorname{Gamma} (a)}\times x ^ {(a - 1)}\times \operatorname{exp} (\operatorname{neg} (r \times x)))}{0}$.
ProbabilityTheory.IsGaussianclassMathlib.Probability.Distributions.Gaussian.Basic, predicateWording
x3 is Gaussian (from the name)
English
Let $x_{3}$ be a measure of $E$. Then we can say that $x_{3}$ is Gaussian.
ProbabilityTheory.HasGaussianLawstructureMathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def, predicateEnglish
Let $X$ be a function from elements of $x$ to elements of $E$. Let $P$ be a measure of $x$. Then we can say that $\operatorname{HasGaussianLaw}$ holds for $X$ and $P$.
ProbabilityTheory.IsGaussianProcessstructureMathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def, predicateEnglish
Let $X$ be a function from elements of $T$ and elements of $x$ to elements of $E$. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_IsGaussianProcess\_\_\_auto\_1}$. Then we can say that $\operatorname{IsGaussianProcess}$ holds for $X$ and $P$.
ProbabilityTheory.multivariateGaussiandefMathlib.Probability.Distributions.Gaussian.Multivariate, function or constantEnglish
Let $x_{3}$ be a Euclidean space of $\Real$ and $x$. Let $S$ be a matrix of $x$ and $\Real$. Then $\operatorname{multivariateGaussian}$ applied to $x_{3}$ and $S$ is a measure of the set of Euclidean spaces of $\Real$ and $x$ defined as the map of the function that maps $x_{4}$ to the sum of $x_{3}$ and $\operatorname{coe}$ applied to the Euclidean continuous linear map, the square root of $S$ and $x_{4}$ and $\operatorname{stdGaussian}$ applied to the set of Euclidean spaces of $\Real$ and $x$.
ProbabilityTheory.stdGaussiandefMathlib.Probability.Distributions.Gaussian.Multivariate, function or constantEnglish
Let $E$ be a set. Then $\operatorname{stdGaussian}$ applied to $E$ is a measure of $E$ defined as the map of the function that maps $x_{3}$ to $\FinsetSum {\FinsetunivMACRoAC}{i}{(\HSMulhSMulMACRoAL {x_{3} (i)}{\operatorname{stdOrthonormalBasis} (\Real , E , i)})}$ and the finite product of the measures of the function that maps $x_{4}$ to $\operatorname{gaussianReal}$ applied to $0$ and $1$.
ProbabilityTheory.gaussianPDFdefMathlib.Probability.Distributions.Gaussian.Real, function or constantWording
the Gaussian probability density function of v and x1 (from the name)
English
Let $x$ and $x_{1}$ be real numbers. Let $v$ be an element of $\mathrm{NNReal}$. Then the Gaussian probability density function of $v$ and $x_{1}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofReal}$ applied to $\operatorname{gaussianPDFReal}$ applied to $x$, $v$ and $x_{1}$.
ProbabilityTheory.gaussianPDFRealdefMathlib.Probability.Distributions.Gaussian.Real, function or constantEnglish
Let $x$ and $x_{1}$ be real numbers. Let $v$ be an element of $\mathrm{NNReal}$. Then $\operatorname{gaussianPDFReal}$ applied to $x$, $v$ and $x_{1}$ is a real number defined as the product of $\operatorname{inv}$ applied to the square root of the product of $2$, the product and $\operatorname{toReal}$ applied to $v$ and the exponential of $\frac{ \operatorname{neg} ((x_{1} - x)^ {2})}{2 \times \operatorname{toReal} (v)}$.
ProbabilityTheory.gaussianRealdefMathlib.Probability.Distributions.Gaussian.Real, function or constantEnglish
Let $x$ be an element of $\Real$. Let $v$ be an element of $\mathrm{NNReal}$. Then $\operatorname{gaussianReal}$ applied to $x$ and $v$ is a measure of $\Real$ defined as $\iteMACRoG {(\EqtMACRoH {v}{0})}{\operatorname{dirac} (x)}{\operatorname{withDensity} (\operatorname{volume} , \operatorname{gaussianPDF} (v))}$.
ProbabilityTheory.geometricMeasuredefMathlib.Probability.Distributions.Geometric, function or constantWording
the geometric measure of p (from the name)
English
Let $p$ be an element of the unit interval. Then the geometric measure of $p$ is a measure of $\Natural$ defined as $\iteMACRoG {\mathrm{Neq} (p , 0)}{\operatorname{sum} (\lambda n . \HSMulhSMulMACRoAL {\operatorname{ofReal} ((1 - p)^ {n}\times p)}{\operatorname{dirac} (n)})}{\operatorname{dirac} (0)}$.
ProbabilityTheory.paretoMeasuredefMathlib.Probability.Distributions.Pareto, function or constantEnglish
Let $t$ and $r$ be real numbers. Then $\operatorname{paretoMeasure}$ applied to $t$ and $r$ is a measure of $\Real$ defined as $\operatorname{withDensity}$ applied to the volume and $\operatorname{paretoPDF}$ applied to $t$ and $r$.
ProbabilityTheory.paretoPDFdefMathlib.Probability.Distributions.Pareto, function or constantEnglish
Let $t$, $r$ and $x$ be real numbers. Then $\operatorname{paretoPDF}$ applied to $t$, $r$ and $x$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofReal}$ applied to $\operatorname{paretoPDFReal}$ applied to $t$, $r$ and $x$.
ProbabilityTheory.paretoPDFRealdefMathlib.Probability.Distributions.Pareto, function or constantEnglish
Let $t$, $r$ and $x$ be real numbers. Then $\operatorname{paretoPDFReal}$ applied to $t$, $r$ and $x$ is a real number defined as $\iteMACRoG {\mathrm{Leq} (t , x)}{(r \times t ^ {r}\times x ^ {\operatorname{neg} (r + 1)})}{0}$.
ProbabilityTheory.poissonMeasuredefMathlib.Probability.Distributions.Poisson.Basic, function or constantWording
the Poisson measure of r (from the name)
English
Let $r$ be an element of $\mathrm{NNReal}$. Then the Poisson measure of $r$ is a measure of $\Natural$ defined as the sum of the function that maps $n$ to $\HSMulhSMulMACRoAL {\operatorname{ofReal} (\frac{ \operatorname{exp} (\operatorname{neg} (\operatorname{toReal} (r)))\times \operatorname{toReal} (r)^ {n}}{n !})}{\operatorname{dirac} (n)}$.
ProbabilityTheory.IsSetBernoullidefMathlib.Probability.Distributions.SetBernoulli, predicateEnglish
Let $X$ be a function from elements of $x_{1}$ to elements of $\wp x$. Let $u$ be an element of $\wp x$. Let $p$ be an element of the unit interval. Let $P$ be a measure of $x_{1}$. Then $\operatorname{IsSetBernoulli}$ holds for $X$, $u$, $p$ and $P$, if $\operatorname{HasLaw}$ holds for $X$, $\operatorname{setBernoulli}$ applied to $u$ and $p$ and $P$.
ProbabilityTheory.setBernoullidefMathlib.Probability.Distributions.SetBernoulli, function or constantEnglish
Let $u$ be an element of $\wp x$. Let $p$ be an element of the unit interval. Then $\operatorname{setBernoulli}$ applied to $u$ and $p$ is a measure of $\wp x$ defined as the preimage of the function that maps $s$ and $i$ to $\MembershipmemMACRoT {s}{i}$ and the product measure of the function that maps $i_{1}$ to the Bernoulli measure of the proposition that we have a contradiction and $p$.
MeasureTheory.Measure.ofMultisetdefMathlib.Probability.Distributions.Uniform, function or constantWording
the measure of s (from the name)
English
Let $s$ be a multiset of $x$. Then the measure of $s$ is a measure of $x$ defined as $\FinsetSum {\operatorname{toFinset} (s)}{a}{(\HSMulhSMulMACRoAL {(\frac{ \operatorname{count} (a , s)}{\operatorname{card} (s)})}{\operatorname{dirac} (a)})}$.
ProbabilityTheory.HasCondDistribdefMathlib.Probability.HasCondDistrib, predicateEnglish
Let $Y$ be a function from elements of $x$ to elements of $x_{2}$. Let $X$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{6}$ be a kernel of $x_{1}$ and $x_{2}$. Let $P$ be a measure of $x$. Then $\operatorname{HasCondDistrib}$ holds for $Y$, $X$, $x_{6}$ and $P$, if $\operatorname{HasLaw}$ holds for the function that maps $x_{7}$ to $\ProdmkMACRoU {X (x_{7})}{Y (x_{7})}$, the composition product of the map of $X$ and $P$ and $x_{6}$ and $P$.
ProbabilityTheory.HasLawstructureMathlib.Probability.HasLaw, predicateEnglish
Let $X$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be a measure of $x_{1}$. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_HasLaw\_\_\_auto\_1}$. Then we can say that $\operatorname{HasLaw}$ holds for $X$, $x_{4}$ and $P$.
ProbabilityTheory.IdentDistribstructureMathlib.Probability.IdentDistrib, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $x_{6}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_IdentDistrib\_\_\_auto\_1}$. Let $x_{7}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{ProbabilityTheory\_\_IdentDistrib\_\_\_auto\_3}$. Then we can say that $\operatorname{IdentDistrib}$ holds for $f$, $g$, $x_{6}$ and $x_{7}$.
ProbabilityTheory.IndepdefMathlib.Probability.Independence.Basic, predicateWording
x4 is independent (from the name)
English
Assume that $x$ is a measurable space. Assume that $x$ is a measurable space. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Indep\_\_\_auto\_1}$. Then $x_{4}$ is independent, if the Dirac of $\operatorname{unit}$ is independent to the constant of $\mathrm{Unit}$ and $x_{4}$.
ProbabilityTheory.IndepFundefMathlib.Probability.Independence.Basic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{6}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_IndepFun\_\_\_auto\_1}$. Then $\operatorname{IndepFun}$ holds for $f$, $g$ and $x_{6}$, if $\operatorname{IndepFun}$ holds for $f$, $g$, the constant of $\mathrm{Unit}$ and $x_{6}$ and the Dirac of $\operatorname{unit}$.
ProbabilityTheory.IndepSetdefMathlib.Probability.Independence.Basic, predicateEnglish
Let $s$ and $t$ be elements of $\wp x$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_IndepSet\_\_\_auto\_1}$. Then $\operatorname{IndepSet}$ holds for $s$, $t$ and $x_{2}$, if $\operatorname{IndepSet}$ holds for $s$, $t$, the constant of $\mathrm{Unit}$ and $x_{2}$ and the Dirac of $\operatorname{unit}$.
ProbabilityTheory.IndepSetsdefMathlib.Probability.Independence.Basic, predicateEnglish
Let $s_{1}$ and $s_{2}$ be elements of $\wp (\wp x)$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_IndepSets\_\_\_auto\_1}$. Then $\operatorname{IndepSets}$ holds for $s_{1}$, $s_{2}$ and $x_{2}$, if $\operatorname{IndepSets}$ holds for $s_{1}$, $s_{2}$, the constant of $\mathrm{Unit}$ and $x_{2}$ and the Dirac of $\operatorname{unit}$.
ProbabilityTheory.iIndepdefMathlib.Probability.Independence.Basic, predicateWording
x3 is independent (from the name)
English
Assume that for all elements of $x_{1}$, $x$ is a measurable space. Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_iIndep\_\_\_auto\_1}$. Then $x_{3}$ is independent, if the constant of $\mathrm{Unit}$ and $x_{3}$ is independent to the Dirac of $\operatorname{unit}$.
ProbabilityTheory.iIndepFundefMathlib.Probability.Independence.Basic, predicateEnglish
Let $f$ be a function from elements $x_{5}$ of $x_{1}$ and elements of $x$ to elements of $x_{3}$ applied to $x_{5}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_iIndepFun\_\_\_auto\_1}$. Then $\operatorname{iIndepFun}$ holds for $x_{5}$, $f$ and $x_{4}$, if $\operatorname{iIndepFun}$ holds for $x_{5}$, the constant of $\mathrm{Unit}$ and $f$, the Dirac of $\operatorname{unit}$ and $x_{4}$.
ProbabilityTheory.iIndepSetdefMathlib.Probability.Independence.Basic, predicateWording
s is independent (from the docstring)
English
Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_iIndepSet\_\_\_auto\_1}$. Then $s$ is independent, if $s$ is independent.
ProbabilityTheory.iIndepSetsdefMathlib.Probability.Independence.Basic, predicateEnglish
Let $x_{3}$ be a function from elements of $x_{1}$ to elements of $\wp (\wp x)$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_iIndepSets\_\_\_auto\_1}$. Then $\operatorname{iIndepSets}$ holds for $x_{3}$ and $x_{4}$, if $\operatorname{iIndepSets}$ holds for $x_{3}$, the constant of $\mathrm{Unit}$ and $x_{4}$ and the Dirac of $\operatorname{unit}$.
ProbabilityTheory.CondIndepdefMathlib.Probability.Independence.Conditional, predicateEnglish
Assume that $x$ is a measurable space. Assume that $x$ is a measurable space. Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq x_{3}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_CondIndep\_\_\_auto\_1}$. Then $\operatorname{CondIndep}$ holds for $\mathrm{m'}$, $x_{1}$, $x_{2}$, $\mathrm{hm'}$ and $x_{4}$, if $\operatorname{trim}$ applied to $x_{4}$ and $\mathrm{hm'}$ is independent to the conditional exponential kernel of $x_{4}$ and $\mathrm{m'}$.
ProbabilityTheory.CondIndepFundefMathlib.Probability.Independence.Conditional, predicateEnglish
Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $g$ be a function from elements of $x$ to elements of $x_{3}$. Let $x_{6}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_CondIndepFun\_\_\_auto\_1}$. Then $\operatorname{CondIndepFun}$ holds for $\mathrm{m'}$, $\mathrm{hm'}$, $f$, $g$ and $x_{6}$, if $\operatorname{IndepFun}$ holds for $f$, $g$, the conditional exponential kernel of $x_{6}$ and $\mathrm{m'}$ and $\operatorname{trim}$ applied to $x_{6}$ and $\mathrm{hm'}$.
ProbabilityTheory.CondIndepSetdefMathlib.Probability.Independence.Conditional, predicateEnglish
Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq x_{1}$. Let $s$ and $t$ be elements of $\wp x$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_CondIndepSet\_\_\_auto\_1}$. Then $\operatorname{CondIndepSet}$ holds for $\mathrm{m'}$, $\mathrm{hm'}$, $s$, $t$ and $x_{2}$, if $\operatorname{IndepSet}$ holds for $s$, $t$, the conditional exponential kernel of $x_{2}$ and $\mathrm{m'}$ and $\operatorname{trim}$ applied to $x_{2}$ and $\mathrm{hm'}$.
ProbabilityTheory.CondIndepSetsdefMathlib.Probability.Independence.Conditional, predicateEnglish
Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq x_{1}$. Let $s_{1}$ and $s_{2}$ be elements of $\wp (\wp x)$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_CondIndepSets\_\_\_auto\_1}$. Then $\operatorname{CondIndepSets}$ holds for $\mathrm{m'}$, $\mathrm{hm'}$, $s_{1}$, $s_{2}$ and $x_{2}$, if $\operatorname{IndepSets}$ holds for $s_{1}$, $s_{2}$, the conditional exponential kernel of $x_{2}$ and $\mathrm{m'}$ and $\operatorname{trim}$ applied to $x_{2}$ and $\mathrm{hm'}$.
ProbabilityTheory.iCondIndepdefMathlib.Probability.Independence.Conditional, predicateEnglish
Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq x_{2}$. Assume that for all elements of $x_{1}$, $x$ is a measurable space. Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_iCondIndep\_\_\_auto\_1}$. Then $\operatorname{iCondIndep}$ holds for $\mathrm{m'}$, $\mathrm{hm'}$, $m$ and $x_{3}$, if the conditional exponential kernel of $x_{3}$ and $\mathrm{m'}$ is independent to $\operatorname{trim}$ applied to $x_{3}$ and $\mathrm{hm'}$.
ProbabilityTheory.iCondIndepFundefMathlib.Probability.Independence.Conditional, predicateEnglish
Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq x_{2}$. Let $f$ be a function from elements $x_{5}$ of $x_{1}$ and elements of $x$ to elements of $x_{3}$ applied to $x_{5}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_iCondIndepFun\_\_\_auto\_1}$. Then $\operatorname{iCondIndepFun}$ holds for $\mathrm{m'}$, $\mathrm{hm'}$, $x_{5}$, $f$ and $x_{4}$, if $\operatorname{iIndepFun}$ holds for $x_{5}$, the conditional exponential kernel of $f$ and $\mathrm{m'}$, $\operatorname{trim}$ applied to $f$ and $\mathrm{hm'}$ and $x_{4}$.
ProbabilityTheory.iCondIndepSetdefMathlib.Probability.Independence.Conditional, predicateWording
s is conditionally independent (from the docstring)
English
generation took over the time limit
ProbabilityTheory.iCondIndepSetsdefMathlib.Probability.Independence.Conditional, predicateEnglish
Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq x_{2}$. Let $x_{3}$ be a function from elements of $x_{1}$ to elements of $\wp (\wp x)$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_iCondIndepSets\_\_\_auto\_1}$. Then $\operatorname{iCondIndepSets}$ holds for $\mathrm{m'}$, $\mathrm{hm'}$, $x_{3}$ and $x_{4}$, if $\operatorname{iIndepSets}$ holds for $x_{3}$, the conditional exponential kernel of $x_{4}$ and $\mathrm{m'}$ and $\operatorname{trim}$ applied to $x_{4}$ and $\mathrm{hm'}$.
ProbabilityTheory.Kernel.IndepdefMathlib.Probability.Independence.Kernel.Indep, predicateWording
x7 is independent to x6 (from the name)
English
Assume that $x_{1}$ is a measurable space. Assume that $x_{1}$ is a measurable space. Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_Indep\_\_\_auto\_1}$. Then $x_{7}$ is independent to $x_{6}$, if $\operatorname{IndepSets}$ holds for $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a measurable set, $\operatorname{ofPred}$ applied to the function that maps $s_{1}$ to the proposition that $s_{1}$ is a measurable set, $x_{6}$ and $x_{7}$.
ProbabilityTheory.Kernel.IndepSetdefMathlib.Probability.Independence.Kernel.Indep, predicateEnglish
Let $s$ and $t$ be elements of $\wp x_{1}$. Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_IndepSet\_\_\_auto\_1}$. Then $\operatorname{IndepSet}$ holds for $s$, $t$, $x_{4}$ and $x_{5}$, if $x_{5}$ is independent to $x_{4}$.
ProbabilityTheory.Kernel.IndepSetsdefMathlib.Probability.Independence.Kernel.Indep, predicateEnglish
Let $s_{1}$ and $s_{2}$ be elements of $\wp (\wp x_{1})$. Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_IndepSets\_\_\_auto\_1}$. Then $\operatorname{IndepSets}$ holds for $s_{1}$, $s_{2}$, $x_{4}$ and $x_{5}$, if for all elements $t_{1}$ and $t_{2}$ of $\wp x_{1}$, if $t_{1}$ is an element of $s_{1}$, then if $t_{2}$ is an element of $s_{2}$, then $\operatorname{Eventually}$ holds for the function that maps $a$ to $\EqtMACRoH {\operatorname{coe} (x_{4} , a , \operatorname{inter} (t_{1} , t_{2}))}{(\operatorname{coe} (x_{4} , a , t_{1})\times \operatorname{coe} (x_{4} , a , t_{2}))}$ and $\operatorname{ae}$ applied to $x_{5}$.
ProbabilityTheory.Kernel.iIndepdefMathlib.Probability.Independence.Kernel.Indep, predicateWording
x5 is independent to x6 (from the name)
English
Assume that for all elements of $x_{2}$, $x_{1}$ is a measurable space. Let $x_{5}$ be a kernel of $x$ and $x_{1}$. Let $x_{6}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_iIndep\_\_\_auto\_1}$. Then $x_{5}$ is independent to $x_{6}$, if $\operatorname{iIndepSets}$ holds for the function that maps $x_{7}$ to $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a measurable set, $x_{5}$ and $x_{6}$.
ProbabilityTheory.Kernel.iIndepSetdefMathlib.Probability.Independence.Kernel.Indep, predicateWording
s is independent (from the docstring)
English
Let $s$ be a function from elements of $x_{2}$ to elements of $\wp x_{1}$. Let $x_{5}$ be a kernel of $x$ and $x_{1}$. Let $x_{6}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_iIndepSet\_\_\_auto\_1}$. Then $s$ is independent, if $x_{5}$ is independent to $x_{6}$.
ProbabilityTheory.Kernel.iIndepSetsdefMathlib.Probability.Independence.Kernel.Indep, predicateEnglish
Let $x_{5}$ be a function from elements of $x_{2}$ to elements of $\wp (\wp x_{1})$. Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_iIndepSets\_\_\_auto\_1}$. Then $\operatorname{iIndepSets}$ holds for $x_{5}$, $x_{6}$ and $x_{7}$, if for all finite sets $s$ of $x_{2}$, for all functions $f$ from elements of $x_{2}$ to elements of $\wp x_{1}$, if for all elements $i_{2}$ of $x_{2}$, if $i_{2}$ is an element of $s$, then $\MembershipmemMACRoT {x_{5} (i_{2})}{f (i_{2})}$, then $\operatorname{Eventually}$ holds for the function that maps $a$ to the proposition that $\operatorname{coe}$ applied to $x_{6}$, $a$ and the intersection of the function that maps $i$ to the intersection of the function that maps $h$ to $f$ applied to $i$ is equal to $\FinsetProd {s}{i_{1}}{\operatorname{coe} (x_{6} , a , f (i_{1}))}$ and $\operatorname{ae}$ applied to $x_{7}$.
ProbabilityTheory.Kernel.IndepFundefMathlib.Probability.Independence.Kernel.IndepFun, predicateEnglish
Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x_{3}$. Let $x_{8}$ be a kernel of $x$ and $x_{1}$. Let $x_{9}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_IndepFun\_\_\_auto\_1}$. Then $\operatorname{IndepFun}$ holds for $f$, $g$, $x_{8}$ and $x_{9}$, if $x_{9}$ is independent to $x_{8}$.
ProbabilityTheory.Kernel.iIndepFundefMathlib.Probability.Independence.Kernel.IndepFun, predicateEnglish
Let $f$ be a function from elements $x_{8}$ of $x_{2}$ and elements of $x_{1}$ to elements of $x_{5}$ applied to $x_{8}$. Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_iIndepFun\_\_\_auto\_1}$. Then $\operatorname{iIndepFun}$ holds for $x_{8}$, $f$, $x_{6}$ and $x_{7}$, if $f$ is independent to $x_{6}$.
ProbabilityTheory.HasIndepIncrementsdefMathlib.Probability.Independence.Process.HasIndepIncrements.Basic, predicateEnglish
Let $X$ be a function from elements of $T$ and elements of $x$ to elements of $E$. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_HasIndepIncrements\_\_\_auto\_1}$. Then $\operatorname{HasIndepIncrements}$ holds for $X$ and $P$, if for all natural numbers $n$, for all functions $t$ from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $T$, if $t$ is monotone, then $\operatorname{iIndepFun}$ holds for the function that maps $i$ and $x_{5}$ to $X (t (\operatorname{succ} (i)), x_{5})- X (t (\operatorname{castSucc} (i)), x_{5})$ and $P$.
ProbabilityTheory.Kernel.boolKerneldefMathlib.Probability.Kernel.Basic, function or constantWording
the bool kernel of x2 and x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Then the bool kernel of $x_{2}$ and $x_{3}$ is a kernel of $\mathrm{Bool}$ and $x$.
ProbabilityTheory.Kernel.comapRightdefMathlib.Probability.Kernel.Basic, function or constantWording
the right preimage of x6 and hf (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Assume that $f$ is a measurable embedding. Then the right preimage of $x_{6}$ and $\mathrm{hf}$ is a kernel of $x$ and $x_{4}$.
ProbabilityTheory.Kernel.constdefMathlib.Probability.Kernel.Basic, function or constantWording
the constant of x and x4 (from the name)
English
Let $x$ be a set. Let $x_{4}$ be a measure of $x_{1}$. Then the constant of $x$ and $x_{4}$ is a kernel of $x$ and $x_{1}$.
ProbabilityTheory.Kernel.copydefMathlib.Probability.Kernel.Basic, function or constantWording
the copy of x (from the name)
English
Let $x$ be a set. Then the copy of $x$ is a kernel of $x$ and $\mathrm{Prod}$ applied to $x$ and $x$.
ProbabilityTheory.Kernel.deterministicdefMathlib.Probability.Kernel.Basic, function or constantEnglish
Let $f$ be a measurable function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{deterministic}$ applied to $f$ and $\mathrm{hf}$ is a kernel of $x$ and $x_{1}$.
ProbabilityTheory.Kernel.discarddefMathlib.Probability.Kernel.Basic, function or constantEnglish
Let $x$ be a set. Then $\operatorname{discard}$ applied to $x$ is a kernel of $x$ and $\mathrm{PUnit}$ defined as $\operatorname{deterministic}$ applied to the function that maps $x_{2}$ to $\operatorname{unit}$ and $\mathrm{measurable\_const}$.
ProbabilityTheory.Kernel.iddefMathlib.Probability.Kernel.Basic, function or constantWording
the identity (from the name)
English
The identity is a kernel of $x$ and $x$ defined as $\operatorname{deterministic}$ applied to $\mathrm{id}$ and $\mathrm{measurable\_id}$.
ProbabilityTheory.Kernel.ofFunOfCountabledefMathlib.Probability.Kernel.Basic, function or constantWording
the kernel of f (from the name)
English
Let $f$ be a function from elements of $x$ to measures of $x_{1}$. Then the kernel of $f$ is a kernel of $x$ and $x_{1}$.
ProbabilityTheory.Kernel.piecewisedefMathlib.Probability.Kernel.Basic, function or constantEnglish
Assume that $s$ is a measurable set. Let $x_{5}$ and $x_{6}$ be kernels of $x$ and $x_{1}$. Then $\operatorname{piecewise}$ applied to $\mathrm{hs}$, $x_{5}$ and $x_{6}$ is a kernel of $x$ and $x_{1}$.
ProbabilityTheory.Kernel.restrictdefMathlib.Probability.Kernel.Basic, function or constantEnglish
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Assume that $s$ is a measurable set. Then $\operatorname{restrict}$ applied to $x_{4}$ and $\mathrm{hs}$ is a kernel of $x$ and $x_{1}$.
ProbabilityTheory.Kernel.swapdefMathlib.Probability.Kernel.Basic, function or constantWording
the swap of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the swap of $x$ and $x_{1}$ is a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$ defined as $\operatorname{deterministic}$ applied to $\operatorname{swap}$ and $\mathrm{measurable\_swap}$.
SFinKerstructureMathlib.Probability.Kernel.Category.SFinKer, typeWording
finite kernel (from the name)
English
The finite kernels are a basic type.
SFinKer.HomstructureMathlib.Probability.Kernel.Category.SFinKer, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be finite kernels. Then the homomorphisms of $X$ and $Y$ are a basic type.
SFinKer.Hom.homdefMathlib.Probability.Kernel.Category.SFinKer, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a kernel of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
SFinKer.carrierdefMathlib.Probability.Kernel.Category.SFinKer, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a finite kernel. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
StochdefMathlib.Probability.Kernel.Category.Stoch, typeEnglish
An element of $\mathrm{Stoch}$ is a wide subcategory of $\mathrm{StochHom}$.
StochHomdefMathlib.Probability.Kernel.Category.Stoch, function or constantEnglish
There is a morphism property of the set of finite kernels. Proof. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. By x2. By SFinKer__Hom__hom. By ProbabilityTheory__IsMarkovKernel.
ProbabilityTheory.Kernel.compdefMathlib.Probability.Kernel.Composition.Comp, function or constantWording
the composition of x6 and x7 (from the name)
English
Let $x_{6}$ be a kernel of $x_{1}$ and $x_{2}$. Let $x_{7}$ be a kernel of $x$ and $x_{1}$. Then the composition of $x_{6}$ and $x_{7}$ is a kernel of $x$ and $x_{2}$.
ProbabilityTheory.Kernel.compProddefMathlib.Probability.Kernel.Composition.CompProd, function or constantWording
the composition product of x6 and x7 (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$. Then the composition product of $x_{6}$ and $x_{7}$ is a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_Kernel\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_Composition\_\_CompProd\_\_1128663877\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{6}$ and $x_{7}$.
ProbabilityTheory.Kernel.comapdefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the preimage of x6 and g (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $g$ be a measurable function from elements of $x_{4}$ to elements of $x$. Then the preimage of $x_{6}$ and $g$ is a kernel of $x_{4}$ and $x_{1}$.
ProbabilityTheory.Kernel.fstdefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the first component of x6 (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then the first component of $x_{6}$ is a kernel of $x$ and $x_{1}$ defined as the map of $x_{6}$ and $\ProdfstMACRoZ$.
ProbabilityTheory.Kernel.mapdefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the map of x6 and f (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x_{4}$. Then the map of $x_{6}$ and $f$ is a kernel of $x$ and $x_{4}$ defined as $\mathrm{dite}$ applied to the proposition that $f$ is measurable, the function that maps $\mathrm{hf}$ to the map of $x_{6}$ and $f$ and the function that maps $\mathrm{hf1}$ to $0$.
ProbabilityTheory.Kernel.mapOfMeasurabledefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the map of x6 and f (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $f$ be a measurable function from elements of $x_{1}$ to elements of $x_{4}$. Then the map of $x_{6}$ and $f$ is a kernel of $x$ and $x_{4}$.
ProbabilityTheory.Kernel.prodMkLeftdefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the left product of x4 and x6 (from the name)
English
Let $x_{4}$ be a set. Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Then the left product of $x_{4}$ and $x_{6}$ is a kernel of $\mathrm{Prod}$ applied to $x_{4}$ and $x$ and $x_{1}$ defined as the preimage of $x_{6}$ and $\ProdsndMACRoAA$.
ProbabilityTheory.Kernel.prodMkRightdefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the right product of x4 and x6 (from the name)
English
Let $x_{4}$ be a set. Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Then the right product of $x_{4}$ and $x_{6}$ is a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{4}$ and $x_{1}$ defined as the preimage of $x_{6}$ and $\ProdfstMACRoZ$.
ProbabilityTheory.Kernel.sectLdefMathlib.Probability.Kernel.Composition.MapComap, function or constantEnglish
Let $x_{6}$ be a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{4}$. Let $b$ be an element of $x_{1}$. Then $\operatorname{sectL}$ applied to $x_{6}$ and $b$ is a kernel of $x$ and $x_{4}$.
ProbabilityTheory.Kernel.sectRdefMathlib.Probability.Kernel.Composition.MapComap, function or constantEnglish
Let $x_{6}$ be a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{4}$. Let $a$ be an element of $x$. Then $\operatorname{sectR}$ applied to $x_{6}$ and $a$ is a kernel of $x_{1}$ and $x_{4}$.
ProbabilityTheory.Kernel.snddefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the second component of x6 (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then the second component of $x_{6}$ is a kernel of $x$ and $x_{2}$ defined as the map of $x_{6}$ and $\ProdsndMACRoAA$.
ProbabilityTheory.Kernel.swapLeftdefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the left swap of x6 (from the name)
English
Let $x_{6}$ be a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$. Then the left swap of $x_{6}$ is a kernel of $\mathrm{Prod}$ applied to $x_{1}$ and $x$ and $x_{2}$ defined as the preimage of $x_{6}$ and $\operatorname{swap}$.
ProbabilityTheory.Kernel.swapRightdefMathlib.Probability.Kernel.Composition.MapComap, function or constantWording
the right swap of x6 (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then the right swap of $x_{6}$ is a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{1}$ defined as the map of $x_{6}$ and $\operatorname{swap}$.
MeasureTheory.Measure.compProddefMathlib.Probability.Kernel.Composition.MeasureCompProd, function or constantWording
the composition product of x4 and x5 (from the name)
English
Let $x_{4}$ be a measure of $x$. Let $x_{5}$ be a kernel of $x$ and $x_{1}$. Then the composition product of $x_{4}$ and $x_{5}$ is a measure of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{compProd}$ applied to the constant of $\mathrm{Unit}$ and $x_{4}$, the left product of $\mathrm{Unit}$ and $x_{5}$ and $\operatorname{unit}$.
ProbabilityTheory.Kernel.parallelCompdefMathlib.Probability.Kernel.Composition.ParallelComp, function or constantWording
the parallel composition of x8 and x9 (from the name)
English
Let $x_{8}$ be a kernel of $x$ and $x_{1}$. Let $x_{9}$ be a kernel of $x_{2}$ and $x_{3}$. Then the parallel composition of $x_{8}$ and $x_{9}$ is a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_Kernel\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_Composition\_\_ParallelComp\_\_4290254366\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{8}$ and $x_{9}$.
ProbabilityTheory.Kernel.proddefMathlib.Probability.Kernel.Composition.Prod, function or constantWording
the product of x6 and x7 (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $x_{1}$. Let $x_{7}$ be a kernel of $x$ and $x_{4}$. Then the product of $x_{6}$ and $x_{7}$ is a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{4}$ defined as the composition of the parallel composition of $x_{6}$ and $x_{7}$ and the copy of $x$.
ProbabilityTheory.condDistribdefMathlib.Probability.Kernel.CondDistrib, function or constantEnglish
Let $Y$ be a function from elements of $x$ to elements of $x_{2}$. Let $X$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{6}$ be a measure of $x$. Then $\operatorname{condDistrib}$ applied to $Y$, $X$ and $x_{6}$ is a kernel of $x_{1}$ and $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_CondDistrib\_\_2261733823\_\_\_hygCtx\_\_\_hyg\_\_2}$, $Y$, $X$ and $x_{6}$.
ProbabilityTheory.condExpKerneldefMathlib.Probability.Kernel.Condexp, function or constantWording
the conditional exponential kernel of x2 and m (from the name)
English
Let $x_{2}$ be a measure of $x$. Assume that $x$ is a measurable space. Then the conditional exponential kernel of $x_{2}$ and $m$ is a kernel of $x$ and $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_Condexp\_\_1252835584\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{2}$ and $m$.
ProbabilityTheory.IsFiniteKernelclassMathlib.Probability.Kernel.Defs, predicateWording
x4 is finite (from the docstring)
English
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Then we can say that $x_{4}$ is finite.
ProbabilityTheory.IsMarkovKernelclassMathlib.Probability.Kernel.Defs, predicateWording
x4 is a Markov kernel (from the name)
English
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Then we can say that $x_{4}$ is a Markov kernel.
ProbabilityTheory.IsSFiniteKernelclassMathlib.Probability.Kernel.Defs, predicateWording
x4 is a finite kernel (from the name)
English
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Then we can say that $x_{4}$ is a finite kernel.
ProbabilityTheory.IsZeroOrMarkovKernelclassMathlib.Probability.Kernel.Defs, predicateEnglish
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Then we can say that $\operatorname{IsZeroOrMarkovKernel}$ holds for $x_{4}$.
ProbabilityTheory.KernelstructureMathlib.Probability.Kernel.Defs, typeWording
kernel of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the kernels of $x$ and $x_{1}$ are a basic type.
ProbabilityTheory.Kernel.bounddefMathlib.Probability.Kernel.Defs, function or constantWording
the bound of x4 (from the name)
English
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Then the bound of $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $a$ to $\operatorname{coe}$ applied to $x_{4}$, $a$ and the universal set.
ProbabilityTheory.Kernel.seqdefMathlib.Probability.Kernel.Defs, function or constantWording
the sequence of x4 and x5 (from the name)
English
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Let $x_{5}$ be a natural number. Then the sequence of $x_{4}$ and $x_{5}$ is a kernel of $x$ and $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{ProbabilityTheory\_\_IsSFiniteKernel\_\_tsum\_finite}$ and $x_{5}$.
ProbabilityTheory.Kernel.sumdefMathlib.Probability.Kernel.Defs, function or constantWording
the sum of x5 (from the name)
English
Let $x_{5}$ be a function from elements of $x_{2}$ to kernels of $x$ and $x_{1}$. Then the sum of $x_{5}$ is a kernel of $x$ and $x_{1}$.
ProbabilityTheory.Kernel.toFundefMathlib.Probability.Kernel.Defs, function or constantWording
the underlying function of self and x4 (from the docstring)
English
Let $\mathrm{self}$ be a kernel of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the underlying function of $\mathrm{self}$ and $x_{4}$ is a measure of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
ProbabilityTheory.IsDeterministicclassMathlib.Probability.Kernel.Deterministic, predicateWording
x4 is deterministic (from the docstring)
English
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Then we can say that $x_{4}$ is deterministic.
MeasureTheory.Measure.IsCondKernelclassMathlib.Probability.Kernel.Disintegration.Basic, predicateEnglish
Let $x_{4}$ be a measure of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Let $x_{5}$ be a kernel of $x$ and $x_{1}$. Then we can say that $\operatorname{IsCondKernel}$ holds for $x_{4}$ and $x_{5}$.
ProbabilityTheory.Kernel.IsCondKernelclassMathlib.Probability.Kernel.Disintegration.Basic, predicateEnglish
Let $x_{6}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Let $x_{7}$ be a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{IsCondKernel}$ holds for $x_{6}$ and $x_{7}$.
ProbabilityTheory.IsCondKernelCDFstructureMathlib.Probability.Kernel.Disintegration.CDFToKernel, predicateEnglish
Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ to Stieltjes functions of $\Real$. Let $x_{4}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\Real$. Let $x_{5}$ be a kernel of $x$ and $x_{1}$. Then we can say that $\operatorname{IsCondKernelCDF}$ holds for $f$, $x_{4}$ and $x_{5}$.
ProbabilityTheory.IsCondKernelCDF.toKerneldefMathlib.Probability.Kernel.Disintegration.CDFToKernel, function or constantWording
the kernel of f and hf (from the name)
English
Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ to Stieltjes functions of $\Real$ such that $\operatorname{IsCondKernelCDF}$ holds for $f$, $x_{4}$ and $x_{5}$. Then the kernel of $f$ and $\mathrm{hf}$ is a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\Real$.
ProbabilityTheory.IsRatCondKernelCDFstructureMathlib.Probability.Kernel.Disintegration.CDFToKernel, predicateEnglish
Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and rational numbers to real numbers. Let $x_{4}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\Real$. Let $x_{5}$ be a kernel of $x$ and $x_{1}$. Then we can say that $\operatorname{IsRatCondKernelCDF}$ holds for $f$, $x_{4}$ and $x_{5}$.
MeasureTheory.Measure.IicSnddefMathlib.Probability.Kernel.Disintegration.CondCDF, function or constantEnglish
Let $x_{2}$ be a measure of $\mathrm{Prod}$ applied to $x$ and $\Real$. Let $r$ be a real number. Then $\operatorname{IicSnd}$ applied to $x_{2}$ and $r$ is a measure of $x$ defined as the first component of $\operatorname{restrict}$ applied to $x_{2}$ and $\operatorname{sprod}$ applied to the universal set and $\operatorname{Iic}$ applied to $r$.
ProbabilityTheory.condCDFdefMathlib.Probability.Kernel.Disintegration.CondCDF, function or constantWording
the conditional cumulative distribution function of x2 and a (from the name)
English
Let $x_{2}$ be a measure of $\mathrm{Prod}$ applied to $x$ and $\Real$. Let $a$ be an element of $x$. Then the conditional cumulative distribution function of $x_{2}$ and $a$ is a Stieltjes function of $\Real$ defined as the Stieltjes of the function that maps $a_{1}$ and $r$ to $\operatorname{toReal}$ applied to the cumulative distribution function of $r$ and $a_{1}$ and $a$.
ProbabilityTheory.preCDFdefMathlib.Probability.Kernel.Disintegration.CondCDF, function or constantWording
the cumulative distribution function of r and x3 (from the name)
English
Let $x_{2}$ be a measure of $\mathrm{Prod}$ applied to $x$ and $\Real$. Let $r$ be a rational number. Let $x_{3}$ be an element of $x$. Then the cumulative distribution function of $r$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{rnDeriv}$ applied to $\operatorname{IicSnd}$ applied to $x_{2}$ and $\operatorname{cast}$ applied to $r$, the first component of $x_{2}$ and $x_{3}$.
ProbabilityTheory.Kernel.densitydefMathlib.Probability.Kernel.Disintegration.Density, function or constantWording
the density of x8 and s (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{1}$. Let $x_{7}$ be a kernel of $x$ and $x_{2}$. Let $a$ be an element of $x$. Let $x_{8}$ be an element of $x_{2}$. Let $s$ be an element of $\wp x_{1}$. Then the density of $x_{8}$ and $s$ is a real number defined as the limsup of the function that maps $n$ to the density process of $x_{8}$ and $s$ and $\operatorname{atTop}$.
ProbabilityTheory.Kernel.densityProcessdefMathlib.Probability.Kernel.Disintegration.Density, function or constantWording
the density process of x8 and s (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{1}$. Let $x_{7}$ be a kernel of $x$ and $x_{2}$. Let $n$ be a natural number. Let $a$ be an element of $x$. Let $x_{8}$ be an element of $x_{2}$. Let $s$ be an element of $\wp x_{1}$. Then the density process of $x_{8}$ and $s$ is a real number defined as $\operatorname{toReal}$ applied to the quotient of $\operatorname{coe}$ applied to $x_{6}$, $a$ and $\operatorname{sprod}$ applied to the countable partition set of $n$ and $x_{8}$ and $s$ and $\operatorname{coe}$ applied to $x_{7}$, $a$ and the countable partition set of $n$ and $x_{8}$.
ProbabilityTheory.IsMeasurableRatCDFstructureMathlib.Probability.Kernel.Disintegration.MeasurableStieltjes, predicateWording
f is a measurable rational number cumulative distribution function (from the name)
English
Let $f$ be a function from elements of $x$ and rational numbers to real numbers. Then we can say that $f$ is a measurable rational number cumulative distribution function.
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctiondefMathlib.Probability.Kernel.Disintegration.MeasurableStieltjes, function or constantWording
the Stieltjes function of hf and a (from the name)
English
Assume that $f$ is a measurable rational number cumulative distribution function. Let $a$ be an element of $x$. Then the Stieltjes function of $\mathrm{hf}$ and $a$ is a Stieltjes function of $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{stieltjesFunctionAux}$ applied to $f$ and $a$, $\mathrm{ProbabilityTheory\_\_IsMeasurableRatCDF\_\_monotone\_stieltjesFunctionAux}$ applied to $\mathrm{hf}$ and $a$ and the function that maps $x_{2}$ to $\mathrm{ProbabilityTheory\_\_IsMeasurableRatCDF\_\_continuousWithinAt\_stieltjesFunctionAux\_Ici}$ applied to $\mathrm{hf}$, $a$ and $x_{2}$.
ProbabilityTheory.IsRatStieltjesPointstructureMathlib.Probability.Kernel.Disintegration.MeasurableStieltjes, predicateEnglish
Let $f$ be a function from elements of $x$ and rational numbers to real numbers. Let $a$ be an element of $x$. Then we can say that $\operatorname{IsRatStieltjesPoint}$ holds for $f$ and $a$.
ProbabilityTheory.defaultRatCDFdefMathlib.Probability.Kernel.Disintegration.MeasurableStieltjes, function or constantWording
the default rational number cumulative distribution function of q (from the name)
English
Let $q$ be a rational number. Then the default rational number cumulative distribution function of $q$ is a real number defined as $\iteMACRoG {\mathrm{Lt} (q , 0)}{0}{1}$.
ProbabilityTheory.stieltjesOfMeasurableRatdefMathlib.Probability.Kernel.Disintegration.MeasurableStieltjes, function or constantWording
the Stieltjes of f and x2 (from the name)
English
Let $f$ be a measurable function from elements of $x$ and rational numbers to real numbers. Let $x_{2}$ be an element of $x$. Then the Stieltjes of $f$ and $x_{2}$ is a Stieltjes function of $\Real$ defined as the Stieltjes function of $\mathrm{ProbabilityTheory\_\_isMeasurableRatCDF\_toRatCDF}$ applied to $\mathrm{hf}$ and $x_{2}$.
ProbabilityTheory.toRatCDFdefMathlib.Probability.Kernel.Disintegration.MeasurableStieltjes, function or constantWording
the rational number cumulative distribution function of x1 and x2 (from the name)
English
Let $f$ be a function from elements of $x$ and elements of $\Rational$ to elements of $\Real$. Let $x_{1}$ be an element of $x$. Let $x_{2}$ be an element of $\Rational$. Then the rational number cumulative distribution function of $x_{1}$ and $x_{2}$ is an element of $\Real$ defined as $\iteMACRoG {\operatorname{IsRatStieltjesPoint} (f , x_{1})}{f (x_{1})}{\operatorname{defaultRatCDF}}$.
MeasureTheory.Measure.condKerneldefMathlib.Probability.Kernel.Disintegration.StandardBorel, function or constantWording
the conditional kernel of x4 (from the name)
English
Let $x_{4}$ be a measure of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the conditional kernel of $x_{4}$ is a kernel of $x$ and $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_Kernel\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_Disintegration\_\_StandardBorel\_\_275338330\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $x_{4}$.
ProbabilityTheory.Kernel.condKerneldefMathlib.Probability.Kernel.Disintegration.StandardBorel, function or constantWording
the conditional kernel of x6 (from the name)
English
Let $x_{6}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$. Then the conditional kernel of $x_{6}$ is a kernel of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_Kernel\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_Disintegration\_\_StandardBorel\_\_367213062\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $x_{6}$.
ProbabilityTheory.Kernel.condKernelCDFdefMathlib.Probability.Kernel.Disintegration.StandardBorel, function or constantWording
the conditional kernel cumulative distribution function of x4 and x5 (from the name)
English
Let $x_{4}$ be a kernel of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\Real$. Let $x_{5}$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the conditional kernel cumulative distribution function of $x_{4}$ and $x_{5}$ is a Stieltjes function of $\Real$.
ProbabilityTheory.Kernel.InvariantdefMathlib.Probability.Kernel.Invariance, predicateEnglish
Let $x_{2}$ be a kernel of $x$ and $x$. Let $x_{3}$ be a measure of $x$. Then $\operatorname{Invariant}$ holds for $x_{2}$ and $x_{3}$, if $\operatorname{bind}$ applied to $x_{3}$ and $\operatorname{coe}$ applied to $x_{2}$ is equal to $x_{3}$.
ProbabilityTheory.Kernel.IsReversibledefMathlib.Probability.Kernel.Invariance, predicateWording
x2 is reversible with respect to x3 (from the name)
English
Let $x_{2}$ be a kernel of $x$ and $x$. Let $x_{3}$ be a measure of $x$. Then $x_{2}$ is reversible with respect to $x_{3}$, if for all elements $A$ and $B$ of $\wp x$, if $A$ is a measurable set, then if $B$ is a measurable set, then $\EqtMACRoH {\operatorname{lintegral} (\operatorname{restrict} (x_{3} , A), \lambda x_{4} . \operatorname{coe} (x_{2} , x_{4} , B))}{\operatorname{lintegral} (\operatorname{restrict} (x_{3} , B), \lambda x_{5} . \operatorname{coe} (x_{2} , x_{5} , A))}$.
IicProdIocdefMathlib.Probability.Kernel.IonescuTulcea.Maps, function or constantEnglish
Let $a$ and $b$ be elements of $x$. Let $x_{5}$ be an element of $\mathrm{Prod}$ applied to the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{7}})}$ to elements of $X$ applied to $i_{1}$ and the set of functions from elements $i_{2}$ of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {(\FinsetIocMACRoAI {a}{b})}{x_{8}})}$ to elements of $X$ applied to $i_{2}$. Let $i$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {b}}{x_{6}})}$. Then $\mathrm{IicProdIoc}$ applied to $a$, $b$, $x_{5}$ and $i$ is an element of $X$ applied to $i$ defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (i , a)$, the function that maps $h$ to $\ProdfstMACRoZ {x_{5}}$ and the function that maps $h_{1}$ to $\ProdsndMACRoAA {x_{5}}$.
IocProdIocdefMathlib.Probability.Kernel.IonescuTulcea.Maps, function or constantEnglish
Let $a$, $b$ and $c$ be elements of $x$. Let $x_{4}$ be an element of $\mathrm{Prod}$ applied to the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {(\FinsetIocMACRoAI {a}{b})}{x_{6}})}$ to elements of $X$ applied to $i_{1}$ and the set of functions from elements $i_{2}$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {(\FinsetIocMACRoAI {b}{c})}{x_{7}})}$ to elements of $X$ applied to $i_{2}$. Let $i$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {(\FinsetIocMACRoAI {a}{c})}{x_{5}})}$. Then $\mathrm{IocProdIoc}$ applied to $a$, $b$, $c$, $x_{4}$ and $i$ is an element of $X$ applied to $i$ defined as $\mathrm{dite}$ applied to $\mathrm{Leq} (i , b)$, the function that maps $h$ to $\ProdfstMACRoZ {x_{4}}$ and the function that maps $h_{1}$ to $\ProdsndMACRoAA {x_{4}}$.
MeasurableEquiv.IicProdIocdefMathlib.Probability.Kernel.IonescuTulcea.Maps, function or constantEnglish
Assume that $a \leq b$. Then $\operatorname{IicProdIoc}$ applied to $\mathrm{hab}$ is a measurable equivalence of $\mathrm{Prod}$ applied to the set of functions from elements $i$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{6}})}$ to elements of $X$ applied to $i$ and the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {(\FinsetIocMACRoAI {a}{b})}{x_{7}})}$ to elements of $X$ applied to $i_{1}$ and the set of functions from elements $i_{2}$ of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {b}}{x_{8}})}$ to elements of $X$ applied to $i_{2}$.
MeasurableEquiv.IicProdIoidefMathlib.Probability.Kernel.IonescuTulcea.Maps, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{IicProdIoi}$ applied to $a$ is a measurable equivalence of $\mathrm{Prod}$ applied to the set of functions from elements $i$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{5}})}$ to elements of $X$ applied to $i$ and the set of functions from elements $i_{1}$ of $\operatorname{Ioi}$ applied to $a$ to elements of $X$ applied to $i_{1}$ and the set of functions from elements $n$ of $x$ to elements of $X$ applied to $n$.
MeasurableEquiv.piSingletondefMathlib.Probability.Kernel.IonescuTulcea.Maps, function or constantWording
the product singleton of a (from the name)
English
Let $a$ be a natural number. Then the product singleton of $a$ is a measurable equivalence of $X$ applied to $a + 1$ and the set of functions from elements $i$ of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {(\FinsetIocMACRoAI {a}{(a + 1)})}{x_{1}})}$ to elements of $X$ applied to $i$.
ProbabilityTheory.Kernel.lmarginalPartialTrajdefMathlib.Probability.Kernel.IonescuTulcea.PartialTraj, function or constantEnglish
Let $x$ be a function from natural numbers $n_{2}$ to kernels of the set of functions from elements $i$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n_{2}}}{x_{3}})}$ to elements of $X$ applied to $i$ and $X$ applied to $n_{2} + 1$. Let $a$ and $b$ be natural numbers. Let $f$ be a function from functions from natural numbers $n_{1}$ to elements of $X$ applied to $n_{1}$ to elements of $\mathrm{ENNReal}$. Let $x_{1}$ be a function from natural numbers $n$ to elements of $X$ applied to $n$. Then $\operatorname{lmarginalPartialTraj}$ applied to $n_{2}$, $x$, $a$, $b$, $f$, $n$ and $x_{1}$ is an element of $\mathrm{ENNReal}$ defined as the function that maps $n$ and $x_{1}$ to $\operatorname{lintegral}$ applied to $\operatorname{partialTraj}$ applied to $n_{2}$, $x$, $a$ and $\operatorname{frestrictLe}$ applied to $x$ and $f$, the function that maps $z$ to $b$ applied to $\operatorname{updateFinset}$ applied to $f$, $\FinsetIicMACRoAJ {a}$ and $z$, $n$ and $x_{1}$.
ProbabilityTheory.Kernel.partialTrajdefMathlib.Probability.Kernel.IonescuTulcea.PartialTraj, function or constantEnglish
Let $x$ be a function from natural numbers $n$ to kernels of the set of functions from elements $i_{2}$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n}}{x_{3}})}$ to elements of $X$ applied to $i_{2}$ and $X$ applied to $n + 1$. Let $a$ and $b$ be natural numbers. Then $\operatorname{partialTraj}$ applied to $n$, $x$, $a$ and $b$ is a kernel of the set of functions from elements $i$ of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{1}})}$ to elements of $X$ applied to $i$ and the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {b}}{x_{2}})}$ to elements of $X$ applied to $i_{1}$.
MeasureTheory.inducedFamilydefMathlib.Probability.Kernel.IonescuTulcea.Traj, function or constantWording
the induced family of x1 and n (from the name)
English
Let $x_{1}$ be a function from natural numbers $n$ to measures of the set of functions from elements $i$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n}}{x_{3}})}$ to elements of $X$ applied to $i$. Let $S$ be a finite set of $\Natural$. Then the induced family of $n$ and $x_{1}$ is a measure of the set of functions from elements $k$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {S}{x_{2}})}$ to elements of $X$ applied to $k$.
ProbabilityTheory.Kernel.trajdefMathlib.Probability.Kernel.IonescuTulcea.Traj, function or constantEnglish
Let $x_{1}$ be a function from natural numbers $n_{1}$ to kernels of the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n_{1}}}{x_{3}})}$ to elements of $X$ applied to $i_{1}$ and $X$ applied to $n_{1} + 1$. Let $a$ be a natural number. Then $\operatorname{traj}$ applied to $n_{1}$, $x_{1}$ and $a$ is a kernel of the set of functions from elements $i$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{2}})}$ to elements of $X$ applied to $i$ and the set of functions from natural numbers $n$ to elements of $X$ applied to $n$ defined as the function that maps $a$ to $\operatorname{mk}$ applied to $\operatorname{trajFun}$ applied to $n_{1}$ and $x_{1}$, $\mathrm{ProbabilityTheory\_\_Kernel\_\_measurable\_trajFun}$ applied to $x_{1}$ and $a$.
ProbabilityTheory.Kernel.trajContentdefMathlib.Probability.Kernel.IonescuTulcea.Traj, function or constantEnglish
Let $x_{1}$ be a function from natural numbers $n$ to kernels of the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n}}{x_{4}})}$ to elements of $X$ applied to $i_{1}$ and $X$ applied to $n + 1$. Let $x_{2}$ be a function from elements $i$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{3}})}$ to elements of $X$ applied to $i$. Then $\operatorname{trajContent}$ applied to $n$, $x_{1}$, $i$ and $x_{2}$ is an additive content of $\mathrm{ENNReal}$ and the measurable cylinder of $X$ defined as the function that maps $i$ and $x_{2}$ to the projective family content of $\mathrm{ProbabilityTheory\_\_Kernel\_\_isProjectiveMeasureFamily\_partialTraj}$ applied to $n$ and $x_{1}$.
ProbabilityTheory.Kernel.trajFundefMathlib.Probability.Kernel.IonescuTulcea.Traj, function or constantEnglish
Let $x_{1}$ be a function from natural numbers $n_{1}$ to kernels of the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n_{1}}}{x_{4}})}$ to elements of $X$ applied to $i_{1}$ and $X$ applied to $n_{1} + 1$. Let $a$ be a natural number. Let $x_{2}$ be a function from elements $i$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{3}})}$ to elements of $X$ applied to $i$. Then $\operatorname{trajFun}$ applied to $n_{1}$, $x_{1}$, $a$, $i$ and $x_{2}$ is a measure of the set of functions from natural numbers $n$ to elements of $X$ applied to $n$.
ProbabilityTheory.Kernel.trajMeasuredefMathlib.Probability.Kernel.IonescuTulcea.Traj, function or constantEnglish
Let $x_{1}$ be a measure of $X$ applied to $0$. Let $x_{2}$ be a function from natural numbers $n_{1}$ to kernels of the set of functions from elements $i$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n_{1}}}{x_{3}})}$ to elements of $X$ applied to $i$ and $X$ applied to $n_{1} + 1$. Then $\operatorname{trajMeasure}$ applied to $x_{1}$, $n_{1}$ and $x_{2}$ is a measure of the set of functions from natural numbers $n$ to elements of $X$ applied to $n$ defined as the function that maps $x_{2}$ to $\operatorname{bind}$ applied to the map of $\operatorname{coe}$ applied to the inverse of $\operatorname{piUnique}$ applied to the function that maps $i$ to $X$ applied to $i$ and $x_{1}$, $\operatorname{coe}$ applied to $\operatorname{traj}$ applied to $n_{1}$ and $0$ and $x_{2}$.
iterateInductiondefMathlib.Probability.Kernel.IonescuTulcea.Traj, function or constantEnglish
Let $x$ be a function from elements $i_{1}$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{3}})}$ to elements of $X$ applied to $i_{1}$. Let $\mathrm{ind}$ be a function from natural numbers $n_{1}$ and functions from elements $i$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n_{1}}}{x_{2}})}$ to elements of $X$ applied to $i$ to elements of $X$ applied to $n_{1} + 1$. Let $n$ be a natural number. Then $\mathrm{iterateInduction}$ applied to $i_{1}$, $x$, $n_{1}$, $\mathrm{ind}$ and $n$ is an element of $X$ applied to $n$.
ProbabilityTheory.Kernel.IsIrreducibleclassMathlib.Probability.Kernel.Irreducible, predicateWording
x3 is irreducible with respect to x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Let $x_{3}$ be a kernel of $x$ and $x$. Then we can say that $x_{3}$ is irreducible with respect to $x_{2}$.
ProbabilityTheory.posteriordefMathlib.Probability.Kernel.Posterior, function or constantEnglish
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Let $x_{5}$ be a measure of $x$. Then $\operatorname{posterior}$ applied to $x_{4}$ and $x_{5}$ is a kernel of $x_{1}$ and $x$ defined as the conditional kernel of the map of $\operatorname{swap}$ and the composition product of $x_{5}$ and $x_{4}$.
ProbabilityTheory.Kernel.IsProperstructureMathlib.Probability.Kernel.Proper, predicateWording
x2 is proper (from the name)
English
Let $x_{2}$ be a kernel of $X$ and $X$. Then we can say that $x_{2}$ is proper.
ProbabilityTheory.Kernel.mutuallySingularSetdefMathlib.Probability.Kernel.RadonNikodym, function or constantWording
the mutually singular set of x4 and x5 (from the name)
English
generation took over the time limit
ProbabilityTheory.Kernel.mutuallySingularSetSlicedefMathlib.Probability.Kernel.RadonNikodym, function or constantWording
the mutually singular set slice of x5 and a (from the name)
English
generation took over the time limit
ProbabilityTheory.Kernel.rnDerivdefMathlib.Probability.Kernel.RadonNikodym, function or constantEnglish
Let $x_{4}$ and $x_{5}$ be kernels of $x$ and $x_{1}$. Let $a$ be an element of $x$. Let $x_{6}$ be an element of $x_{1}$. Then $\operatorname{rnDeriv}$ applied to $x_{4}$, $x_{5}$, $a$ and $x_{6}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_Kernel\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_RadonNikodym\_\_2526622965\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{4}$, $x_{5}$, $a$ and $x_{6}$.
ProbabilityTheory.Kernel.singularPartdefMathlib.Probability.Kernel.RadonNikodym, function or constantWording
the singular part of x4 and x5 (from the name)
English
Let $x_{4}$ and $x_{5}$ be kernels of $x$ and $x_{1}$. Then the singular part of $x_{4}$ and $x_{5}$ is a kernel of $x$ and $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{ProbabilityTheory\_\_Kernel\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Kernel\_\_RadonNikodym\_\_743833221\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{4}$ and $x_{5}$.
ProbabilityTheory.Kernel.withDensitydefMathlib.Probability.Kernel.WithDensity, function or constantEnglish
Let $x_{4}$ be a kernel of $x$ and $x_{1}$. Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{withDensity}$ applied to $x_{4}$ and $f$ is a kernel of $x$ and $x_{1}$.
MeasureTheory.MartingaledefMathlib.Probability.Martingale.Basic, predicateWording
x6 is a martingale with respect to x5 (from the name)
English
Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $E$. Let $x_{5}$ be a filtration of $x_{1}$ and $m_{0}$. Let $x_{6}$ be a measure of $x$. Then $x_{6}$ is a martingale with respect to $x_{5}$, if $\operatorname{StronglyAdapted}$ holds for $x_{5}$ and $f$ and for all elements $i$ of $x_{1}$, for all elements $j$ of $x_{1}$, if $i \leq j$, then $\operatorname{EventuallyEq}$ holds for $\operatorname{ae}$ applied to $x_{6}$, $\operatorname{condExp}$ applied to $f$ applied to $j$ and $f$ applied to $i$.
MeasureTheory.SubmartingaledefMathlib.Probability.Martingale.Basic, predicateEnglish
Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $E$. Let $x_{6}$ be a filtration of $x_{1}$ and $m_{0}$. Let $x_{7}$ be a measure of $x$. Then $\operatorname{Submartingale}$ holds for $f$, $x_{6}$ and $x_{7}$, if $\operatorname{StronglyAdapted}$ holds for $x_{6}$ and $f$, for all elements $i$ of $x_{1}$, for all elements $j$ of $x_{1}$, if $i \leq j$, then $\operatorname{EventuallyLE}$ holds for $\operatorname{ae}$ applied to $x_{7}$, $f$ applied to $i$ and $\operatorname{condExp}$ applied to $f$ applied to $j$ and for all elements $i_{1}$ of $x_{1}$, $\operatorname{Integrable}$ holds for $f$ applied to $i_{1}$ and $x_{7}$.
MeasureTheory.SupermartingaledefMathlib.Probability.Martingale.Basic, predicateEnglish
Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $E$. Let $x_{6}$ be a filtration of $x_{1}$ and $m_{0}$. Let $x_{7}$ be a measure of $x$. Then $\operatorname{Supermartingale}$ holds for $f$, $x_{6}$ and $x_{7}$, if $\operatorname{StronglyAdapted}$ holds for $x_{6}$ and $f$, for all elements $i$ of $x_{1}$, for all elements $j$ of $x_{1}$, if $i \leq j$, then $\operatorname{EventuallyLE}$ holds for $\operatorname{ae}$ applied to $x_{7}$, $\operatorname{condExp}$ applied to $f$ applied to $j$ and $f$ applied to $i$ and for all elements $i_{1}$ of $x_{1}$, $\operatorname{Integrable}$ holds for $f$ applied to $i_{1}$ and $x_{7}$.
MeasureTheory.leastGEdefMathlib.Probability.Martingale.BorelCantelli, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $r$ be an element of $x_{2}$. Let $x_{7}$ be an element of $x_{1}$. Then $\operatorname{leastGE}$ applied to $f$, $r$ and $x_{7}$ is an element of $\mathrm{WithTop}$ applied to $x$ defined as $\operatorname{hittingAfter}$ applied to $f$, $\operatorname{Ici}$ applied to $r$, the bottom and $x_{7}$.
MeasureTheory.stoppedAbovedefMathlib.Probability.Martingale.BorelCantelli, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $r$ be an element of $x_{2}$. Let $x_{7}$ be an element of $x$. Let $x_{8}$ be an element of $x_{1}$. Then $\operatorname{stoppedAbove}$ applied to $f$, $r$, $x_{7}$ and $x_{8}$ is an element of $x_{2}$ defined as $\operatorname{stoppedProcess}$ applied to $f$, $\operatorname{leastGE}$ applied to $f$ and $r$, $x_{7}$ and $x_{8}$.
MeasureTheory.martingalePartdefMathlib.Probability.Martingale.Centering, function or constantWording
the martingale part of x5 and x6 (from the name)
English
Let $f$ be a function from natural numbers and elements of $x$ to elements of $E$. Let $x_{3}$ be a filtration of $\Natural$ and $m_{0}$. Let $x_{4}$ be a measure of $x$. Let $x_{5}$ be a natural number. Let $x_{6}$ be an element of $x$. Then the martingale part of $x_{5}$ and $x_{6}$ is an element of $E$ defined as $\mathrm{minus}$ applied to $f$ applied to $x_{5}$, $\operatorname{predictablePart}$ applied to $x_{5}$ and $x_{6}$.
MeasureTheory.predictablePartdefMathlib.Probability.Martingale.Centering, function or constantWording
the predictable part of x5 and x6 (from the name)
English
Let $f$ be a function from elements of $\Natural$ and elements of $x$ to elements of $E$. Let $x_{3}$ be a filtration of $\Natural$ and $m_{0}$. Let $x_{4}$ be a measure of $x$. Let $x_{5}$ be an element of $\Natural$. Let $x_{6}$ be an element of $x$. Then the predictable part of $x_{5}$ and $x_{6}$ is an element of $E$ defined as $\operatorname{sum} (\FinsetrangeMACRoN {x_{5}}, \lambda i . \lambda x_{6} . \operatorname{condExp} (f (i + 1)- f (i), x_{6}), x_{6})$.
MeasureTheory.lowerCrossingTimedefMathlib.Probability.Martingale.Upcrossing, function or constantWording
the lower crossing time of n and x5 (from the name)
English
Let $a$ and $b$ be real numbers. Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to real numbers. Let $N$ be an element of $x_{1}$. Let $n$ be a natural number. Let $x_{5}$ be an element of $x$. Then the lower crossing time of $n$ and $x_{5}$ is an element of $x_{1}$ defined as $\operatorname{hittingBtwn}$ applied to $f$, $\operatorname{Iic}$ applied to $a$, the upper crossing time of $n$ and $x_{5}$, $N$ and $x_{5}$.
MeasureTheory.upcrossingStratdefMathlib.Probability.Martingale.Upcrossing, function or constantEnglish
Let $a$ and $b$ be elements of $\Real$. Let $f$ be a function from elements of $\Natural$ and elements of $x$ to elements of $\Real$. Let $N$ and $n$ be elements of $\Natural$. Let $x_{1}$ be an element of $x$. Then $\operatorname{upcrossingStrat}$ applied to $a$, $b$, $f$, $N$, $n$ and $x_{1}$ is an element of $\Real$ defined as $\FinsetSum {\FinsetrangeMACRoN {N}}{k}{\operatorname{indicator} (1 , n)}$.
MeasureTheory.upcrossingsdefMathlib.Probability.Martingale.Upcrossing, function or constantEnglish
Let $a$ and $b$ be real numbers. Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to real numbers. Let $x_{5}$ be an element of $x$. Then $\operatorname{upcrossings}$ applied to $a$, $b$, $f$ and $x_{5}$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $N$ to $\operatorname{upcrossingsBefore}$ applied to $a$, $b$, $f$, $N$ and $x_{5}$.
MeasureTheory.upcrossingsBeforedefMathlib.Probability.Martingale.Upcrossing, function or constantEnglish
Let $a$ and $b$ be real numbers. Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to real numbers. Let $N$ be an element of $x_{1}$. Let $x_{5}$ be an element of $x$. Then $\operatorname{upcrossingsBefore}$ applied to $a$, $b$, $f$, $N$ and $x_{5}$ is a natural number defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that the upper crossing time of $n$ and $x_{5}$ is less than $N$.
MeasureTheory.upperCrossingTimedefMathlib.Probability.Martingale.Upcrossing, function or constantWording
the upper crossing time of x5 and x6 (from the name)
English
Let $a$ and $b$ be real numbers. Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to real numbers. Let $N$ be an element of $x_{1}$. Let $x_{5}$ be a natural number. Let $x_{6}$ be an element of $x$. Then the upper crossing time of $x_{5}$ and $x_{6}$ is an element of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{5}$, $\mathrm{MeasureTheory\_\_upperCrossingTime\_\_\_f}$ applied to $a$, $b$, $f$ and $N$ and $x_{6}$.
ProbabilityTheory.centralMomentdefMathlib.Probability.Moments.Basic, function or constantWording
the central moment of p and x1 (from the name)
English
Let $X$ be a function from elements of $x$ to real numbers. Let $p$ be a natural number. Let $x_{1}$ be a measure of $x$. Then the central moment of $p$ and $x_{1}$ is a real number defined as the Bochner integral of $x_{1}$ and the function that maps $x_{2}$ to $\mathrm{pow}$ applied to the difference between $X$ and the function that maps $x_{3}$ to the Bochner integral of $x_{1}$ and the function that maps $x_{4}$ to $X$ applied to $x_{4}$, $p$ and $x_{2}$.
ProbabilityTheory.cgfdefMathlib.Probability.Moments.Basic, function or constantEnglish
Let $X$ be a function from elements of $x$ to real numbers. Let $x_{1}$ be a measure of $x$. Let $t$ be a real number. Then $\operatorname{cgf}$ applied to $X$, $x_{1}$ and $t$ is a real number defined as the logarithm of $\operatorname{mgf}$ applied to $X$, $x_{1}$ and $t$.
ProbabilityTheory.mgfdefMathlib.Probability.Moments.Basic, function or constantEnglish
Let $X$ be a function from elements of $x$ to real numbers. Let $x_{1}$ be a measure of $x$. Let $t$ be a real number. Then $\operatorname{mgf}$ applied to $X$, $x_{1}$ and $t$ is a real number defined as the Bochner integral of $x_{1}$ and the function that maps $x_{2}$ to the exponential of $t \times X (x_{2})$.
ProbabilityTheory.momentdefMathlib.Probability.Moments.Basic, function or constantWording
the moment of p and x1 (from the name)
English
Let $X$ be a function from elements of $x$ to real numbers. Let $p$ be a natural number. Let $x_{1}$ be a measure of $x$. Then the moment of $p$ and $x_{1}$ is a real number defined as the Bochner integral of $x_{1}$ and the function that maps $x_{2}$ to $\mathrm{pow} (X , p , x_{2})$.
ProbabilityTheory.complexMGFdefMathlib.Probability.Moments.ComplexMGF, function or constantEnglish
Let $X$ be a function from elements of $x$ to real numbers. Let $x_{1}$ be a measure of $x$. Let $z$ be a complex. Then $\operatorname{complexMGF}$ applied to $X$, $x_{1}$ and $z$ is a complex defined as the Bochner integral of $x_{1}$ and the function that maps $x_{2}$ to the exponential of the product of $z$ and the natural inclusion of the real numbers into the complex numbers of $X$ applied to $x_{2}$.
ProbabilityTheory.covariancedefMathlib.Probability.Moments.Covariance, function or constantWording
the covariance of Y and x2 (from the name)
English
Let $X$ and $Y$ be functions from elements of $x$ to real numbers. Let $x_{2}$ be a measure of $x$. Then the covariance of $Y$ and $x_{2}$ is a real number defined as the Bochner integral of $x_{2}$ and the function that maps $x_{3}$ to the product of the difference between $X$ applied to $x_{3}$ and the Bochner integral of $x_{2}$ and the function that maps $x_{4}$ to $X$ applied to $x_{4}$ and the difference between $Y$ applied to $x_{3}$ and the Bochner integral of $x_{2}$ and the function that maps $x_{5}$ to $Y$ applied to $x_{5}$.
ProbabilityTheory.covarianceBilindefMathlib.Probability.Moments.CovarianceBilin, function or constantWording
the covariance bilinear of x3 (from the name)
English
Let $x_{3}$ be a measure of $E$. Then the covariance bilinear of $x_{3}$ is a continuous linear map of $E$ and the set of continuous linear maps of $E$ and $\Real$ defined as the bilinear composition of the continuous linear map of the dual map of $\Real$ and $E$ and the continuous linear map of the dual map of $\Real$ and $E$.
ProbabilityTheory.covarianceOperatordefMathlib.Probability.Moments.CovarianceBilin, function or constantWording
the covariance operator of the measure of x3 (from the docstring)
English
Let $x_{3}$ be a measure of $E$. Then the covariance operator of the measure of $x_{3}$ is a continuous linear map of $E$ and $E$ defined as the continuous linear map of the bilinear composition of the continuous linear map of the dual map of $\Real$ and $E$ and the continuous linear map of the dual map of $\Real$ and $E$.
ProbabilityTheory.covarianceBilinDualdefMathlib.Probability.Moments.CovarianceBilinDual, function or constantWording
the covariance bilinear dual of x2 (from the name)
English
Let $x_{2}$ be a measure of $E$. Then the covariance bilinear dual of $x_{2}$ is a continuous linear map of the set of strong duals of $\Real$ and $E$ and the set of continuous linear maps of the set of strong duals of $\Real$ and $E$ and $\Real$ defined as $\operatorname{uncenteredCovarianceBilinDual}$ applied to the map of the function that maps $x_{3}$ to the difference between $x_{3}$ and the Bochner integral of $x_{2}$ and the function that maps $x_{4}$ to $x_{4}$ and $x_{2}$.
ProbabilityTheory.uncenteredCovarianceBilinDualdefMathlib.Probability.Moments.CovarianceBilinDual, function or constantEnglish
Let $x_{2}$ be a measure of $E$. Then $\operatorname{uncenteredCovarianceBilinDual}$ applied to $x_{2}$ is a continuous linear map of the set of strong duals of $\Real$ and $E$ and the set of continuous linear maps of the set of strong duals of $\Real$ and $E$ and $\Real$.
StrongDual.toLpdefMathlib.Probability.Moments.CovarianceBilinDual, function or constantEnglish
Let $x_{4}$ be a measure of $E$. Let $p$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{toLp}$ applied to $x_{4}$ and $p$ is a continuous linear map of the set of strong duals of $x_{1}$ and $E$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (x_{1} , p , x_{4})}{x_{5}})}$.
StrongDual.toLpₗdefMathlib.Probability.Moments.CovarianceBilinDual, function or constantEnglish
Let $x_{4}$ be a measure of $E$. Let $p$ be an element of $\mathrm{ENNReal}$. Then $\mathrm{StrongDual\_\_toLp\_u2097\_}$ applied to $x_{4}$ and $p$ is a linear map of the set of strong duals of $x_{1}$ and $E$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (x_{1} , p , x_{4})}{x_{5}})}$.
ProbabilityTheory.integrableExpSetdefMathlib.Probability.Moments.IntegrableExpMul, function or constantWording
the integrable exponential set of X and x1 (from the name)
English
Let $X$ be a function from elements of $x$ to real numbers. Let $x_{1}$ be a measure of $x$. Then the integrable exponential set of $X$ and $x_{1}$ is an element of $\wp \Real$ defined as $\operatorname{ofPred}$ applied to the function that maps $t$ to $\operatorname{Integrable}$ applied to the function that maps $x_{2}$ to the exponential of $t \times X (x_{2})$ and $x_{1}$.
ProbabilityTheory.HasCondSubgaussianMGFdefMathlib.Probability.Moments.SubGaussian, predicateEnglish
Assume that $x$ is a measurable space. Assume that $m \leq x_{1}$. Let $X$ be a function from elements of $x$ to real numbers. Let $c$ be an element of $\mathrm{NNReal}$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_HasCondSubgaussianMGF\_\_\_auto\_1}$. Then $\operatorname{HasCondSubgaussianMGF}$ holds for $m$, $\mathrm{hm}$, $X$, $c$ and $x_{2}$, if $\operatorname{HasSubgaussianMGF}$ holds for $X$, $c$, the conditional exponential kernel of $x_{2}$ and $m$ and $\operatorname{trim}$ applied to $x_{2}$ and $\mathrm{hm}$.
ProbabilityTheory.HasSubgaussianMGFstructureMathlib.Probability.Moments.SubGaussian, predicateEnglish
Let $X$ be a function from elements of $x$ to real numbers. Let $c$ be an element of $\mathrm{NNReal}$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{ProbabilityTheory\_\_HasSubgaussianMGF\_\_\_auto\_1}$. Then we can say that $\operatorname{HasSubgaussianMGF}$ holds for $X$, $c$ and $x_{2}$.
ProbabilityTheory.Kernel.HasSubgaussianMGFstructureMathlib.Probability.Moments.SubGaussian, predicateEnglish
Let $X$ be a function from elements of $x$ to real numbers. Let $c$ be an element of $\mathrm{NNReal}$. Let $x_{4}$ be a kernel of $x_{1}$ and $x$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{ProbabilityTheory\_\_Kernel\_\_HasSubgaussianMGF\_\_\_auto\_1}$. Then we can say that $\operatorname{HasSubgaussianMGF}$ holds for $X$, $c$, $x_{4}$ and $x_{5}$.
ProbabilityTheory.evariancedefMathlib.Probability.Moments.Variance, function or constantEnglish
Let $X$ be a function from elements of $x$ to real numbers. Let $x_{2}$ be a measure of $x$. Then $\operatorname{evariance}$ applied to $X$ and $x_{2}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{lintegral}$ applied to $x_{2}$ and the function that maps $x_{3}$ to the exponentiation of the extended norm of the difference between $X$ applied to $x_{3}$ and the Bochner integral of $x_{2}$ and the function that maps $x_{4}$ to $X$ applied to $x_{4}$ to $2$.
ProbabilityTheory.variancedefMathlib.Probability.Moments.Variance, function or constantWording
the variance of X and x2 (from the name)
English
Let $X$ be a function from elements of $x$ to real numbers. Let $x_{2}$ be a measure of $x$. Then the variance of $X$ and $x_{2}$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{evariance}$ applied to $X$ and $x_{2}$.
MeasureTheory.Measure.toPMFdefMathlib.Probability.ProbabilityMassFunction.Basic, function or constantWording
the probability mass function of x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Then the probability mass function of $x_{2}$ is a probability mass function of $x$ defined as the function that maps $x_{3}$ to $x_{2}$ applied to $\operatorname{singleton}$ applied to $x_{3}$.
PMFdefMathlib.Probability.ProbabilityMassFunction.Basic, typeWording
probability mass function of x (from the name)
English
Let $x$ be a set. Then a probability mass function of $x$ is an element of the function that maps $x$ to $\SubtypeSet {f}{\mathrm{HasSum} (f , 1 , \operatorname{unconditional} (x))}$.
PMF.supportdefMathlib.Probability.ProbabilityMassFunction.Basic, function or constantWording
the support of p (from the docstring)
English
Let $p$ be a probability mass function of $x$. Then the support of $p$ is an element of $\wp x$ defined as the support of $\operatorname{coe}$ applied to $p$.
PMF.toMeasuredefMathlib.Probability.ProbabilityMassFunction.Basic, function or constantWording
the measure of p (from the name)
English
Let $p$ be a probability mass function of $x$. Then the measure of $p$ is a measure of $x$.
PMF.toOuterMeasuredefMathlib.Probability.ProbabilityMassFunction.Basic, function or constantWording
the outer measure of p (from the name)
English
Let $p$ be a probability mass function of $x$. Then the outer measure of $p$ is an outer measure of $x$ defined as the sum of the function that maps $x_{1}$ to $\HSMulhSMulMACRoAL {p (x_{1})}{\operatorname{dirac} (x_{1})}$.
PMF.filterdefMathlib.Probability.ProbabilityMassFunction.Constructions, function or constantWording
the filter of p and s (from the name)
English
Let $p$ be a probability mass function of $x$. Let $s$ be an element of $\wp x$ such that there exists an element $a$ of $x$, such that $a$ is an element of $s$ and $a$ is an element of the support of $p$. Then the filter of $p$ and $s$ is a probability mass function of $x$.
PMF.mapdefMathlib.Probability.ProbabilityMassFunction.Constructions, function or constantWording
the map of f and p (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be a probability mass function of $x$. Then the map of $f$ and $p$ is a probability mass function of $x_{1}$ defined as $\operatorname{bind}$ applied to $p$ and $\operatorname{comp}$ applied to $\operatorname{pure}$ and $f$.
PMF.normalizedefMathlib.Probability.ProbabilityMassFunction.Constructions, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$ such that the sum of $f$ and $\operatorname{unconditional}$ applied to $x$ is distinct from $0$ and the sum of $f$ and $\operatorname{unconditional}$ applied to $x$ is distinct from the top. Then $\operatorname{normalize}$ applied to $f$, $\mathrm{hf0}$ and $\mathrm{hf}$ is a probability mass function of $x$ defined as the function that maps $a$ to the product of $f$ applied to $a$ and $\operatorname{inv}$ applied to the sum of the function that maps $x_{1}$ to $f$ applied to $x_{1}$ and $\operatorname{unconditional}$ applied to $x$.
PMF.ofFinsetdefMathlib.Probability.ProbabilityMassFunction.Constructions, function or constantWording
the probability mass function of f and s (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$. Let $s$ be a finite set of $x$ such that $\EqtMACRoH {\FinsetSum {s}{a_{1}}{f (a_{1})}}{1}$ and for all elements $a$ of $x$, if $a$ is not an element of $s$, then $\EqtMACRoH {f (a)}{0}$. Then the probability mass function of $f$ and $s$ is a probability mass function of $x$ defined as $f$.
PMF.ofFintypedefMathlib.Probability.ProbabilityMassFunction.Constructions, function or constantWording
the probability mass function of f and h (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$ such that $\EqtMACRoH {\FinsetSum {\FinsetunivMACRoAC}{a}{f (a)}}{1}$. Then the probability mass function of $f$ and $h$ is a probability mass function of $x$.
PMF.seqdefMathlib.Probability.ProbabilityMassFunction.Constructions, function or constantWording
the sequence of q and p (from the name)
English
Let $q$ be a probability mass function of the set of functions from elements of $x$ to elements of $x_{1}$. Let $p$ be a probability mass function of $x$. Then the sequence of $q$ and $p$ is a probability mass function of $x_{1}$ defined as $\operatorname{bind}$ applied to $q$ and the function that maps $m$ to $\operatorname{bind}$ applied to $p$ and the function that maps $a$ to $\operatorname{pure}$ applied to $m$ applied to $a$.
PMF.binddefMathlib.Probability.ProbabilityMassFunction.Monad, function or constantEnglish
Let $p$ be a probability mass function of $x$. Let $f$ be a function from elements of $x$ to probability mass functions of $x_{1}$. Then $\operatorname{bind}$ applied to $p$ and $f$ is a probability mass function of $x_{1}$ defined as the function that maps $b$ to the sum of the function that maps $a$ to $p (a)\times f (a , b)$ and $\operatorname{unconditional}$ applied to $x$.
PMF.bindOnSupportdefMathlib.Probability.ProbabilityMassFunction.Monad, function or constantEnglish
Let $p$ be a probability mass function of $x$. Let $f$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a$ is an element of the support of $p$ to probability mass functions of $x_{1}$. Then $\operatorname{bindOnSupport}$ applied to $p$, $a$ and $f$ is a probability mass function of $x_{1}$ defined as the function that maps $b$ to the sum of the function that maps $a$ to $p (a)\times \mathrm{dite} (\EqtMACRoH {p (a)}{0}, \lambda h . 0 , \lambda h_{1} . a (a , h_{1} , f))$ and $\operatorname{unconditional}$ applied to $x$.
PMF.puredefMathlib.Probability.ProbabilityMassFunction.Monad, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{pure}$ applied to $a$ is a probability mass function of $x$ defined as the function that maps $\mathrm{a'}$ to $\iteMACRoG {(\EqtMACRoH {\mathrm{a'}}{a})}{1}{0}$.
MeasureTheory.AdapteddefMathlib.Probability.Process.Adapted, predicateEnglish
Let $f$ be a filtration of $x_{1}$ and $m$. Let $u$ be a function from elements $i$ of $x_{1}$ and elements of $x$ to elements of $x_{3}$ applied to $i$. Then $\operatorname{Adapted}$ holds for $f$, $i$ and $u$, if for all elements $i$ of $x_{1}$, $i$ applied to $i$ is measurable.
MeasureTheory.IsProgressivedefMathlib.Probability.Process.Adapted, predicateEnglish
Let $f$ be a filtration of $x_{1}$ and $m$. Let $u$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $x_{3}$. Then $\operatorname{IsProgressive}$ holds for $f$ and $u$, if for all elements $i$ of $x_{1}$, the function that maps $p$ to $u$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$ is measurable.
MeasureTheory.IsStronglyProgressivedefMathlib.Probability.Process.Adapted, predicateEnglish
Let $f$ be a filtration of $x_{1}$ and $m$. Let $u$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $x_{3}$. Then $\operatorname{IsStronglyProgressive}$ holds for $f$ and $u$, if for all elements $i$ of $x_{1}$, $\operatorname{StronglyMeasurable}$ holds for the function that maps $p$ to $u$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.
MeasureTheory.StronglyAdapteddefMathlib.Probability.Process.Adapted, predicateEnglish
Let $f$ be a filtration of $x_{1}$ and $m$. Let $u$ be a function from elements $i$ of $x_{1}$ and elements of $x$ to elements of $x_{3}$ applied to $i$. Then $\operatorname{StronglyAdapted}$ holds for $f$, $i$ and $u$, if for all elements $i$ of $x_{1}$, $\operatorname{StronglyMeasurable}$ holds for $i$ applied to $i$.
MeasureTheory.FiltrationstructureMathlib.Probability.Process.Filtration, typeWording
filtration of x1 and m (from the name)
English
Let $x_{1}$ be a set. Assume that $x$ is a measurable space. Then the filtrations of $x_{1}$ and $m$ are a basic type.
MeasureTheory.Filtration.IsRightContinuousclassMathlib.Probability.Process.Filtration, predicateEnglish
Let $x_{3}$ be a filtration of $x_{1}$ and $m$. Then we can say that $\operatorname{IsRightContinuous}$ holds for $x_{3}$.
MeasureTheory.Filtration.constdefMathlib.Probability.Process.Filtration, function or constantWording
the constant of #2 and #3 (from the name)
English
Let $x_{1}$ be a set. Assume that $x$ is a measurable space. Assume that $\mathrm{m'} \leq m$. Then the constant of $\mathrm{m'}$ and $\mathrm{hm'}$ is a filtration of $x_{1}$ and $m$.
MeasureTheory.Filtration.cylinderEventsCompldefMathlib.Probability.Process.Filtration, function or constantWording
the cylinder event complement (from the name)
English
The cylinder event complement is a filtration of the set of order duals of the set of finite sets of $x_{1}$ and $\operatorname{pi}$.
MeasureTheory.Filtration.naturaldefMathlib.Probability.Process.Filtration, function or constantEnglish
Let $u$ be a function from elements $i_{1}$ of $x_{1}$ and elements of $x$ to elements of $x_{2}$ applied to $i_{1}$ such that for all elements $i$ of $x_{1}$, $\operatorname{StronglyMeasurable}$ holds for $u$ applied to $i$. Then $\operatorname{natural}$ applied to $i_{1}$, $u$ and $\mathrm{hum}$ is a filtration of $x_{1}$ and $m$.
MeasureTheory.Filtration.piFinsetdefMathlib.Probability.Process.Filtration, function or constantWording
the product finite set (from the name)
English
The product finite set is a filtration of the set of finite sets of $x$ and $\operatorname{pi}$.
MeasureTheory.Filtration.piLEdefMathlib.Probability.Process.Filtration, function or constantWording
the canonical filtration on the product space (from the docstring)
English
The canonical filtration on the product space is a filtration of $x$ and $\operatorname{pi}$.
MeasureTheory.Filtration.rightContdefMathlib.Probability.Process.Filtration, function or constantEnglish
Let $x_{3}$ be a filtration of $x_{1}$ and $m$. Then $\operatorname{rightCont}$ applied to $x_{3}$ is a filtration of $x_{1}$ and $m$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_Filtration\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Probability\_\_Process\_\_Filtration\_\_2188831487\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $x_{3}$.
MeasureTheory.SigmaFiniteFiltrationclassMathlib.Probability.Process.Filtration, predicateWording
x3 is a sigma finite filtration with respect to f (from the name)
English
Let $x_{3}$ be a measure of $x$. Let $f$ be a filtration of $x_{1}$ and $m$. Then we can say that $x_{3}$ is a sigma finite filtration with respect to $f$.
MeasureTheory.filtrationOfSetdefMathlib.Probability.Process.Filtration, function or constantWording
the filtration of hsm (from the name)
English
Assume that for all elements $i$ of $x_{1}$, $s$ applied to $i$ is a measurable set. Then the filtration of $\mathrm{hsm}$ is a filtration of $x_{1}$ and $m$.
MeasureTheory.hittingAfterdefMathlib.Probability.Process.HittingTime, function or constantEnglish
Let $u$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Let $n$ be an element of $x_{2}$. Let $x_{5}$ be an element of $x$. Then $\operatorname{hittingAfter}$ applied to $u$, $s$, $n$ and $x_{5}$ is an element of $\mathrm{WithTop}$ applied to $x_{2}$ defined as $\iteMACRoG {\mathrm{exists} (x_{2} , \lambda j . \mathrm{and} (\mathrm{Leq} (n , j), \MembershipmemMACRoT {s}{u (j , x_{5})}))}{\operatorname{some} (\operatorname{sInf} (\operatorname{ofPred} (\lambda i . \mathrm{and} (\mathrm{Leq} (n , i), \MembershipmemMACRoT {s}{u (i , x_{5})}))))}{\operatorname{top}}$.
MeasureTheory.hittingBtwndefMathlib.Probability.Process.HittingTime, function or constantEnglish
Let $u$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Let $n$ and $m$ be elements of $x_{2}$. Let $x_{5}$ be an element of $x$. Then $\operatorname{hittingBtwn}$ applied to $u$, $s$, $n$, $m$ and $x_{5}$ is an element of $x_{2}$ defined as $\iteMACRoG {\mathrm{exists} (x_{2} , \lambda j . \mathrm{and} (\MembershipmemMACRoT {(\SetIccMACRoP {n}{m})}{j}, \MembershipmemMACRoT {s}{u (j , x_{5})}))}{\operatorname{sInf} (\operatorname{inter} (\SetIccMACRoP {n}{m}, \operatorname{ofPred} (\lambda i . \MembershipmemMACRoT {s}{u (i , x_{5})})))}{m}$.
ProbabilityTheory.IndistinguishabledefMathlib.Probability.Process.Indistinguishable, predicateEnglish
Let $P$ be a measure of $x_{1}$. Let $X$ and $Y$ be functions from elements of $x$ and elements of $x_{1}$ to elements of $E$. Then $\operatorname{Indistinguishable}$ holds for $P$, $X$ and $Y$, if $\operatorname{Eventually}$ holds for the function that maps $x_{3}$ to the proposition that for all elements $t$ of $x$, $\EqtMACRoH {X (t , x_{3})}{Y (t , x_{3})}$ and $\operatorname{ae}$ applied to $P$.
ProbabilityTheory.IsAEKolmogorovProcessdefMathlib.Probability.Process.Kolmogorov, predicateEnglish
Let $X$ be a function from elements of $T$ and elements of $x$ to elements of $E$. Let $P$ be a measure of $x$. Let $p$ and $q$ be real numbers. Let $M$ be an element of $\mathrm{NNReal}$. Then $\operatorname{IsAEKolmogorovProcess}$ holds for $X$, $P$, $p$, $q$ and $M$, if there exists a function $Y$ from elements of $T$ and elements of $x$ to elements of $E$, such that $\operatorname{IsKolmogorovProcess}$ holds for $Y$, $P$, $p$, $q$ and $M$ and for all elements $t$ of $T$, $\operatorname{EventuallyEq}$ holds for $\operatorname{ae}$ applied to $P$, $X$ applied to $t$ and $Y$ applied to $t$.
ProbabilityTheory.IsAEKolmogorovProcess.mkdefMathlib.Probability.Process.Kolmogorov, function or constantEnglish
Let $X$ be a function from elements of $T$ and elements of $x$ to elements of $E$ such that $\operatorname{IsAEKolmogorovProcess}$ holds for $X$, $P$, $p$, $q$ and $M$. Let $x_{4}$ be an element of $T$. Let $x_{5}$ be an element of $x$. Then $\operatorname{mk}$ applied to $X$, $h$, $x_{4}$ and $x_{5}$ is an element of $E$ defined as $\operatorname{choose}$ applied to $h$, $x_{4}$ and $x_{5}$.
ProbabilityTheory.IsKolmogorovProcessstructureMathlib.Probability.Process.Kolmogorov, predicateEnglish
Let $X$ be a function from elements of $T$ and elements of $x$ to elements of $E$. Let $P$ be a measure of $x$. Let $p$ and $q$ be real numbers. Let $M$ be an element of $\mathrm{NNReal}$. Then we can say that $\operatorname{IsKolmogorovProcess}$ holds for $X$, $P$, $p$, $q$ and $M$.
MeasureTheory.Filtration.HasLimitProcessdefMathlib.Probability.Process.LimitProcess, predicateEnglish
Let $X$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $E$. Let $x_{5}$ be a filtration of $x$ and $x_{3}$. Let $P$ be a measure of $x_{1}$. Then $\operatorname{HasLimitProcess}$ holds for $X$, $x_{5}$ and $P$, if there exists a function $g$ from elements of $x_{1}$ to elements of $E$, such that $\operatorname{StronglyMeasurable}$ holds for $g$ and $\operatorname{Eventually}$ holds for the function that maps $x_{6}$ to $\operatorname{Tendsto}$ applied to the function that maps $x_{7}$ to $X$ applied to $x_{7}$ and $x_{6}$, $\operatorname{atTop}$ and the neighbourhood filter of $g$ applied to $x_{6}$ and $\operatorname{ae}$ applied to $P$.
MeasureTheory.Filtration.limitProcessdefMathlib.Probability.Process.LimitProcess, function or constantWording
the limit process of P and x7 (from the name)
English
Let $X$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $E$. Let $x_{6}$ be a filtration of $x$ and $x_{3}$. Let $P$ be a measure of $x_{1}$. Let $x_{7}$ be an element of $x_{1}$. Then the limit process of $P$ and $x_{7}$ is an element of $E$ defined as $\mathrm{dite}$ applied to $\operatorname{HasLimitProcess}$ applied to $X$, $x_{6}$ and $P$, the function that maps $h$ to $\operatorname{choose}$ applied to $h$, the function that maps $h_{1}$ to $0$ and $x_{7}$.
ProbabilityTheory.IsLocalizingSequencestructureMathlib.Probability.Process.LocalProperty, predicateEnglish
Let $x_{5}$ be a filtration of $x$ and $x_{2}$. Let $x_{6}$ be a function from natural numbers and elements of $x_{1}$ to elements of $\mathrm{WithTop}$ applied to $x$. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{ProbabilityTheory\_\_IsLocalizingSequence\_\_\_auto\_1}$. Then we can say that $\operatorname{IsLocalizingSequence}$ holds for $x_{5}$, $x_{6}$ and $P$.
ProbabilityTheory.IsPreLocalizingSequencestructureMathlib.Probability.Process.LocalProperty, predicateEnglish
Let $x_{5}$ be a filtration of $x$ and $x_{2}$. Let $x_{6}$ be a function from natural numbers and elements of $x_{1}$ to elements of $\mathrm{WithTop}$ applied to $x$. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{ProbabilityTheory\_\_IsPreLocalizingSequence\_\_\_auto\_1}$. Then we can say that $\operatorname{IsPreLocalizingSequence}$ holds for $x_{5}$, $x_{6}$ and $P$.
ProbabilityTheory.IsStabledefMathlib.Probability.Process.LocalProperty, predicateEnglish
Let $x_{6}$ be a filtration of $x$ and $x_{2}$. Let $p$ be a function from functions from elements of $x$ and elements of $x_{1}$ to elements of $E$ to propositions. Then $\operatorname{IsStable}$ holds for $x_{6}$ and $p$, if for all functions $X$ from elements of $x$ and elements of $x_{1}$ to elements of $E$, if $p$ holds for $X$, then for all functions $x_{7}$ from elements of $x_{1}$ to elements of $\mathrm{WithTop}$ applied to $x$, if $x_{7}$ is a stopping time with respect to $x_{6}$, then $p$ holds for $\operatorname{stoppedProcess}$ applied to the function that maps $i$ to $\operatorname{indicator}$ applied to $X$ applied to $i$ and $x_{7}$.
ProbabilityTheory.LocallydefMathlib.Probability.Process.LocalProperty, predicateEnglish
Let $p$ be a function from functions from elements of $x$ and elements of $x_{1}$ to elements of $E$ to propositions. Let $x_{7}$ be a filtration of $x$ and $x_{2}$. Let $X$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $E$. Let $P$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{ProbabilityTheory\_\_Locally\_\_\_auto\_1}$. Then $\operatorname{Locally}$ holds for $p$, $x_{7}$, $X$ and $P$, if there exists a function $x_{8}$ from natural numbers and elements of $x_{1}$ to elements of $\mathrm{WithTop}$ applied to $x$, such that $\operatorname{IsLocalizingSequence}$ holds for $x_{7}$, $x_{8}$ and $P$ and for all natural numbers $n$, $p$ holds for $\operatorname{stoppedProcess}$ applied to the function that maps $i$ to $\operatorname{indicator}$ applied to $X$ applied to $i$ and $x_{8}$ applied to $n$.
ProbabilityTheory.Locally.localSeqdefMathlib.Probability.Process.LocalProperty, function or constantWording
the local sequence of x8 and x9 (from the name)
English
Assume that $\operatorname{Locally}$ holds for $p$, $x_{4}$, $X$ and $P$. Let $x_{8}$ be a natural number. Let $x_{9}$ be an element of $x_{1}$. Then the local sequence of $x_{8}$ and $x_{9}$ is an element of $\mathrm{WithTop}$ applied to $x$ defined as $\operatorname{choose}$ applied to $\mathrm{hX}$, $x_{8}$ and $x_{9}$.
ProbabilityTheory.countableFiltrationdefMathlib.Probability.Process.PartitionFiltration, function or constantWording
the countable filtration of x (from the name)
English
Let $x$ be a set. Then the countable filtration of $x$ is a filtration of $\Natural$ and $m$.
ProbabilityTheory.partitionFiltrationdefMathlib.Probability.Process.PartitionFiltration, function or constantWording
the partition filtration of ht (from the name)
English
Assume that for all natural numbers $n$, $t$ applied to $n$ is a measurable set. Then the partition filtration of $\mathrm{ht}$ is a filtration of $\Natural$ and $m$.
MeasureTheory.IsStronglyPredictabledefMathlib.Probability.Process.Predictable, predicateEnglish
Let $x_{5}$ be a filtration of $x_{1}$ and $m$. Let $u$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $E$. Then $\operatorname{IsStronglyPredictable}$ holds for $x_{5}$ and $u$, if $\operatorname{StronglyMeasurable}$ holds for $\operatorname{uncurry}$ applied to $u$.
MeasureTheory.IsStoppingTimedefMathlib.Probability.Process.Stopping, predicateWording
x3 is a stopping time with respect to f (from the name)
English
Let $f$ be a filtration of $x_{1}$ and $m$. Let $x_{3}$ be a function from elements of $x$ to elements of $\mathrm{WithTop}$ applied to $x_{1}$. Then $x_{3}$ is a stopping time with respect to $f$, if for all elements $i$ of $x_{1}$, $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to $\mathrm{Leq} (x_{3} (x_{4}), \operatorname{some} (i))$ is a measurable set.
MeasureTheory.stoppedProcessdefMathlib.Probability.Process.Stopping, function or constantEnglish
Let $u$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be a function from elements of $x$ to elements of $\mathrm{WithTop}$ applied to $x_{2}$. Let $x_{5}$ be an element of $x_{2}$. Let $x_{6}$ be an element of $x$. Then $\operatorname{stoppedProcess}$ applied to $u$, $x_{4}$, $x_{5}$ and $x_{6}$ is an element of $x_{1}$ defined as $u$ applied to $\operatorname{untopA}$ applied to $\MinminMACRoAG {\operatorname{some} (x_{5})}{x_{4} (x_{6})}$ and $x_{6}$.
MeasureTheory.stoppedValuedefMathlib.Probability.Process.Stopping, function or constantEnglish
Let $u$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be a function from elements of $x$ to elements of $\mathrm{WithTop}$ applied to $x_{2}$. Let $x_{4}$ be an element of $x$. Then $\operatorname{stoppedValue}$ applied to $u$, $x_{3}$ and $x_{4}$ is an element of $x_{1}$ defined as $u$ applied to $\operatorname{untopA}$ applied to $x_{3}$ applied to $x_{4}$ and $x_{4}$.
MeasureTheory.Measure.infinitePidefMathlib.Probability.ProductMeasure, function or constantWording
the product measure of x1 (from the docstring)
English
Let $x_{1}$ be a function from elements $i_{1}$ of $x$ to measures of $X$ applied to $i_{1}$. Then the product measure of $i_{1}$ is a measure of the set of functions from elements $i$ of $x$ to elements of $X$ applied to $i$.
MeasureTheory.Measure.infinitePiNatdefMathlib.Probability.ProductMeasure, function or constantWording
the infinite product natural number of x (from the name)
English
Let $x$ be a function from natural numbers $n_{1}$ to measures of $X$ applied to $n_{1}$. Then the infinite product natural number of $n_{1}$ is a measure of the set of functions from natural numbers $n$ to elements of $X$ applied to $n$ defined as the function that maps $x$ to $\operatorname{bind}$ applied to the finite product of the measures of the function that maps $i$ to $n_{1}$ applied to $i$, $\operatorname{coe}$ applied to $\operatorname{traj}$ applied to the function that maps $n$ to the constant of the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {n}}{x_{1}})}$ to elements of $X$ applied to $i_{1}$ and $n_{1}$ applied to $n + 1$ and $0$ and $x$.
MeasureTheory.piContentdefMathlib.Probability.ProductMeasure, function or constantWording
the product content of x1 (from the name)
English
Let $x_{1}$ be a function from elements $i$ of $x$ to measures of $X$ applied to $i$. Then the product content of $i$ is an additive content of $\mathrm{ENNReal}$ and the measurable cylinder of $X$ defined as the function that maps $x_{1}$ to the projective family content of $\mathrm{MeasureTheory\_\_isProjectiveMeasureFamily\_pi}$ applied to $i$.
ProbabilityTheory.truncationdefMathlib.Probability.StrongLaw, function or constantWording
the truncation of A and x1 (from the name)
English
Let $f$ be a function from elements of $x$ to real numbers. Let $A$ be a real number. Let $x_{1}$ be an element of $x$. Then the truncation of $A$ and $x_{1}$ is a real number defined as $\operatorname{comp}$ applied to $\operatorname{indicator}$ applied to $\mathrm{id}$, $f$ and $x_{1}$.