Definitions: Mathlib.Analysis, part 5 of 5

spectralAlgNormdefMathlib.Analysis.Normed.Unbundled.SpectralNorm, function or constant

Wording

the spectral norm of K and L (from the docstring)

English

Let $K$ and $L$ be sets. Then the spectral norm of $K$ and $L$ is an algebra norm of $K$ and $L$.

spectralAlgNorm_of_finiteDimensional_normaldefMathlib.Analysis.Normed.Unbundled.SpectralNorm, function or constant

Wording

the spectral norm of K and L (from the docstring)

English

Let $K$ and $L$ be sets. Then the spectral norm of $K$ and $L$ is an algebra norm of $K$ and $L$.

spectralMulAlgNormdefMathlib.Analysis.Normed.Unbundled.SpectralNorm, function or constant

Wording

the spectral norm of K and L (from the docstring)

English

Let $K$ and $L$ be sets. Then the spectral norm of $K$ and $L$ is a multiplicative algebra norm of $K$ and $L$.

spectralNormdefMathlib.Analysis.Normed.Unbundled.SpectralNorm, function or constant

Wording

the spectral norm of y (from the name)

English

Let $K$ and $L$ be sets. Let $y$ be an element of $L$. Then the spectral norm of $y$ is a real number defined as the spectral value in the minimal polynomial of $K$ and $y$.

spectralValuedefMathlib.Analysis.Normed.Unbundled.SpectralNorm, function or constant

Wording

the spectral value in p (from the docstring)

English

Let $p$ be a polynomial of $R$. Then the spectral value in $p$ is a real number defined as the supremum of $\mathrm{spectralValueTerms}$ applied to $p$.

spectralValueTermsdefMathlib.Analysis.Normed.Unbundled.SpectralNorm, function or constant

Wording

the spectral value term of p and x1 (from the name)

English

Let $p$ be a polynomial of $R$. Let $x_{1}$ be an element of $\Natural$. Then the spectral value term of $p$ and $x_{1}$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Lt} (x_{1} , \operatorname{natDegree} (p))}{(\operatorname{norm} (\operatorname{coeff} (p , x_{1}))^ {\frac{ 1}{\operatorname{natDegree} (p)- x_{1}}})}{0}$.

Mathlib.Analysis.ODE.Basic

IsIntegralCurvedefMathlib.Analysis.ODE.Basic, predicate

Wording

no wording

English

Let $x_{2}$ and $v$ be functions from real numbers to elements of $E$. Then $\mathrm{IsIntegralCurve}$ holds for $x_{2}$ and $v$, if for all real numbers $t$, $\mathrm{HasDerivAt}$ holds for $x_{2}$, $v$ applied to $t$ and $x_{2}$ applied to $t$ and $t$.

IsIntegralCurveAtdefMathlib.Analysis.ODE.Basic, predicate

Wording

no wording

English

Let $x_{2}$ and $v$ be functions from real numbers to elements of $E$. Let $x_{3}$ be a real number. Then $\mathrm{IsIntegralCurveAt}$ holds for $x_{2}$, $v$ and $x_{3}$, if $\operatorname{Eventually}$ holds for the function that maps $t$ to $\mathrm{HasDerivAt}$ applied to $x_{2}$, $v$ applied to $t$ and $x_{2}$ applied to $t$ and $t$ and the neighbourhood filter of $x_{3}$.

IsIntegralCurveOndefMathlib.Analysis.ODE.Basic, predicate

Wording

no wording

English

Let $x_{2}$ and $v$ be functions from real numbers to elements of $E$. Let $s$ be an element of $\wp \Real$. Then $\mathrm{IsIntegralCurveOn}$ holds for $x_{2}$, $v$ and $s$, if for all real numbers $t$, if $t$ is an element of $s$, then $\mathrm{HasDerivWithinAt}$ holds for $x_{2}$, $v$ applied to $t$ and $x_{2}$ applied to $t$, $s$ and $t$.

Mathlib.Analysis.ODE.Gronwall

gronwallBounddefMathlib.Analysis.ODE.Gronwall, function or constant

Wording

no wording

English

Let $x$, $K$, $x_{1}$ and $x_{2}$ be elements of $\Real$. Then $\mathrm{gronwallBound}$ applied to $x$, $K$, $x_{1}$ and $x_{2}$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Eq} (K , 0)}{(x + x_{1} \times x_{2})}{(x \times \operatorname{exp} (K \times x_{2})+ \frac{ x_{1}}{K}\times (\operatorname{exp} (K \times x_{2})- 1))}$.

Mathlib.Analysis.ODE.PicardLindelof

IsPicardLindelofstructureMathlib.Analysis.ODE.PicardLindelof, predicate

Wording

no wording

English

Let $f$ be a function from real numbers and elements of $E$ to elements of $E$. Let $x_{1}$ be an element of $\SetIccMACRoP {\mathrm{tmin}}{\mathrm{tmax}}$. Let $x_{2}$ be an element of $E$. Let $a$, $r$, $L$ and $K$ be elements of $\mathrm{NNReal}$. Then we can say that $\mathrm{IsPicardLindelof}$ holds for $f$, $x_{1}$, $x_{2}$, $a$, $r$, $L$ and $K$.

ODE.FunSpacestructureMathlib.Analysis.ODE.PicardLindelof, type

Wording

function space of r and L (from the name)

English

Let $x_{1}$ be an element of $\SetIccMACRoP {\mathrm{tmin}}{\mathrm{tmax}}$. Let $x_{2}$ be an element of $E$. Let $r$ and $L$ be elements of $\mathrm{NNReal}$. Then the function spaces of $r$ and $L$ are a basic type.

ODE.FunSpace.compProjdefMathlib.Analysis.ODE.PicardLindelof, function or constant

Wording

the composition projection of x3 and t (from the name)

English

Let $x_{3}$ be a function space of $r$ and $L$. Let $t$ be a real number. Then the composition projection of $x_{3}$ and $t$ is an element of $E$.

ODE.FunSpace.nextdefMathlib.Analysis.ODE.PicardLindelof, function or constant

Wording

no wording

English

Assume that $\mathrm{IsPicardLindelof}$ holds for $f$, $x_{2}$, $x_{3}$, $a$, $r$, $L$ and $K$. Assume that $x_{4}$ is an element of the closed ball of $x_{3}$ and $\operatorname{toReal}$ applied to $r$. Let $x_{5}$ be a function space of $r$ and $L$. Then $\operatorname{next}$ applied to $\mathrm{hf}$, $\mathrm{hx}$ and $x_{5}$ is a function space of $r$ and $L$.

ODE.FunSpace.toContinuousMapdefMathlib.Analysis.ODE.PicardLindelof, function or constant

Wording

the continuous map (from the name)

English

The continuous map is an embedding of the set of function spaces of $r$ and $L$ and the set of continuous maps of the set of elements of $\SetIccMACRoP {\mathrm{tmin}}{\mathrm{tmax}}$ and $E$.

ODE.FunSpace.toFundefMathlib.Analysis.ODE.PicardLindelof, function or constant

Wording

the function space of self and x3 (from the name)

English

Let $\mathrm{self}$ be a function space of $r$ and $L$. Let $x_{3}$ be an element of $\SetIccMACRoP {\mathrm{tmin}}{\mathrm{tmax}}$. Then the function space of $\mathrm{self}$ and $x_{3}$ is an element of $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

ODE.picarddefMathlib.Analysis.ODE.PicardLindelof, function or constant

Wording

no wording

English

Let $f$ and $x_{4}$ be functions from real numbers and elements of $E$ to elements of $E$. Let $x_{2}$ and $x_{5}$ be real numbers. Let $x_{3}$ be an element of $E$. Then $\operatorname{picard}$ applied to $f$, $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ is an element of $E$ defined as the sum of $x_{3}$ and the interval integral of $x_{5}$ and the volume.

Mathlib.Analysis.Oscillation

oscillationdefMathlib.Analysis.Oscillation, function or constant

Wording

the oscillation of f and x2 (from the name)

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{2}$ be an element of $E$. Then the oscillation of $f$ and $x_{2}$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $S$ to the infimum of the function that maps $h$ to $\operatorname{ediam}$ applied to $S$.

oscillationWithindefMathlib.Analysis.Oscillation, function or constant

Wording

the oscillation of f (from the docstring)

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $D$ be an element of $\wp E$. Let $x_{2}$ be an element of $E$. Then the oscillation of $f$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $S$ to the infimum of the function that maps $h$ to $\operatorname{ediam}$ applied to $S$.

Mathlib.Analysis.PSeries

SuccDiffBoundeddefMathlib.Analysis.PSeries, predicate

Wording

no wording

English

Let $C$ be a natural number. Let $u$ be a function from natural numbers to natural numbers. Then $\mathrm{SuccDiffBounded}$ holds for $C$ and $u$, if for all natural numbers $n$, $u (n + 2)- u (n + 1)\leq \HSMulhSMulMACRoAL {C}{(u (n + 1)- u (n))}$.

Mathlib.Analysis.Polynomial.CauchyBound

Polynomial.cauchyBounddefMathlib.Analysis.Polynomial.CauchyBound, function or constant

Wording

the Cauchy bound of p (from the name)

English

Let $p$ be a polynomial of $K$. Then the Cauchy bound of $p$ is an element of $\mathrm{NNReal}$ defined as the sum of the quotient of the supremum of the range of the natural degree of $p$ and the function that maps $x_{1}$ to the norm of $\operatorname{coeff}$ applied to $p$ and $x_{1}$ and the norm of the leading coefficient of $p$ and $1$.

Mathlib.Analysis.Polynomial.Fourier

Polynomial.toAddCircledefMathlib.Analysis.Polynomial.Fourier, function or constant

Wording

the additive circle (from the name)

English

The additive circle is an algebra homomorphism of the set of polynomials of the set of complexes and the set of continuous maps of the set of additive circles of the product of $2$ and the product and the set of complexes.

Mathlib.Analysis.Polynomial.MahlerMeasure

Polynomial.logMahlerMeasuredefMathlib.Analysis.Polynomial.MahlerMeasure, function or constant

Wording

the logarithmic Mahler measure of p (from the docstring)

English

Let $p$ be a polynomial of the set of complexes. Then the logarithmic Mahler measure of $p$ is a real number defined as $\operatorname{circleAverage}$ applied to the function that maps $x$ to the logarithm of the norm of the evaluation of $x$ and $p$, $0$ and $1$.

Polynomial.mahlerMeasuredefMathlib.Analysis.Polynomial.MahlerMeasure, function or constant

Wording

the Mahler measure of p (from the docstring)

English

Let $p$ be a polynomial of the set of complexes. Then the Mahler measure of $p$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Neq} (p , 0)}{\operatorname{exp} (\operatorname{logMahlerMeasure} (p))}{0}$.

Polynomial.mapMahlerMeasuredefMathlib.Analysis.Polynomial.MahlerMeasure, function or constant

Wording

the map Mahler measure of p and v (from the name)

English

Let $p$ be a polynomial of $A$. Let $v$ be a ring homomorphism of $A$ and the set of complexes. Then the map Mahler measure of $p$ and $v$ is a real number defined as the Mahler measure of the map of $v$ and $p$.

Mathlib.Analysis.Polynomial.Norm

Polynomial.supNormdefMathlib.Analysis.Polynomial.Norm, function or constant

Wording

the supremum norm of p (from the name)

English

Let $p$ be a polynomial of $A$. Then the supremum norm of $p$ is a real number defined as the Gauss norm of $1$ and $p$.

Mathlib.Analysis.Polynomial.SignRight

Polynomial.signRightdefMathlib.Analysis.Polynomial.SignRight, function or constant

Wording

the right sign of x and p (from the name)

English

Let $x$ be a real number. Let $p$ be a polynomial of $\Real$. Then the right sign of $x$ and $p$ is a sign type defined as $\operatorname{limUnder}$ applied to $\mathrm{nhdsWithin}$ applied to $x$ and $\operatorname{Ioi}$ applied to $x$ and the function that maps $y$ to $\operatorname{sign}$ applied to the evaluation of $y$ and $p$.

Mathlib.Analysis.Quaternion

Quaternion.coeComplexdefMathlib.Analysis.Quaternion, function or constant

Wording

the coercion complex of z (from the name)

English

Let $z$ be a complex. Then the coercion complex of $z$ is a quaternion of $\Real$ defined as $\operatorname{mk}$ applied to the real part of $z$, the imaginary part of $z$, $0$ and $0$.

Quaternion.linearIsometryEquivTupledefMathlib.Analysis.Quaternion, function or constant

Wording

the linear isometry equivalence tuple (from the name)

English

The linear isometry equivalence tuple is a linear isometry equivalence of the set of quaternions of $\Real$ and the set of Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $4$.

Quaternion.ofComplexdefMathlib.Analysis.Quaternion, function or constant

Wording

the quaternion (from the name)

English

The quaternion is an algebra homomorphism of the set of complexes and the set of quaternions of $\Real$.

Mathlib.Analysis.RCLike.Basic

IsRCLikeNormedFieldclassMathlib.Analysis.RCLike.Basic, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{IsRCLikeNormedField}$ holds for $x$.

RCLikeclassMathlib.Analysis.RCLike.Basic, predicate

Wording

no wording

English

Let $K$ be an element of $\mathrm{semiOutParam}$ applied to the set of sets. Then we can say that $\mathrm{RCLike}$ holds for $K$.

RCLike.IdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{I}$ is an element of $K$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

RCLike.cauSeqImdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the imaginary part of f (from the docstring)

English

Let $f$ be an element of $\mathrm{CauSeq}$ applied to $K$ and $\operatorname{norm}$. Then the imaginary part of $f$ is an element of $\mathrm{CauSeq}$ applied to $\Real$ and $\mathrm{abs}$ defined as the function that maps $n$ to $\operatorname{im}$ applied to $n$.

RCLike.cauSeqRedefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the real part of f (from the docstring)

English

Let $f$ be an element of $\mathrm{CauSeq}$ applied to $K$ and $\operatorname{norm}$. Then the real part of $f$ is an element of $\mathrm{CauSeq}$ applied to $\Real$ and $\mathrm{abs}$ defined as the function that maps $n$ to $\operatorname{re}$ applied to $n$.

RCLike.conjAedefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{conjAe}$ is an algebra isomorphism of $K$ and $K$.

RCLike.conjCLEdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{conjCLE}$ is a continuous linear equivalence of $K$ and $K$ defined as the continuous linear equivalence of $\operatorname{conjLIE}$.

RCLike.conjLIEdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{conjLIE}$ is a linear isometry equivalence of $K$ and $K$ defined as $\operatorname{mk}$ applied to the linear equivalence of $\operatorname{conjAe}$ and $\mathrm{RCLike\_\_norm\_conj}$.

RCLike.conjToRingEquivdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the conjugate to ring isomorphism of K (from the name)

English

Let $K$ be a set. Then the conjugate to ring isomorphism of $K$ is a ring isomorphism of $K$ and the set of multiplicative opposites of $K$ defined as the star ring isomorphism.

RCLike.imdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the imaginary part (from the docstring)

English

The imaginary part is an additive monoid homomorphism of $K$ and $\Real$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

RCLike.imCLMdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the imaginary part continuous linear map (from the name)

English

The imaginary part continuous linear map is a strong dual of $\Real$ and $K$.

RCLike.imLmdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{imLm}$ is a linear map of $K$ and $\Real$.

RCLike.mapdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the map of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the map of $x$ and $x_{1}$ is a continuous linear map of $x$ and $x_{1}$.

RCLike.normSqdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the norm squared function (from the docstring)

English

The norm squared function is a monoid with zero homomorphism of $K$ and $\Real$.

RCLike.ofRealdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be a real number. Then $\operatorname{ofReal}$ applied to $x_{1}$ is an element of $K$ defined as the cast of $x_{1}$.

RCLike.ofRealAmdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{ofRealAm}$ is an algebra homomorphism of $\Real$ and $K$ defined as the algebra of $\Real$ and $K$.

RCLike.ofRealCLMdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{ofRealCLM}$ is a continuous linear map of $\Real$ and $K$ defined as the continuous linear map of $\operatorname{ofRealLI}$.

RCLike.ofRealLIdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{ofRealLI}$ is a linear isometry of $\Real$ and $K$ defined as $\operatorname{mk}$ applied to the linear map of $\operatorname{ofRealAm}$ and $\mathrm{RCLike\_\_norm\_ofReal}$.

RCLike.ofRealStarAlgHomdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

Let $K$ be a set. Then $\operatorname{ofRealStarAlgHom}$ applied to $K$ is a star algebra homomorphism of $\Real$ and $K$ defined as the star algebra homomorphism of $\Real$ and $K$.

RCLike.redefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the real part (from the docstring)

English

The real part is an additive monoid homomorphism of $K$ and $\Real$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

RCLike.reCLMdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the real part continuous linear map (from the name)

English

The real part continuous linear map is a strong dual of $\Real$ and $K$.

RCLike.reLmdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

no wording

English

$\operatorname{reLm}$ is a linear map of $K$ and $\Real$.

RCLike.realLinearIsometryEquivdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the real linear isometry equivalence of h (from the name)

English

Assume that $\EqtMACRoH {\operatorname{I}}{0}$. Then the real linear isometry equivalence of $h$ is a linear isometry equivalence of $K$ and $\Real$.

RCLike.realRingEquivdefMathlib.Analysis.RCLike.Basic, function or constant

Wording

the real ring isomorphism of h (from the name)

English

Assume that $\EqtMACRoH {\operatorname{I}}{0}$. Then the real ring isomorphism of $h$ is a ring isomorphism of $K$ and $\Real$.

Mathlib.Analysis.RCLike.ContinuousMap

ContinuousMap.rclikeToRealdefMathlib.Analysis.RCLike.ContinuousMap, function or constant

Wording

no wording

English

Let $f$ be a continuous map of $X$ and $x$. Then $\operatorname{rclikeToReal}$ applied to $f$ is a continuous map of $X$ and $\Real$.

ContinuousMap.realToRCLikedefMathlib.Analysis.RCLike.ContinuousMap, function or constant

Wording

no wording

English

Let $x$ be a set. Let $f$ be a continuous map of $X$ and $\Real$. Then $\operatorname{realToRCLike}$ applied to $x$ and $f$ is a continuous map of $X$ and $x$.

ContinuousMap.realToRCLikeOrderEmbeddingdefMathlib.Analysis.RCLike.ContinuousMap, function or constant

Wording

no wording

English

Let $X$ and $x$ be sets. Then $\operatorname{realToRCLikeOrderEmbedding}$ applied to $X$ and $x$ is an order embedding of the set of continuous maps of $X$ and $\Real$ and the set of continuous maps of $X$ and $x$.

ContinuousMap.realToRCLikeStarAlgHomdefMathlib.Analysis.RCLike.ContinuousMap, function or constant

Wording

no wording

English

Let $X$ and $x$ be sets. Then $\operatorname{realToRCLikeStarAlgHom}$ applied to $X$ and $x$ is a star algebra homomorphism of the set of continuous maps of $X$ and $\Real$ and the set of continuous maps of $X$ and $x$ defined as the composition star algebra homomorphism of $\operatorname{ofRealStarAlgHom}$ applied to $x$.

Mathlib.Analysis.RCLike.Extend

Module.Dual.extendRCLikedefMathlib.Analysis.RCLike.Extend, function or constant

Wording

no wording

English

Let $\mathrm{fr}$ be a dual of $\Real$ and $F$. Then $\operatorname{extendRCLike}$ applied to $\mathrm{fr}$ is a dual of $x$ and $F$.

Module.Dual.extendRCLikeₗdefMathlib.Analysis.RCLike.Extend, function or constant

Wording

the extension (from the docstring)

English

The extension is a linear equivalence of the set of duals of $\Real$ and $F$ and the set of duals of $x$ and $F$.

StrongDual.extendRCLikedefMathlib.Analysis.RCLike.Extend, function or constant

Wording

no wording

English

Let $\mathrm{fr}$ be a strong dual of $\Real$ and $F$. Then $\operatorname{extendRCLike}$ applied to $\mathrm{fr}$ is a strong dual of $x$ and $F$.

StrongDual.extendRCLikeₗdefMathlib.Analysis.RCLike.Extend, function or constant

Wording

the extension (from the docstring)

English

The extension is a linear equivalence of the set of strong duals of $\Real$ and $F$ and the set of strong duals of $x$ and $F$.

Mathlib.Analysis.RCLike.Inner

RCLike.cWeightdefMathlib.Analysis.RCLike.Inner, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{cWeight}$ applied to $x_{2}$ is a real number defined as $\operatorname{const}$ applied to $x$, $\operatorname{inv}$ applied to the cardinality of $x$ and $x_{2}$.

RCLike.wInnerdefMathlib.Analysis.RCLike.Inner, function or constant

Wording

no wording

English

Let $w$ be a function from elements of $x$ to real numbers. Let $f$ be a function from elements $i_{1}$ of $x$ to elements of $E$ applied to $i_{1}$. Let $g$ be a function from elements $i$ of $x$ to elements of $E$ applied to $i$. Then $\operatorname{wInner}$ applied to $w$, $i_{1}$, $f$, $i$ and $g$ is an element of $x_{1}$ defined as the function that maps $i$ and $g$ to $\operatorname{sum} (\FinsetunivMACRoAC , \lambda i . \HSMulhSMulMACRoAL {w (i)}{\operatorname{inner} (x_{1} , i_{1} (i), f (i))}, i , g)$.

Mathlib.Analysis.RCLike.Lemmas

LibraryNote.RCLike_instancedefMathlib.Analysis.RCLike.Lemmas, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_RCLike\_instance}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Mathlib.Analysis.RCLike.Sqrt

Complex.sqrtdefMathlib.Analysis.RCLike.Sqrt, function or constant

Wording

the square root of a (from the docstring)

English

Let $a$ be a complex. Then the square root of $a$ is a complex defined as $a ^ {\operatorname{inv} (2)}$.

RCLike.sqrtdefMathlib.Analysis.RCLike.Sqrt, function or constant

Wording

the square root of a (from the name)

English

Let $a$ be an element of $x$. Then the square root of $a$ is an element of $x$ defined as $\operatorname{map}$ applied to the set of complexes, $x$ and the square root of $\operatorname{map}$ applied to $x$, the set of complexes and $a$.

Mathlib.Analysis.Real.Cardinality

Cardinal.cantorFunctiondefMathlib.Analysis.Real.Cardinality, function or constant

Wording

the Cantor function of c and f (from the name)

English

Let $c$ be a real number. Let $f$ be a function from natural numbers to elements of $\mathrm{Bool}$. Then the Cantor function of $c$ and $f$ is a real number defined as the sum of the function that maps $n$ to $\operatorname{cantorFunctionAux}$ applied to $c$, $f$ and $n$ and $\operatorname{unconditional}$ applied to $\Natural$.

Mathlib.Analysis.Real.Hyperreal

HyperrealdefMathlib.Analysis.Real.Hyperreal, type

Wording

no wording

English

An element of $\mathrm{Hyperreal}$ is a germ of $\operatorname{toFilter}$ applied to $\operatorname{hyperfilter}$ applied to $\Natural$ and $\Real$.

Hyperreal.coeRingHomdefMathlib.Analysis.Real.Hyperreal, function or constant

Wording

the coercion ring homomorphism (from the name)

English

The coercion ring homomorphism is an order ring homomorphism of $\Real$ and $\mathrm{Hyperreal}$.

Hyperreal.epsilondefMathlib.Analysis.Real.Hyperreal, function or constant

Wording

the epsilon (from the name)

English

The epsilon is an element of $\mathrm{Hyperreal}$ defined as $\operatorname{ofSeq}$ applied to the function that maps $n$ to $\operatorname{inv}$ applied to $n$.

Hyperreal.ofRealdefMathlib.Analysis.Real.Hyperreal, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{ofReal}$ applied to $x$ is an element of $\mathrm{Hyperreal}$ defined as the constant of $x$.

Hyperreal.ofSeqdefMathlib.Analysis.Real.Hyperreal, function or constant

Wording

no wording

English

Let $f$ be a function from natural numbers to real numbers. Then $\operatorname{ofSeq}$ applied to $f$ is an element of $\mathrm{Hyperreal}$ defined as the germ corresponding to a global function of $f$.

Hyperreal.omegadefMathlib.Analysis.Real.Hyperreal, function or constant

Wording

the omega (from the name)

English

The omega is an element of $\mathrm{Hyperreal}$ defined as $\operatorname{ofSeq}$ applied to $\operatorname{instNatCast}$.

Mathlib.Analysis.Real.OfDigits

Real.digitsdefMathlib.Analysis.Real.OfDigits, function or constant

Wording

the digit of b and x1 (from the name)

English

Let $x$ be a real number. Let $b$ and $x_{1}$ be natural numbers. Then the digit of $b$ and $x_{1}$ is an element of $\mathrm{Fin}$ applied to $b$ defined as $\operatorname{ofNat}$ applied to $b$ and the floor of $x \times b ^ {(x_{1} + 1)}$.

Real.ofDigitsdefMathlib.Analysis.Real.OfDigits, function or constant

Wording

no wording

English

Let $\mathrm{digits}$ be a function from natural numbers to elements of $\mathrm{Fin}$ applied to $b$. Then $\operatorname{ofDigits}$ applied to $\mathrm{digits}$ is a real number defined as the sum of the function that maps $n$ to $\operatorname{ofDigitsTerm}$ applied to $\mathrm{digits}$ and $n$ and $\operatorname{unconditional}$ applied to $\Natural$.

Real.ofDigitsTermdefMathlib.Analysis.Real.OfDigits, function or constant

Wording

no wording

English

Let $\mathrm{digits}$ be a function from natural numbers to elements of $\mathrm{Fin}$ applied to $b$. Let $x$ be a natural number. Then $\operatorname{ofDigitsTerm}$ applied to $\mathrm{digits}$ and $x$ is a real number defined as $\operatorname{val} (\mathrm{digits} (x))\times \operatorname{inv} (b ^ {(x + 1)})$.

Mathlib.Analysis.Real.Pi.Chudnovsky

chudnovskyDenomdefMathlib.Analysis.Real.Pi.Chudnovsky, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\mathrm{chudnovskyDenom}$ applied to $n$ is a natural number defined as $(3 \times n)! \times (n !)^ {3}\times 640320 ^ {3 \times n}$.

chudnovskyNumdefMathlib.Analysis.Real.Pi.Chudnovsky, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\mathrm{chudnovskyNum}$ applied to $n$ is an integer defined as $\operatorname{neg} (1)^ {n}\times (6 \times n)! \times (545140134 \times n + 13591409)$.

chudnovskySumdefMathlib.Analysis.Real.Pi.Chudnovsky, function or constant

Wording

no wording

English

$\mathrm{chudnovskySum}$ is a real number defined as the product of $\frac{ 12}{640320 ^ {\frac{ 3}{2}}}$ and the sum of the function that maps $n$ to $\operatorname{cast}$ applied to $\mathrm{chudnovskyTerm}$ applied to $n$ and $\operatorname{unconditional}$ applied to $\Natural$.

chudnovskyTermdefMathlib.Analysis.Real.Pi.Chudnovsky, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\mathrm{chudnovskyTerm}$ applied to $n$ is a rational number defined as $\frac{ \mathrm{chudnovskyNum} (n)}{\mathrm{chudnovskyDenom} (n)}$.

Mathlib.Analysis.Real.Pi.Wallis

Real.Wallis.WdefMathlib.Analysis.Real.Pi.Wallis, function or constant

Wording

no wording

English

Let $k$ be a natural number. Then $\operatorname{W}$ applied to $k$ is a real number defined as $\FinsetProd {\FinsetrangeMACRoN {k}}{i}{(\frac{ 2 \times i + 2}{2 \times i + 1}\times \frac{ 2 \times i + 2}{2 \times i + 3})}$.

Mathlib.Analysis.Real.Sqrt

NNReal.sqrtdefMathlib.Analysis.Real.Sqrt, function or constant

Wording

the square root (from the name)

English

The square root is an order isomorphism of $\mathrm{NNReal}$ and $\mathrm{NNReal}$.

NNReal.sqrtHomdefMathlib.Analysis.Real.Sqrt, function or constant

Wording

the square root homomorphism (from the name)

English

The square root homomorphism is a monoid with zero homomorphism of $\mathrm{NNReal}$ and $\mathrm{NNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to the square root and $\mathrm{NNReal\_\_sqrt\_zero}$, $\mathrm{NNReal\_\_sqrt\_one}$ and $\mathrm{NNReal\_\_sqrt\_mul}$.

Real.sqrtdefMathlib.Analysis.Real.Sqrt, function or constant

Wording

the square root of x (from the docstring)

English

Let $x$ be a real number. Then the square root of $x$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{sqrt}$ applied to $\operatorname{toNNReal}$ applied to $x$.

Mathlib.Analysis.SpecialFunctions.Arcosh

Real.arcoshdefMathlib.Analysis.SpecialFunctions.Arcosh, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{arcosh}$ applied to $x$ is a real number defined as the logarithm of the sum of $x$ and the square root of $x ^ {2}- 1$.

Real.coshOpenPartialHomeomorphdefMathlib.Analysis.SpecialFunctions.Arcosh, function or constant

Wording

the cosh open partial homeomorphism (from the name)

English

The cosh open partial homeomorphism is an open partial homeomorphism of $\Real$ and $\Real$.

Real.coshPartialEquivdefMathlib.Analysis.SpecialFunctions.Arcosh, function or constant

Wording

the cosh partial equivalence (from the name)

English

The cosh partial equivalence is a partial equivalence of $\Real$ and $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{cosh}$, $\operatorname{arcosh}$, $\operatorname{Ici}$ applied to $0$, $\operatorname{Ici}$ applied to $1$, the function that maps $r$ and $h$ to $\mathrm{Real\_\_one\_le\_cosh}$ applied to $r$, the function that maps $x$ and $\mathrm{hr}$ to $\mathrm{Real\_\_arcosh\_nonneg}$ applied to $\mathrm{hr}$, the function that maps $x_{1}$ and $\mathrm{hr1}$ to $\mathrm{Real\_\_arcosh\_cosh}$ applied to $\mathrm{hr1}$ and the function that maps $x_{2}$ and $\mathrm{hr2}$ to $\mathrm{Real\_\_cosh\_arcosh}$ applied to $\mathrm{hr2}$.

Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

NNReal.agmdefMathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean, function or constant

Wording

no wording

English

Let $x$ and $y$ be elements of $\mathrm{NNReal}$. Then $\operatorname{agm}$ applied to $x$ and $y$ is an element of $\mathrm{NNReal}$ defined as the infimum of the function that maps $n$ to $\ProdsndMACRoAA {\operatorname{agmSequences} (x , y , n)}$.

NNReal.agmSequencesdefMathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean, function or constant

Wording

no wording

English

Let $x$ and $y$ be elements of $\mathrm{NNReal}$. Let $x_{1}$ be a natural number. Then $\operatorname{agmSequences}$ applied to $x$, $y$ and $x_{1}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{NNReal}$ and $\mathrm{NNReal}$ defined as $\operatorname{iterate}$ applied to the function that maps $p$ to $\ProdmkMACRoU {\operatorname{sqrt} (\ProdfstMACRoZ {p}\times \ProdsndMACRoAA {p})}{(\frac{ \ProdfstMACRoZ {p}+ \ProdsndMACRoAA {p}}{2})}$, $x_{1} + 1$ and $\ProdmkMACRoU {x}{y}$.

Mathlib.Analysis.SpecialFunctions.Arsinh

Real.arsinhdefMathlib.Analysis.SpecialFunctions.Arsinh, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{arsinh}$ applied to $x$ is a real number defined as the logarithm of the sum of $x$ and the square root of $1 + x ^ {2}$.

Real.sinhEquivdefMathlib.Analysis.SpecialFunctions.Arsinh, function or constant

Wording

no wording

English

$\operatorname{sinhEquiv}$ is an equivalence from $\Real$ to $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{sinh}$, $\operatorname{arsinh}$, $\mathrm{Real\_\_arsinh\_sinh}$ and $\mathrm{Real\_\_sinh\_arsinh}$.

Real.sinhHomeomorphdefMathlib.Analysis.SpecialFunctions.Arsinh, function or constant

Wording

no wording

English

$\operatorname{sinhHomeomorph}$ is a homeomorphism of $\Real$ and $\Real$ defined as the homeomorphism of $\operatorname{sinhOrderIso}$.

Real.sinhOrderIsodefMathlib.Analysis.SpecialFunctions.Arsinh, function or constant

Wording

no wording

English

$\operatorname{sinhOrderIso}$ is an order isomorphism of $\Real$ and $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{sinhEquiv}$ and $\mathrm{Real\_\_sinh\_le\_sinh}$.

Mathlib.Analysis.SpecialFunctions.Artanh

Real.artanhdefMathlib.Analysis.SpecialFunctions.Artanh, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{artanh}$ applied to $x$ is a real number defined as the logarithm of the square root of $\frac{ 1 + x}{1 - x}$.

Real.tanhPartialEquivdefMathlib.Analysis.SpecialFunctions.Artanh, function or constant

Wording

no wording

English

$\operatorname{tanhPartialEquiv}$ is a partial equivalence of $\Real$ and $\Real$.

Mathlib.Analysis.SpecialFunctions.Bernstein

bernsteindefMathlib.Analysis.SpecialFunctions.Bernstein, function or constant

Wording

the Bernstein of n and x (from the name)

English

Let $n$ and $x$ be natural numbers. Then the Bernstein of $n$ and $x$ is a continuous map of the set of elements of the unit interval and $\Real$ defined as $\operatorname{toContinuousMapOn}$ applied to the Bernstein polynomial of $n$ and $x$ and the unit interval.

bernstein.zdefMathlib.Analysis.SpecialFunctions.Bernstein, function or constant

Wording

no wording

English

Let $k$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{z}$ applied to $k$ is an element of the unit interval defined as $\frac{ \operatorname{val} (k)}{n}$.

bernsteinApproximationdefMathlib.Analysis.SpecialFunctions.Bernstein, function or constant

Wording

the Bernstein approximation of n and f (from the name)

English

Let $n$ be an element of $\Natural$. Let $f$ be a continuous map of the set of elements of the unit interval and $E$. Then the Bernstein approximation of $n$ and $f$ is a continuous map of the set of elements of the unit interval and $E$ defined as $\FinsetSum {\FinsetunivMACRoAC}{k}{(\HSMulhSMulMACRoAL {\mathrm{bernstein} (n , \operatorname{val} (k))}{\operatorname{const} (\operatorname{Elem} (\mathrm{unitInterval}), f (\operatorname{z} (k)))})}$.

Mathlib.Analysis.SpecialFunctions.Bessel

Complex.besselJdefMathlib.Analysis.SpecialFunctions.Bessel, function or constant

Wording

no wording

English

Let $a$ and $x$ be complexes. Then $\operatorname{besselJ}$ applied to $a$ and $x$ is a complex defined as $(\frac{ x}{2})^ {a}\times \operatorname{regularizedHGFun} (0 , \operatorname{singleton} (a + 1), \operatorname{neg} ((\frac{ x}{2})^ {2}))$.

Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Real.binEntropydefMathlib.Analysis.SpecialFunctions.BinaryEntropy, function or constant

Wording

no wording

English

Let $p$ be a real number. Then $\operatorname{binEntropy}$ applied to $p$ is a real number defined as the sum of the product of $p$ and the logarithm of $\operatorname{inv}$ applied to $p$ and the product of $1 - p$ and the logarithm of $\operatorname{inv}$ applied to $1 - p$.

Real.qaryEntropydefMathlib.Analysis.SpecialFunctions.BinaryEntropy, function or constant

Wording

no wording

English

Let $q$ be a natural number. Let $p$ be a real number. Then $\operatorname{qaryEntropy}$ applied to $q$ and $p$ is a real number defined as the sum of the product of $p$ and the logarithm of $q - 1$ and $\operatorname{binEntropy}$ applied to $p$.

Mathlib.Analysis.SpecialFunctions.CompareExp

Complex.IsExpCmpFilterstructureMathlib.Analysis.SpecialFunctions.CompareExp, predicate

Wording

l is a exponential comparison filter (from the name)

English

Let $l$ be a filter of the set of complexes. Then we can say that $l$ is an exponential comparison filter.

Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Complex.arctandefMathlib.Analysis.SpecialFunctions.Complex.Arctan, function or constant

Wording

no wording

English

Let $z$ be a complex. Then $\operatorname{arctan}$ applied to $z$ is a complex defined as the product of $\frac{ \operatorname{neg} (\operatorname{I})}{2}$ and the logarithm of $\frac{ 1 + z \times \operatorname{I}}{1 - z \times \operatorname{I}}$.

Mathlib.Analysis.SpecialFunctions.Complex.Arg

Complex.argdefMathlib.Analysis.SpecialFunctions.Complex.Arg, function or constant

Wording

no wording

English

Let $x$ be a complex. Then $\operatorname{arg}$ applied to $x$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Leq} (0 , \operatorname{re} (x))}{\operatorname{arcsin} (\frac{ \operatorname{im} (x)}{\operatorname{norm} (x)})}{(\iteMACRoG {\mathrm{Leq} (0 , \operatorname{im} (x))}{(\operatorname{arcsin} (\frac{ \operatorname{im} (\operatorname{neg} (x))}{\operatorname{norm} (x)})+ \operatorname{pi})}{(\operatorname{arcsin} (\frac{ \operatorname{im} (\operatorname{neg} (x))}{\operatorname{norm} (x)})- \operatorname{pi})})}$.

Mathlib.Analysis.SpecialFunctions.Complex.Circle

AddCircle.homeomorphCircledefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

the homeomorphism circle of hT (from the name)

English

Assume that $T \neq 0$. Then the homeomorphism circle of $\mathrm{hT}$ is a homeomorphism of the set of additive circles of $T$ and the set of circles.

AddCircle.homeomorphCircle'defMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

the homeomorphism circle (from the name)

English

The homeomorphism circle is a homeomorphism of the set of additive circles of the product of $2$ and the product and the set of circles.

AddCircle.toCircledefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

the circle of x (from the name)

English

Let $x$ be an additive circle of $T$. Then the circle of $x$ is a circle defined as the lift of $\mathrm{AddCircle\_\_scaled\_exp\_map\_periodic}$ and $x$.

Circle.angleDiffdefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

the angle difference of x and y (from the name)

English

Let $x$ and $y$ be circles. Then the angle difference of $x$ and $y$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Leq} (\operatorname{arg} (x), \operatorname{arg} (y))}{(\operatorname{arg} (y)- \operatorname{arg} (x))}{(2 \times \operatorname{pi} + \operatorname{arg} (y)- \operatorname{arg} (x))}$.

Circle.argEquivdefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

no wording

English

$\operatorname{argEquiv}$ is an equivalence from the set of circles to the set of elements of $\operatorname{Ioc}$ applied to $\operatorname{neg}$ applied to the product and the product.

Circle.argPartialEquivdefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

no wording

English

$\operatorname{argPartialEquiv}$ is a partial equivalence of the set of circles and $\Real$.

Circle.centeredArcdefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

the centered arc of r (from the name)

English

Let $r$ be a real number. Then the centered arc of $r$ is an element of the power set of the set of circles defined as the image of $\operatorname{coe}$ applied to the exponential and $\operatorname{ofPred}$ applied to the function that maps $x$ to the proposition that the absolute value of $x$ is less than $r$.

Circle.pathdefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

the path of x and y (from the name)

English

Let $x$ and $y$ be circles. Then the path of $x$ and $y$ is a path of $x$ and $y$.

Real.Angle.toCircledefMathlib.Analysis.SpecialFunctions.Complex.Circle, function or constant

Wording

the circle of x (from the name)

English

Let $x$ be an angle. Then the circle of $x$ is a circle defined as the lift of $\mathrm{Circle\_\_periodic\_exp}$ and $x$.

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

AddCircle.toCircle_addChardefMathlib.Analysis.SpecialFunctions.Complex.CircleAddChar, function or constant

Wording

the circle additive characteristic (from the name)

English

The circle additive characteristic is an additive characteristic of the set of additive circles of $T$ and the set of circles defined as $\operatorname{mk}$ applied to $\operatorname{toCircle}$, $\mathrm{AddCircle\_\_toCircle\_zero}$ and $\mathrm{AddCircle\_\_toCircle\_add}$.

ZMod.rootsOfUnityAddChardefMathlib.Analysis.SpecialFunctions.Complex.CircleAddChar, function or constant

Wording

the root of n (from the name)

English

Let $n$ be an element of $\Natural$. Then the root of $n$ is an additive characteristic of $\mathrm{ZMod}$ applied to $n$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , \mathrm{Circle})}{x})}$.

ZMod.stdAddChardefMathlib.Analysis.SpecialFunctions.Complex.CircleAddChar, function or constant

Wording

no wording

English

$\operatorname{stdAddChar}$ is an additive characteristic of $\mathrm{ZMod}$ applied to $N$ and the set of complexes defined as the composition additive characteristic of the coercion and the circle.

ZMod.toCircledefMathlib.Analysis.SpecialFunctions.Complex.CircleAddChar, function or constant

Wording

the circle (from the name)

English

The circle is an additive characteristic of $\mathrm{ZMod}$ applied to $N$ and the set of circles defined as the composition additive monoid homomorphism of the circle additive characteristic and the additive circle.

rootsOfUnityCircleEquivdefMathlib.Analysis.SpecialFunctions.Complex.CircleAddChar, function or constant

Wording

the root of n (from the name)

English

Let $n$ be an element of $\Natural$. Then the root of $n$ is a multiplicative equivalence of $\SubtypeSet {x}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , \mathrm{Circle})}{x})}$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , \mathrm{Complex})}{x_{1}})}$.

rootsOfUnitytoCircledefMathlib.Analysis.SpecialFunctions.Complex.CircleAddChar, function or constant

Wording

the root of n (from the name)

English

Let $n$ be an element of $\Natural$. Then the root of $n$ is a monoid homomorphism of $\SubtypeSet {x}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (n , \mathrm{Complex})}{x})}$ and the set of circles.

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

circleMapdefMathlib.Analysis.SpecialFunctions.Complex.CircleMap, function or constant

Wording

the circle map of R and x (from the name)

English

Let $c$ be a complex. Let $R$ and $x$ be real numbers. Then the circle map of $R$ and $x$ is a complex defined as the sum of $c$ and the product of the natural inclusion of the real numbers into the complex numbers of $R$ and the exponential of the product of the natural inclusion of the real numbers into the complex numbers of $x$ and $\operatorname{I}$.

Mathlib.Analysis.SpecialFunctions.Complex.Log

Complex.expOpenPartialHomeomorphdefMathlib.Analysis.SpecialFunctions.Complex.Log, function or constant

Wording

the exponential open partial homeomorphism (from the name)

English

The exponential open partial homeomorphism is an open partial homeomorphism of the set of complexes and the set of complexes.

Complex.logdefMathlib.Analysis.SpecialFunctions.Complex.Log, function or constant

Wording

the logarithm of x (from the name)

English

Let $x$ be a complex. Then the logarithm of $x$ is a complex defined as the sum of the natural inclusion of the real numbers into the complex numbers of the logarithm of the norm of $x$ and the product of the natural inclusion of the real numbers into the complex numbers of $\operatorname{arg}$ applied to $x$ and $\operatorname{I}$.

Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Complex.logTaylordefMathlib.Analysis.SpecialFunctions.Complex.LogBounds, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $x$ be a complex. Then $\operatorname{logTaylor}$ applied to $n$ and $x$ is a complex defined as $\FinsetSum {\FinsetrangeMACRoN {n}}{j}{(\frac{ \operatorname{neg} (1)^ {(j + 1)}\times x ^ {j}}{j})}$.

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

CFC.absdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs, function or constant

Wording

the absolute value of a (from the name)

English

Let $a$ be an element of $A$. Then the absolute value of $a$ is an element of $A$ defined as the square root of the product of the star of $a$ and $a$.

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

CFC.logdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic, function or constant

Wording

the logarithm of a (from the name)

English

Let $a$ be an element of $A$. Then the logarithm of $a$ is an element of $A$ defined as $\mathrm{cfc}$ applied to $\operatorname{log}$ and $a$.

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

CFC.nnrpowdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $A$. Let $y$ be an element of $\mathrm{NNReal}$. Then $\operatorname{nnrpow}$ applied to $a$ and $y$ is an element of $A$ defined as $\mathrm{cfc\_u2099\_}$ applied to the function that maps $x_{5}$ to $\operatorname{nnrpow}$ applied to $x_{5}$ and $y$ and $a$.

CFC.rpowdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic, function or constant

Wording

the real power of a and y (from the name)

English

Let $a$ be an element of $A$. Let $y$ be a real number. Then the real power of $a$ and $y$ is an element of $A$ defined as $\mathrm{cfc}$ applied to the function that maps $x_{5}$ to $x_{5} ^ {y}$ and $a$.

CFC.sqrtdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic, function or constant

Wording

the square root of a (from the name)

English

Let $a$ be an element of $A$. Then the square root of $a$ is an element of $A$ defined as $\mathrm{cfc\_u2099\_}$ applied to $\operatorname{coe}$ applied to the square root and $a$.

NNReal.nnrpowdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $\mathrm{NNReal}$. Then $\operatorname{nnrpow}$ applied to $a$ and $b$ is an element of $\mathrm{NNReal}$ defined as $a ^ {\operatorname{toReal} (b)}$.

Units.cfcRpowdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic, function or constant

Wording

no wording

English

Let $a$ be a unit of $A$. Let $x_{5}$ be a real number. Assume that $\mathrm{autoParam}$ holds for the proposition that $0$ is less than or equal to the underlying value in the base of $a$ and $\mathrm{Units\_\_cfcRpow\_\_\_auto\_1}$. Then $\operatorname{cfcRpow}$ applied to $a$, $x_{5}$ and $\mathrm{ha}$ is a unit of $A$.

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

CFC.conjSqrtdefMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt, function or constant

Wording

the conjugate square root of c (from the name)

English

Let $c$ be an element of $A$. Then the conjugate square root of $c$ is a continuous linear map of $A$ and $A$.

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Real.rpowIntegrand₀₁defMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation, function or constant

Wording

no wording

English

Let $p$, $t$ and $x$ be real numbers. Then $\mathrm{Real\_\_rpowIntegrand\_u2080\_\_u2081\_}$ applied to $p$, $t$ and $x$ is a real number defined as $t ^ {p}\times (\operatorname{inv} (t)- \operatorname{inv} (t + x))$.

Real.rpowIntegrand₁₂defMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation, function or constant

Wording

no wording

English

Let $p$, $t$ and $x$ be real numbers. Then $\mathrm{Real\_\_rpowIntegrand\_u2081\_\_u2082\_}$ applied to $p$, $t$ and $x$ is a real number defined as $t ^ {(p - 1)}\times (\operatorname{inv} (t)\times x + t \times \operatorname{inv} (t + x)- 1)$.

Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

PeriodPairstructureMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, type

Wording

period pair (from the name)

English

The period pairs are a basic type.

PeriodPair.GdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Let $n$ be an element of $\Natural$. Then $\operatorname{G}$ applied to $L$ and $n$ is a complex defined as the sum of the function that maps $l$ to $\operatorname{inv}$ applied to $l ^ {n}$ and $\operatorname{unconditional}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x})}$.

PeriodPair.basisdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the basis of L (from the name)

English

Let $L$ be a period pair. Then the basis of $L$ is a basis of $\Real$ and the set of complexes.

PeriodPair.derivWeierstrassPdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Let $z$ be a complex. Then $\operatorname{derivWeierstrassP}$ applied to $L$ and $z$ is a complex defined as $\operatorname{neg}$ applied to the sum of the function that maps $l$ to $\frac{ 2}{(z - l)^ {3}}$ and $\operatorname{unconditional}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x})}$.

PeriodPair.derivWeierstrassPExceptdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Let $x$ and $z$ be complexes. Then $\operatorname{derivWeierstrassPExcept}$ applied to $L$, $x$ and $z$ is a complex defined as the sum of the function that maps $l$ to $\iteMACRoG {(\EqtMACRoH {l}{x})}{0}{(\frac{ \operatorname{neg} (2)}{(z - l)^ {3}})}$ and $\operatorname{unconditional}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x_{1}})}$.

PeriodPair.derivWeierstrassPExceptSeriesdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the power series expansion of L (from the docstring)

English

Let $L$ be a period pair. Let $x$ and $x_{1}$ be complexes. Then the power series expansion of $L$ is a formal multilinear series of the set of complexes and the set of complexes defined as the formal multilinear series of the set of complexes and the function that maps $i$ to $(i + 1)\times (i + 2)\times (\operatorname{sumInvPow} (x_{1} , i + 3)- \iteMACRoG {(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x})}{\operatorname{inv} ((x - x_{1})^ {(i + 3)})}{0})$.

PeriodPair.g₂defMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Then $\mathrm{PeriodPair\_\_g\_u2082\_}$ applied to $L$ is a complex defined as $60 \times \operatorname{G} (L , 4)$.

PeriodPair.g₃defMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Then $\mathrm{PeriodPair\_\_g\_u2083\_}$ applied to $L$ is a complex defined as $140 \times \operatorname{G} (L , 6)$.

PeriodPair.latticedefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the lattice spanned by a pair of periods of L (from the docstring)

English

Let $L$ be a period pair. Then the lattice spanned by a pair of periods of $L$ is a submodule of $\Integer$ and the set of complexes defined as the span of $\Integer$ and $\operatorname{insert}$ applied to $\mathrm{PeriodPair\_\_\_u3c9\_\_u2081\_}$ applied to $L$ and $\operatorname{singleton}$ applied to $\mathrm{PeriodPair\_\_\_u3c9\_\_u2082\_}$ applied to $L$.

PeriodPair.latticeBasisdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the lattice basis of L (from the name)

English

Let $L$ be a period pair. Then the lattice basis of $L$ is a basis of $\Integer$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x})}$.

PeriodPair.latticeEquivProddefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the equivalence from the lattice generated by a pair of periods to L (from the docstring)

English

Let $L$ be a period pair. Then the equivalence from the lattice generated by a pair of periods to $L$ is a linear equivalence of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x})}$ and $\mathrm{Prod}$ applied to $\Integer$ and $\Integer$ defined as the composition of the composition of the representation of the lattice basis of $L$ and $\operatorname{linearEquivFunOnFinite}$ applied to $\Integer$, $\Integer$ and $\mathrm{Fin}$ applied to $2$ and $\operatorname{finTwoArrow}$ applied to $\Integer$ and $\Integer$.

PeriodPair.sumInvPowdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the sum inverse power of x and r (from the name)

English

Let $L$ be a period pair. Let $x$ be a complex. Let $r$ be an element of $\Natural$. Then the sum inverse power of $x$ and $r$ is a complex defined as the sum of the function that maps $l$ to $\operatorname{inv}$ applied to $(l - x)^ {r}$ and $\operatorname{unconditional}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x_{1}})}$.

PeriodPair.weierstrassPdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Let $z$ be a complex. Then $\operatorname{weierstrassP}$ applied to $L$ and $z$ is a complex defined as the sum of the function that maps $l$ to $\frac{ 1}{(z - l)^ {2}}- \frac{ 1}{l ^ {2}}$ and $\operatorname{unconditional}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x})}$.

PeriodPair.weierstrassPExceptdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Let $x$ and $z$ be complexes. Then $\operatorname{weierstrassPExcept}$ applied to $L$, $x$ and $z$ is a complex defined as the sum of the function that maps $l$ to $\iteMACRoG {(\EqtMACRoH {l}{x})}{0}{(\frac{ 1}{(z - l)^ {2}}- \frac{ 1}{l ^ {2}})}$ and $\operatorname{unconditional}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x_{1}})}$.

PeriodPair.weierstrassPExceptSeriesdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the power series expansion of L (from the docstring)

English

Let $L$ be a period pair. Let $x$ and $x_{1}$ be complexes. Then the power series expansion of $L$ is a formal multilinear series of the set of complexes and the set of complexes defined as the formal multilinear series of the set of complexes and the function that maps $i$ to $\iteMACRoG {\mathrm{Eq} (i , 0)}{\operatorname{weierstrassPExcept} (L , x , x_{1})}{((i + 1)\times (\operatorname{sumInvPow} (x_{1} , i + 2)- \iteMACRoG {(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x})}{\operatorname{inv} ((x - x_{1})^ {(i + 2)})}{0}))}$.

PeriodPair.weierstrassPExceptSummanddefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $L$ be a period pair. Let $x$ and $x_{1}$ be complexes. Let $i$ be an element of $\Natural$. Let $l$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x_{2}})}$. Then $\operatorname{weierstrassPExceptSummand}$ applied to $L$, $x$, $x_{1}$, $i$ and $l$ is a complex.

PeriodPair.weierstrassPSeriesdefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the Weierstrass series of L and x (from the name)

English

Let $L$ be a period pair. Let $x$ be a complex. Then the Weierstrass series of $L$ and $x$ is a formal multilinear series of the set of complexes and the set of complexes defined as the formal multilinear series of the set of complexes and the function that maps $i$ to $\iteMACRoG {\mathrm{Eq} (i , 0)}{\operatorname{weierstrassP} (L , x)}{((i + 1)\times \operatorname{sumInvPow} (x , i + 2))}$.

PeriodPair.weierstrassPSummanddefMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

the Weierstrass summand of i and l (from the name)

English

Let $L$ be a period pair. Let $x$ be a complex. Let $i$ be an element of $\Natural$. Let $l$ be an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{lattice} (L)}{x_{1}})}$. Then the Weierstrass summand of $i$ and $l$ is a complex.

PeriodPair.ω₁defMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a period pair. Then $\mathrm{PeriodPair\_\_\_u3c9\_\_u2081\_}$ applied to $\mathrm{self}$ is a complex defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

PeriodPair.ω₂defMathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a period pair. Then $\mathrm{PeriodPair\_\_\_u3c9\_\_u2082\_}$ applied to $\mathrm{self}$ is a complex defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Mathlib.Analysis.SpecialFunctions.Exp

Real.expOrderIsodefMathlib.Analysis.SpecialFunctions.Exp, function or constant

Wording

the exponential order isomorphism (from the name)

English

The exponential order isomorphism is an order isomorphism of $\Real$ and the set of elements of $\operatorname{Ioi}$ applied to $0$.

Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Complex.GammadefMathlib.Analysis.SpecialFunctions.Gamma.Basic, function or constant

Wording

the Gamma of s (from the name)

English

Let $s$ be a complex. Then the Gamma of $s$ is a complex.

Complex.GammaIntegraldefMathlib.Analysis.SpecialFunctions.Gamma.Basic, function or constant

Wording

the Gamma integral of s (from the name)

English

Let $s$ be a complex. Then the Gamma integral of $s$ is a complex defined as the Bochner integral of $\operatorname{restrict}$ applied to the volume and $\operatorname{Ioi}$ applied to $0$ and the function that maps $x$ to the product of the natural inclusion of the real numbers into the complex numbers of the exponential of $\operatorname{neg}$ applied to $x$ and the exponentiation of the natural inclusion of the real numbers into the complex numbers of $x$ to $s - 1$.

Complex.partialGammadefMathlib.Analysis.SpecialFunctions.Gamma.Basic, function or constant

Wording

the partial Gamma of s and X (from the name)

English

Let $s$ be a complex. Let $X$ be a real number. Then the partial Gamma of $s$ and $X$ is a complex defined as the interval integral of $X$ and the volume.

Real.GammadefMathlib.Analysis.SpecialFunctions.Gamma.Basic, function or constant

Wording

the Gamma of s (from the name)

English

Let $s$ be a real number. Then the Gamma of $s$ is a real number defined as the real part of the Gamma of the natural inclusion of the real numbers into the complex numbers of $s$.

Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Complex.GammaSeqdefMathlib.Analysis.SpecialFunctions.Gamma.Beta, function or constant

Wording

the Gamma sequence of s and n (from the name)

English

Let $s$ be a complex. Let $n$ be a natural number. Then the Gamma sequence of $s$ and $n$ is a complex defined as $\frac{ n ^ {s}\times n !}{\FinsetProd {\FinsetrangeMACRoN {(n + 1)}}{j}{(s + j)}}$.

Complex.betaIntegraldefMathlib.Analysis.SpecialFunctions.Gamma.Beta, function or constant

Wording

the Beta function of u and v (from the docstring)

English

Let $u$ and $v$ be complexes. Then the Beta function of $u$ and $v$ is a complex defined as the interval integral of $1$ and the volume.

Real.GammaSeqdefMathlib.Analysis.SpecialFunctions.Gamma.Beta, function or constant

Wording

the Gamma sequence of s and n (from the name)

English

Let $s$ be a real number. Let $n$ be a natural number. Then the Gamma sequence of $s$ and $n$ is a real number defined as $\frac{ n ^ {s}\times n !}{\FinsetProd {\FinsetrangeMACRoN {(n + 1)}}{j}{(s + j)}}$.

Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Real.BohrMollerup.logGammaSeqdefMathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup, function or constant

Wording

the logarithm Gamma sequence of x and n (from the name)

English

Let $x$ be an element of $\Real$. Let $n$ be an element of $\Natural$. Then the logarithm Gamma sequence of $x$ and $n$ is an element of $\Real$ defined as $x \times \operatorname{log} (n)+ \operatorname{log} (n !)- \FinsetSum {\FinsetrangeMACRoN {(n + 1)}}{m}{\operatorname{log} (x + m)}$.

Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Complex.GammaℂdefMathlib.Analysis.SpecialFunctions.Gamma.Deligne, function or constant

Wording

the Gamma of s (from the name)

English

Let $s$ be a complex. Then the Gamma of $s$ is a complex defined as the product of $2$, the exponentiation of the product of $2$ and the natural inclusion of the real numbers into the complex numbers of the product to $\operatorname{neg}$ applied to $s$ and the Gamma of $s$.

Complex.GammaℝdefMathlib.Analysis.SpecialFunctions.Gamma.Deligne, function or constant

Wording

the Gamma of s (from the name)

English

Let $s$ be a complex. Then the Gamma of $s$ is a complex defined as the product of the exponentiation of the natural inclusion of the real numbers into the complex numbers of the product to $\frac{ \operatorname{neg} (s)}{2}$ and the Gamma of $\frac{ s}{2}$.

Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Complex.digammadefMathlib.Analysis.SpecialFunctions.Gamma.Digamma, function or constant

Wording

no wording

English

Let $x$ be a complex. Then $\operatorname{digamma}$ applied to $x$ is a complex defined as the logarithmic derivative of $\operatorname{Gamma}$ and $x$.

Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

GaussianFourier.verticalIntegraldefMathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform, function or constant

Wording

the vertical integral of c and T (from the name)

English

Let $b$ be a complex. Let $c$ and $T$ be real numbers. Then the vertical integral of $c$ and $T$ is a complex defined as the interval integral of $c$ and the volume.

Mathlib.Analysis.SpecialFunctions.Log.Base

Real.logbdefMathlib.Analysis.SpecialFunctions.Log.Base, function or constant

Wording

no wording

English

Let $b$ and $x$ be real numbers. Then $\operatorname{logb}$ applied to $b$ and $x$ is a real number defined as the quotient of the logarithm of $x$ and the logarithm of $b$.

Mathlib.Analysis.SpecialFunctions.Log.Basic

Real.expPartialHomeomorphdefMathlib.Analysis.SpecialFunctions.Log.Basic, function or constant

Wording

the exponential partial homeomorphism (from the name)

English

The exponential partial homeomorphism is an open partial homeomorphism of $\Real$ and $\Real$.

Real.logdefMathlib.Analysis.SpecialFunctions.Log.Basic, function or constant

Wording

the logarithm of x (from the name)

English

Let $x$ be a real number. Then the logarithm of $x$ is a real number defined as $\mathrm{dite}$ applied to $\mathrm{Eq} (x , 0)$, the function that maps $\mathrm{hx}$ to $0$ and the function that maps $\mathrm{hx1}$ to $\operatorname{symm}$ applied to the exponential order isomorphism and the absolute value of $x$.

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

ENNReal.logdefMathlib.Analysis.SpecialFunctions.Log.ENNRealLog, function or constant

Wording

the logarithm of x (from the name)

English

Let $x$ be an element of $\mathrm{ENNReal}$. Then the logarithm of $x$ is an element of $\mathrm{EReal}$ defined as $\iteMACRoG {(\EqtMACRoH {x}{0})}{\operatorname{bot}}{(\iteMACRoG {(\EqtMACRoH {x}{\operatorname{top}})}{\operatorname{top}}{\operatorname{toEReal} (\operatorname{log} (\operatorname{toReal} (x)))})}$.

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

ENNReal.logHomeomorphdefMathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp, function or constant

Wording

the logarithm homeomorphism (from the name)

English

The logarithm homeomorphism is a homeomorphism of $\mathrm{ENNReal}$ and $\mathrm{EReal}$ defined as the homeomorphism of the logarithm order isomorphism.

ENNReal.logOrderIsodefMathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp, function or constant

Wording

the logarithm order isomorphism (from the name)

English

The logarithm order isomorphism is an order isomorphism of $\mathrm{ENNReal}$ and $\mathrm{EReal}$.

EReal.expHomeomorphdefMathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp, function or constant

Wording

the exponential homeomorphism (from the name)

English

The exponential homeomorphism is a homeomorphism of $\mathrm{EReal}$ and $\mathrm{ENNReal}$ defined as the homeomorphism of the exponential order isomorphism.

EReal.expOrderIsodefMathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp, function or constant

Wording

the exponential order isomorphism (from the name)

English

The exponential order isomorphism is an order isomorphism of $\mathrm{EReal}$ and $\mathrm{ENNReal}$ defined as the inverse of the logarithm order isomorphism.

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

EReal.expdefMathlib.Analysis.SpecialFunctions.Log.ERealExp, function or constant

Wording

the exponential of x (from the name)

English

Let $x$ be an element of $\mathrm{EReal}$. Then the exponential of $x$ is an element of $\mathrm{ENNReal}$.

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Real.negMulLogdefMathlib.Analysis.SpecialFunctions.Log.NegMulLog, function or constant

Wording

the negation multiplicative logarithm of x (from the name)

English

Let $x$ be a real number. Then the negation multiplicative logarithm of $x$ is a real number defined as the product of $\operatorname{neg}$ applied to $x$ and the logarithm of $x$.

Mathlib.Analysis.SpecialFunctions.Log.PosLog

Real.posLogdefMathlib.Analysis.SpecialFunctions.Log.PosLog, function or constant

Wording

the positive part logarithm of x (from the name)

English

Let $x$ be a real number. Then the positive part logarithm of $x$ is a real number defined as the maximum of $0$ and the logarithm of $x$.

Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Real.mulExpNegMulSqdefMathlib.Analysis.SpecialFunctions.MulExpNegMulSq, function or constant

Wording

the multiplicative exponential negation multiplicative square of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be real numbers. Then the multiplicative exponential negation multiplicative square of $x$ and $x_{1}$ is a real number defined as the product of $x_{1}$ and the exponential of $\operatorname{neg}$ applied to $x \times x_{1} \times x_{1}$.

Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

ordinaryHypergeometricdefMathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric, function or constant

Wording

no wording

English

Let $a$, $b$ and $c$ be elements of $x$. Let $x_{6}$ be an element of $x_{1}$. Then $\mathrm{ordinaryHypergeometric}$ applied to $a$, $b$, $c$ and $x_{6}$ is an element of $x_{1}$ defined as the sum of the ordinary hypergeometric series of $b$ and $c$ and $x_{6}$.

ordinaryHypergeometricCoefficientdefMathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric, function or constant

Wording

the ordinary hypergeometric coefficient of c and n (from the name)

English

Let $a$, $b$ and $c$ be elements of $x$. Let $n$ be a natural number. Then the ordinary hypergeometric coefficient of $c$ and $n$ is an element of $x$ defined as the product of $\operatorname{inv}$ applied to $n !$, the evaluation of $a$ and $\mathrm{ascPochhammer}$ applied to $x$ and $n$, the evaluation of $b$ and $\mathrm{ascPochhammer}$ applied to $x$ and $n$ and $\operatorname{inv}$ applied to the evaluation of $c$ and $\mathrm{ascPochhammer}$ applied to $x$ and $n$.

ordinaryHypergeometricSeriesdefMathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric, function or constant

Wording

the ordinary hypergeometric series of b and c (from the name)

English

Let $x_{1}$ be a set. Let $a$, $b$ and $c$ be elements of $x$. Then the ordinary hypergeometric series of $b$ and $c$ is a formal multilinear series of $x_{1}$ and $x_{1}$ defined as the formal multilinear series of $x_{1}$ and $\mathrm{ordinaryHypergeometricCoefficient}$ applied to $c$.

Mathlib.Analysis.SpecialFunctions.PolarCoord

Complex.polarCoorddefMathlib.Analysis.SpecialFunctions.PolarCoord, function or constant

Wording

the polar coordinate (from the name)

English

The polar coordinate is an open partial homeomorphism of the set of complexes and $\mathrm{Prod}$ applied to $\Real$ and $\Real$ defined as the composition open partial homeomorphism of the homeomorphism of the equivalence real product continuous linear map and the polar coordinate.

fderivPiPolarCoordSymmdefMathlib.Analysis.SpecialFunctions.PolarCoord, function or constant

Wording

the derivative of p (from the docstring)

English

Let $p$ be a function from elements of $x$ to elements of $\mathrm{Prod}$ applied to $\Real$ and $\Real$. Then the derivative of $p$ is a continuous linear map of the set of functions from elements of $x$ to elements of $\mathrm{Prod}$ applied to $\Real$ and $\Real$ and the set of functions from elements of $x$ to elements of $\mathrm{Prod}$ applied to $\Real$ and $\Real$ defined as the product of the function that maps $i$ to the composition of the derivative of $p$ applied to $i$ and the projection of $i$.

fderivPolarCoordSymmdefMathlib.Analysis.SpecialFunctions.PolarCoord, function or constant

Wording

the derivative of p (from the docstring)

English

Let $p$ be an element of $\mathrm{Prod}$ applied to $\Real$ and $\Real$. Then the derivative of $p$ is a continuous linear map of $\mathrm{Prod}$ applied to $\Real$ and $\Real$ and $\mathrm{Prod}$ applied to $\Real$ and $\Real$ defined as $\operatorname{toContinuousLinearMap}$ applied to $\operatorname{toLin}$ applied to $\operatorname{finTwoProd}$ applied to $\Real$, $\operatorname{finTwoProd}$ applied to $\Real$ and $\operatorname{of}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{cos}$ applied to $\ProdsndMACRoAA {p}$ and $\operatorname{vecCons}$ applied to the product of $\operatorname{neg}$ applied to $\ProdfstMACRoZ {p}$ and the sin of $\ProdsndMACRoAA {p}$ and $\operatorname{vecEmpty}$ and $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to the sin of $\ProdsndMACRoAA {p}$ and $\operatorname{vecCons}$ applied to $\ProdfstMACRoZ {p}\times \operatorname{cos} (\ProdsndMACRoAA {p})$ and $\operatorname{vecEmpty}$ and $\operatorname{vecEmpty}$.

polarCoorddefMathlib.Analysis.SpecialFunctions.PolarCoord, function or constant

Wording

the polar coordinate (from the name)

English

The polar coordinate is an open partial homeomorphism of $\mathrm{Prod}$ applied to $\Real$ and $\Real$ and $\mathrm{Prod}$ applied to $\Real$ and $\Real$.

Mathlib.Analysis.SpecialFunctions.Pow.Complex

Complex.cpowdefMathlib.Analysis.SpecialFunctions.Pow.Complex, function or constant

Wording

the complex power function of x and y (from the docstring)

English

Let $x$ and $y$ be complexes. Then the complex power function of $x$ and $y$ is a complex defined as $\iteMACRoG {(\EqtMACRoH {x}{0})}{(\iteMACRoG {(\EqtMACRoH {y}{0})}{1}{0})}{\operatorname{exp} (\operatorname{log} (x)\times y)}$.

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

ENNReal.orderIsoRpowdefMathlib.Analysis.SpecialFunctions.Pow.NNReal, function or constant

Wording

the order isomorphism real power of y and hy (from the name)

English

Let $y$ be a real number such that $0 < y$. Then the order isomorphism real power of $y$ and $\mathrm{hy}$ is an order isomorphism of $\mathrm{ENNReal}$ and $\mathrm{ENNReal}$.

ENNReal.rpowdefMathlib.Analysis.SpecialFunctions.Pow.NNReal, function or constant

Wording

the real power function of x and x1 (from the docstring)

English

Let $x$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a real number. Then the real power function of $x$ and $x_{1}$ is an element of $\mathrm{ENNReal}$.

NNReal.orderIsoRpowdefMathlib.Analysis.SpecialFunctions.Pow.NNReal, function or constant

Wording

the order isomorphism real power of y and hy (from the name)

English

Let $y$ be a real number such that $0 < y$. Then the order isomorphism real power of $y$ and $\mathrm{hy}$ is an order isomorphism of $\mathrm{NNReal}$ and $\mathrm{NNReal}$.

NNReal.rpowdefMathlib.Analysis.SpecialFunctions.Pow.NNReal, function or constant

Wording

the nonnegative real power function of x and y (from the docstring)

English

Let $x$ be an element of $\mathrm{NNReal}$. Let $y$ be a real number. Then the nonnegative real power function of $x$ and $y$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{toReal} (x)^ {y}$.

NNReal.rpowMonoidHomdefMathlib.Analysis.SpecialFunctions.Pow.NNReal, function or constant

Wording

the real power monoid homomorphism of r (from the name)

English

Let $r$ be a real number. Then the real power monoid homomorphism of $r$ is a monoid homomorphism of $\mathrm{NNReal}$ and $\mathrm{NNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x$ to $x ^ {r}$ and $\mathrm{NNReal\_\_one\_rpow}$ applied to $r$ and the function that maps $\mathrm{\_x}$ and $\mathrm{\_y}$ to $\mathrm{NNReal\_\_mul\_rpow}$.

Mathlib.Analysis.SpecialFunctions.Pow.Real

Real.rpowdefMathlib.Analysis.SpecialFunctions.Pow.Real, function or constant

Wording

the real power function of x and y (from the docstring)

English

Let $x$ and $y$ be real numbers. Then the real power function of $x$ and $y$ is a real number defined as the real part of the exponentiation of the natural inclusion of the real numbers into the complex numbers of $x$ to the natural inclusion of the real numbers into the complex numbers of $y$.

Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Complex.regularizedGaussHGFundefMathlib.Analysis.SpecialFunctions.RegularizedHypergeometric, function or constant

Wording

no wording

English

Let $a$, $b$, $c$ and $z$ be complexes. Then $\operatorname{regularizedGaussHGFun}$ applied to $a$, $b$, $c$ and $z$ is a complex defined as the sum of $\operatorname{regularizedGaussHGFunSeries}$ applied to $a$, $b$ and $c$ and $z$.

Complex.regularizedGaussHGFunSeriesdefMathlib.Analysis.SpecialFunctions.RegularizedHypergeometric, function or constant

Wording

no wording

English

Let $a$, $b$ and $c$ be complexes. Then there is a formal multilinear series of the set of complexes and the set of complexes. Proof. Let $a$ be arbitrary. Let $b$ be arbitrary. Let $c$ be arbitrary. By a. By b. By Singleton__singleton. By Insert__insert. By c. By Singleton__singleton. By Complex__regularizedHGFunSeries.

Complex.regularizedHGFundefMathlib.Analysis.SpecialFunctions.RegularizedHypergeometric, function or constant

Wording

no wording

English

Let $a$ and $b$ be multisets of the set of complexes. Let $z$ be a complex. Then $\operatorname{regularizedHGFun}$ applied to $a$, $b$ and $z$ is a complex defined as the sum of the regularized hypergeometric series of $a$ and $b$ and $z$.

Complex.regularizedHGFunCoeffdefMathlib.Analysis.SpecialFunctions.RegularizedHypergeometric, function or constant

Wording

no wording

English

Let $a$ and $b$ be multisets of the set of complexes. Let $n$ be a natural number. Then $\operatorname{regularizedHGFunCoeff}$ applied to $a$, $b$ and $n$ is a complex defined as the quotient of the product of the map of the function that maps $x$ to the evaluation of $x$ and $\mathrm{ascPochhammer}$ applied to the set of complexes and $n$ and $a$ and the product of $n !$ and the product of the map of the function that maps $x_{1}$ to the Gamma of $x_{1} + n$ and $b$.

Complex.regularizedHGFunSeriesdefMathlib.Analysis.SpecialFunctions.RegularizedHypergeometric, function or constant

Wording

the regularized hypergeometric series of a and b (from the docstring)

English

Let $a$ and $b$ be multisets of the set of complexes. Then the regularized hypergeometric series of $a$ and $b$ is a formal multilinear series of the set of complexes and the set of complexes defined as the formal multilinear series of the set of complexes and $\operatorname{regularizedHGFunCoeff}$ applied to $a$ and $b$.

Mathlib.Analysis.SpecialFunctions.Sigmoid

OrderEmbedding.sigmoiddefMathlib.Analysis.SpecialFunctions.Sigmoid, function or constant

Wording

no wording

English

$\operatorname{sigmoid}$ is an order embedding of $\Real$ and the set of elements of the unit interval defined as the order embedding of $\operatorname{sigmoid}$ and $\mathrm{unitInterval\_\_sigmoid\_strictMono}$.

Real.sigmoiddefMathlib.Analysis.SpecialFunctions.Sigmoid, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{sigmoid}$ applied to $x$ is a real number defined as $\operatorname{inv}$ applied to the sum of $1$ and the exponential of $\operatorname{neg}$ applied to $x$.

unitInterval.sigmoiddefMathlib.Analysis.SpecialFunctions.Sigmoid, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{sigmoid}$ applied to $x$ is an element of the unit interval.

Mathlib.Analysis.SpecialFunctions.SmoothTransition

Real.smoothTransitiondefMathlib.Analysis.SpecialFunctions.SmoothTransition, function or constant

Wording

the smooth transition of x (from the name)

English

Let $x$ be a real number. Then the smooth transition of $x$ is a real number defined as the quotient of the exponential negation inverse glue of $x$ and the sum of the exponential negation inverse glue of $x$ and the exponential negation inverse glue of $1 - x$.

expNegInvGluedefMathlib.Analysis.SpecialFunctions.SmoothTransition, function or constant

Wording

the exponential negation inverse glue of x (from the name)

English

Let $x$ be an element of $\Real$. Then the exponential negation inverse glue of $x$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Leq} (x , 0)}{0}{\operatorname{exp} (\operatorname{neg} (\operatorname{inv} (x)))}$.

Mathlib.Analysis.SpecialFunctions.Sqrt

Real.sqPartialHomeomorphdefMathlib.Analysis.SpecialFunctions.Sqrt, function or constant

Wording

the square partial homeomorphism (from the name)

English

The square partial homeomorphism is an open partial homeomorphism of $\Real$ and $\Real$.

Mathlib.Analysis.SpecialFunctions.Stirling

Stirling.stirlingSeqdefMathlib.Analysis.SpecialFunctions.Stirling, function or constant

Wording

the Stirling sequence of n (from the name)

English

Let $n$ be a natural number. Then the Stirling sequence of $n$ is a real number defined as the quotient of $n !$ and the product of the square root of $2 \times n$ and the exponentiation of the quotient of $n$ and the exponential of $1$ to $n$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Real.AngledefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, type

Wording

angle (from the name)

English

An angle is an additive circle of the product of $2$ and the product.

Real.Angle.coedefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, function or constant

Wording

the coercion of r (from the name)

English

Let $r$ be a real number. Then the coercion of $r$ is an angle defined as $\operatorname{mk}$ applied to $r$.

Real.Angle.coeHomdefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, function or constant

Wording

the coercion homomorphism (from the name)

English

The coercion homomorphism is an additive monoid homomorphism of $\Real$ and the set of angles defined as $\operatorname{mk'}$ applied to $\operatorname{zmultiples}$ applied to the product of $2$ and the product.

Real.Angle.cosdefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, function or constant

Wording

the cosine of x (from the docstring)

English

Let $x$ be an angle. Then the cosine of $x$ is a real number defined as the lift of $\mathrm{Real\_\_cos\_periodic}$ and $x$.

Real.Angle.signdefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, function or constant

Wording

the sign of x (from the docstring)

English

Let $x$ be an angle. Then the sign of $x$ is a sign type defined as $\operatorname{sign}$ applied to the sine of $x$.

Real.Angle.sindefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, function or constant

Wording

the sine of x (from the docstring)

English

Let $x$ be an angle. Then the sine of $x$ is a real number defined as the lift of $\mathrm{Real\_\_sin\_periodic}$ and $x$.

Real.Angle.tandefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, function or constant

Wording

the tangent of x (from the docstring)

English

Let $x$ be an angle. Then the tangent of $x$ is a real number defined as the quotient of the sine of $x$ and the cosine of $x$.

Real.Angle.toRealdefMathlib.Analysis.SpecialFunctions.Trigonometric.Angle, function or constant

Wording

no wording

English

Let $x$ be an angle. Then $\operatorname{toReal}$ applied to $x$ is a real number.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Real.arctandefMathlib.Analysis.SpecialFunctions.Trigonometric.Arctan, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{arctan}$ applied to $x$ is a real number defined as $\operatorname{symm}$ applied to $\operatorname{tanOrderIso}$ and $x$.

Real.tanOrderIsodefMathlib.Analysis.SpecialFunctions.Trigonometric.Arctan, function or constant

Wording

no wording

English

$\operatorname{tanOrderIso}$ is an order isomorphism of the set of elements of the open interval of $\operatorname{neg}$ applied to the quotient of the product and $2$ and the quotient of the product and $2$ and $\Real$ defined as the composition of the order isomorphism of $\operatorname{tan}$ and the open interval of $\operatorname{neg}$ applied to the quotient of the product and $2$ and the quotient of the product and $2$ and the composition of the order isomorphism of the image of $\operatorname{tan}$ and the open interval of $\operatorname{neg}$ applied to the quotient of the product and $2$ and the quotient of the product and $2$ and the universal set and the universal set.

Real.tanPartialHomeomorphdefMathlib.Analysis.SpecialFunctions.Trigonometric.Arctan, function or constant

Wording

no wording

English

$\operatorname{tanPartialHomeomorph}$ is an open partial homeomorphism of $\Real$ and $\Real$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

NNReal.pidefMathlib.Analysis.SpecialFunctions.Trigonometric.Basic, function or constant

Wording

the product (from the name)

English

The product is an element of $\mathrm{NNReal}$ defined as the product.

Real.pidefMathlib.Analysis.SpecialFunctions.Trigonometric.Basic, function or constant

Wording

the product (from the name)

English

The product is a real number defined as $2 \times \operatorname{choose} (\mathrm{Real\_\_exists\_cos\_eq\_zero})$.

Real.sinOrderIsodefMathlib.Analysis.SpecialFunctions.Trigonometric.Basic, function or constant

Wording

the sin order isomorphism (from the name)

English

The sin order isomorphism is an order isomorphism of the set of elements of $\SetIccMACRoP {\operatorname{neg} (\frac{ \operatorname{pi}}{2})}{(\frac{ \operatorname{pi}}{2})}$ and the set of elements of $\SetIccMACRoP {\operatorname{neg} (1)}{1}$.

Real.sqrtTwoAddSeriesdefMathlib.Analysis.SpecialFunctions.Trigonometric.Basic, function or constant

Wording

the series of x and x1 (from the docstring)

English

Let $x$ be a real number. Let $x_{1}$ be a natural number. Then the series of $x$ and $x_{1}$ is a real number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Real\_\_sqrtTwoAddSeries\_\_\_f}$ applied to $x$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Polynomial.Chebyshev.sumZeroesdefMathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss, function or constant

Wording

no wording

English

Let $n$ be an element of $\Natural$. Let $P$ be a polynomial of $\Real$. Then $\operatorname{sumZeroes}$ applied to $n$ and $P$ is an element of $\Real$ defined as $\frac{ \operatorname{pi}}{n}\times \FinsetSum {\FinsetrangeMACRoN {n}}{i}{\operatorname{eval} (\operatorname{cos} (\frac{ 2 \times i + 1}{2 \times n}\times \operatorname{pi}), P)}$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Polynomial.Chebyshev.nodedefMathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal, function or constant

Wording

the node of n and i (from the name)

English

Let $n$ and $i$ be natural numbers. Then the node of $n$ and $i$ is a real number defined as $\operatorname{cos}$ applied to the quotient of the product of $i$ and the product and $n$.

Polynomial.Chebyshev.sumNodesdefMathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal, function or constant

Wording

the sum node of c and P (from the name)

English

Let $n$ be an element of $\Natural$. Let $c$ be a function from elements of $\Natural$ to elements of $\Real$. Let $P$ be a polynomial of $\Real$. Then the sum node of $c$ and $P$ is an element of $\Real$ defined as $\FinsetSum {\FinsetIicMACRoAJ {n}}{i}{(\operatorname{eval} (\operatorname{node} (n , i), P)\times c (i))}$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Polynomial.Chebyshev.measureTdefMathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality, function or constant

Wording

the measure (from the name)

English

The measure is a measure of $\Real$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

cotTermdefMathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent, function or constant

Wording

no wording

English

Let $x$ be a complex. Let $n$ be a natural number. Then $\mathrm{cotTerm}$ applied to $x$ and $n$ is a complex defined as $\frac{ 1}{x - (n + 1)}+ \frac{ 1}{x + (n + 1)}$.

sineTermdefMathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent, function or constant

Wording

the main term in the infinite product for sine of x and n (from the docstring)

English

Let $x$ be a complex. Let $n$ be a natural number. Then the main term in the infinite product for sine of $x$ and $n$ is a complex defined as $\frac{ \operatorname{neg} (x ^ {2})}{(n + 1)^ {2}}$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Real.arccosdefMathlib.Analysis.SpecialFunctions.Trigonometric.Inverse, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{arccos}$ applied to $x$ is a real number defined as the difference between the quotient of the product and $2$ and $\operatorname{arcsin}$ applied to $x$.

Real.arcsindefMathlib.Analysis.SpecialFunctions.Trigonometric.Inverse, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{arcsin}$ applied to $x$ is a real number.

Real.cosPartialEquivdefMathlib.Analysis.SpecialFunctions.Trigonometric.Inverse, function or constant

Wording

no wording

English

$\operatorname{cosPartialEquiv}$ is a partial equivalence of $\Real$ and $\Real$.

Real.cosPartialHomeomorphdefMathlib.Analysis.SpecialFunctions.Trigonometric.Inverse, function or constant

Wording

no wording

English

$\operatorname{cosPartialHomeomorph}$ is an open partial homeomorphism of $\Real$ and $\Real$.

Real.sinPartialEquivdefMathlib.Analysis.SpecialFunctions.Trigonometric.Inverse, function or constant

Wording

the sin partial equivalence (from the name)

English

The sin partial equivalence is a partial equivalence of $\Real$ and $\Real$.

Real.sinPartialHomeomorphdefMathlib.Analysis.SpecialFunctions.Trigonometric.Inverse, function or constant

Wording

the sin partial homeomorphism (from the name)

English

The sin partial homeomorphism is an open partial homeomorphism of $\Real$ and $\Real$.

Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Real.sincdefMathlib.Analysis.SpecialFunctions.Trigonometric.Sinc, function or constant

Wording

no wording

English

Let $x$ be an element of $\Real$. Then $\operatorname{sinc}$ applied to $x$ is an element of $\Real$ defined as $\iteMACRoG {\mathrm{Eq} (x , 0)}{1}{(\frac{ \operatorname{sin} (x)}{x})}$.

Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

arithGeomdefMathlib.Analysis.SpecificLimits.ArithmeticGeometric, function or constant

Wording

no wording

English

Let $a$, $b$ and $x_{2}$ be elements of $R$. Let $x_{3}$ be a natural number. Then $\mathrm{arithGeom}$ applied to $a$, $b$, $x_{2}$ and $x_{3}$ is an element of $R$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{arithGeom\_\_\_f}$ applied to $a$, $b$ and $x_{2}$.

Mathlib.Analysis.SpecificLimits.Basic

posSumOfEncodabledefMathlib.Analysis.SpecificLimits.Basic, function or constant

Wording

the positive part sum of h and x1 (from the name)

English

Assume that $0 < x$. Let $x_{1}$ be a set. Then the positive part sum of $h$ and $x_{1}$ is an element of $\SubtypeSet {x_{3}}{\mathrm{and} (\mathrm{forall} (x_{1} , \lambda i . \mathrm{Lt} (0 , x_{3} (i))), \mathrm{exists} (\Real , \lambda c . \mathrm{and} (\mathrm{HasSum} (x_{3} , c , \operatorname{unconditional} (x_{1})), \mathrm{Leq} (c , x))))}$ defined as $\operatorname{comp}$ applied to the function that maps $n$ to $\frac{ \frac{ x}{2}}{2 ^ {n}}$ and $\operatorname{encode}$.

Mathlib.Analysis.SpecificLimits.Normed

HasSummableGeomSeriesclassMathlib.Analysis.SpecificLimits.Normed, predicate

Wording

no wording

English

Let $K$ be a set. Then we can say that $\mathrm{HasSummableGeomSeries}$ holds for $K$.

Units.oneSubdefMathlib.Analysis.SpecificLimits.Normed, function or constant

Wording

the one difference of t and h1 (from the name)

English

Let $t$ be an element of $R$ such that the norm of $t$ is less than $1$. Then the one difference of $t$ and $h_{1}$ is a unit of $R$ defined as $\operatorname{mk}$ applied to $1 - t$, the sum of the function that maps $n$ to $t ^ {n}$ and $\operatorname{unconditional}$ applied to $\Natural$, $\mathrm{mul\_neg\_geom\_series}$ applied to $t$ and $h_{1}$ and $\mathrm{geom\_series\_mul\_neg}$ applied to $t$ and $h_{1}$.

Mathlib.Analysis.Subadditive

SubadditivedefMathlib.Analysis.Subadditive, predicate

Wording

u is subadditive (from the docstring)

English

Let $u$ be a function from elements of $x$ to elements of $x_{1}$. Then $u$ is subadditive, if for all elements $m$ and $n$ of $x$, $u (m + n)\leq u (m)+ u (n)$.

Subadditive.limdefMathlib.Analysis.Subadditive, function or constant

Wording

the limit of _h (from the docstring)

English

Assume that $u$ is subadditive. Then the limit of $\mathrm{\_h}$ is a real number defined as the infimum of the image of the function that maps $n$ to $\frac{ u (n)}{n}$ and $\operatorname{Ici}$ applied to $1$.

SubmultiplicativedefMathlib.Analysis.Subadditive, predicate

Wording

u is submultiplicative (from the docstring)

English

Let $u$ be a function from elements of $x$ to elements of $x_{1}$. Then $u$ is submultiplicative, if for all elements $m$ and $n$ of $x$, $u (m + n)\leq u (m)\times u (n)$.

Submultiplicative.limdefMathlib.Analysis.Subadditive, function or constant

Wording

the limit of the nth roots of _h (from the docstring)

English

Assume that $u$ is submultiplicative. Then the limit of the nth roots of $\mathrm{\_h}$ is a real number defined as the infimum of the image of the function that maps $n$ to $u (n)^ {\operatorname{inv} (n)}$ and $\operatorname{Ici}$ applied to $1$.

Mathlib.Analysis.VonNeumannAlgebra.Basic

VonNeumannAlgebrastructureMathlib.Analysis.VonNeumannAlgebra.Basic, type

Wording

no wording

English

Let $H$ be a set. Then the elements of $\mathrm{VonNeumannAlgebra}$ applied to $H$ are a basic type.

VonNeumannAlgebra.commutantdefMathlib.Analysis.VonNeumannAlgebra.Basic, function or constant

Wording

no wording

English

Let $S$ be an element of $\mathrm{VonNeumannAlgebra}$ applied to $H$. Then $\operatorname{commutant}$ applied to $S$ is an element of $\mathrm{VonNeumannAlgebra}$ applied to $H$.