Definitions: Mathlib.Analysis, part 2 of 5

Complex.canonicalFactordefMathlib.Analysis.Complex.CanonicalDecomposition, function or constant

Wording

the canonical factor of w and x (from the name)

English

Let $R$ be a real number. Let $w$ and $x$ be complexes. Then the canonical factor of $w$ and $x$ is a complex defined as the quotient of the difference between the exponentiation of the natural inclusion of the real numbers into the complex numbers of $R$ to $2$ and the product of $\operatorname{starRingEnd}$ applied to the set of complexes and $w$ and $x$ and the product of the natural inclusion of the real numbers into the complex numbers of $R$ and $x - w$.

Mathlib.Analysis.Complex.Circle

CircledefMathlib.Analysis.Complex.Circle, type

Wording

circle (from the name)

English

A circle is an element of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{unitSphere} (\mathrm{Complex})}{x})}$.

Circle.coeHomdefMathlib.Analysis.Complex.Circle, function or constant

Wording

the coercion (from the docstring)

English

The coercion is a monoid homomorphism of the set of circles and the set of complexes defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x$ to the proposition that $x$ is an element of the unit sphere of the set of complexes and $\mathrm{Circle\_\_coe\_one}$ and $\mathrm{Circle\_\_coe\_mul}$.

Circle.expdefMathlib.Analysis.Complex.Circle, function or constant

Wording

the exponential (from the name)

English

The exponential is a continuous map of $\Real$ and the set of circles.

Circle.expHomdefMathlib.Analysis.Complex.Circle, function or constant

Wording

the exponential homomorphism (from the name)

English

The exponential homomorphism is an additive monoid homomorphism of $\Real$ and $\mathrm{Additive}$ applied to the set of circles defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofMul}$ and $\operatorname{coe}$ applied to the exponential and $\mathrm{Circle\_\_exp\_zero}$ and $\mathrm{Circle\_\_exp\_add}$.

Circle.ofConjDivSelfdefMathlib.Analysis.Complex.Circle, function or constant

Wording

the circle of z and hz (from the name)

English

Let $z$ be a complex such that $z \neq 0$. Then the circle of $z$ and $\mathrm{hz}$ is a circle defined as the quotient of $\operatorname{starRingEnd}$ applied to the set of complexes and $z$ and $z$.

Circle.toUnitsdefMathlib.Analysis.Complex.Circle, function or constant

Wording

the unit (from the name)

English

The unit is a monoid homomorphism of the set of circles and the set of units of the set of complexes defined as the unit sphere to unit of the set of complexes.

Real.fourierChardefMathlib.Analysis.Complex.Circle, function or constant

Wording

the Fourier characteristic (from the name)

English

The Fourier characteristic is an additive characteristic of $\Real$ and the set of circles.

Real.probChardefMathlib.Analysis.Complex.Circle, function or constant

Wording

no wording

English

$\operatorname{probChar}$ is an additive characteristic of $\Real$ and the set of circles defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to the exponential, $\mathrm{Circle\_\_exp\_zero}$ and $\mathrm{Circle\_\_exp\_add}$.

Mathlib.Analysis.Complex.Conformal

ContinuousLinearMap.complexOfRealdefMathlib.Analysis.Complex.Conformal, function or constant

Wording

the complex of x2 and h (from the name)

English

Let $x_{2}$ be a continuous linear map of the set of complexes and $E$ such that $\EqtMACRoH {x_{2} (\operatorname{I})}{\HSMulhSMulMACRoAL {\operatorname{I}}{x_{2} (1)}}$. Then the complex of $x_{2}$ and $h$ is a continuous linear map of the set of complexes and $E$.

LinearMap.complexOfRealdefMathlib.Analysis.Complex.Conformal, function or constant

Wording

the complex of x2 and h (from the name)

English

Let $x_{2}$ be a linear map of the set of complexes and $E$ such that $\EqtMACRoH {x_{2} (\operatorname{I})}{\HSMulhSMulMACRoAL {\operatorname{I}}{x_{2} (1)}}$. Then the complex of $x_{2}$ and $h$ is a linear map of the set of complexes and $E$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddHom}$ applied to $x_{2}$ and $\mathrm{real\_linearMap\_map\_smul\_complex}$ applied to $h$.

Mathlib.Analysis.Complex.Exponential

Complex.expdefMathlib.Analysis.Complex.Exponential, function or constant

Wording

the exponential of z (from the name)

English

Let $z$ be a complex. Then the exponential of $z$ is a complex defined as $\operatorname{proj0}$ applied to $\mathrm{Complex\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Complex\_\_Exponential\_\_867311647\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $z$.

Complex.exp'defMathlib.Analysis.Complex.Exponential, function or constant

Wording

the exponential of z (from the name)

English

Let $z$ be a complex. Then the exponential of $z$ is an element of $\mathrm{CauSeq}$ applied to the set of complexes and the function that maps $x$ to the norm of $x$ defined as the function that maps $n$ to $\FinsetSum {\FinsetrangeMACRoN {n}}{m}{(\frac{ z ^ {m}}{m !})}$.

Complex.expMonoidHomdefMathlib.Analysis.Complex.Exponential, function or constant

Wording

the exponential function (from the docstring)

English

The exponential function is a monoid homomorphism of the set of multiplicatives of the set of complexes and the set of complexes.

Real.expdefMathlib.Analysis.Complex.Exponential, function or constant

Wording

the exponential of x (from the name)

English

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

Real.expMonoidHomdefMathlib.Analysis.Complex.Exponential, function or constant

Wording

the exponential function (from the docstring)

English

The exponential function is a monoid homomorphism of the set of multiplicatives of $\Real$ and $\Real$.

Real.expNeardefMathlib.Analysis.Complex.Exponential, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $x$ and $r$ be real numbers. Then $\operatorname{expNear}$ applied to $n$, $x$ and $r$ is a real number defined as $\FinsetSum {\FinsetrangeMACRoN {n}}{m}{(\frac{ x ^ {m}}{m !})}+ \frac{ x ^ {n}}{n !}\times r$.

Mathlib.Analysis.Complex.Hadamard

Complex.HadamardThreeLines.FdefMathlib.Analysis.Complex.Hadamard, function or constant

Wording

no wording

English

Let $f$ be a function from complexes to elements of $E$. Let $x_{2}$ be a real number. Let $z$ be a complex. Then $\operatorname{F}$ applied to $f$, $x_{2}$ and $z$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {\operatorname{invInterpStrip} (f , z , x_{2})}{f (z)}$.

Complex.HadamardThreeLines.interpStripdefMathlib.Analysis.Complex.Hadamard, function or constant

Wording

no wording

English

Let $f$ be a function from complexes to elements of $E$. Let $z$ be a complex. Then $\operatorname{interpStrip}$ applied to $f$ and $z$ is a complex defined as $\iteMACRoG {\mathrm{or} (\mathrm{Eq} (\operatorname{sSupNormIm} (f , 0), 0), \mathrm{Eq} (\operatorname{sSupNormIm} (f , 1), 0))}{0}{(\operatorname{ofReal} (\operatorname{sSupNormIm} (f , 0))^ {(1 - z)}\times \operatorname{ofReal} (\operatorname{sSupNormIm} (f , 1))^ {z})}$.

Complex.HadamardThreeLines.interpStrip'defMathlib.Analysis.Complex.Hadamard, function or constant

Wording

no wording

English

Let $f$ be a function from complexes to elements of $E$. Let $l$ and $u$ be elements of $\Real$. Let $z$ be a complex. Then $\operatorname{interpStrip'}$ applied to $f$, $l$, $u$ and $z$ is a complex defined as $\iteMACRoG {\mathrm{or} (\mathrm{Eq} (\operatorname{sSupNormIm} (f , l), 0), \mathrm{Eq} (\operatorname{sSupNormIm} (f , u), 0))}{0}{(\operatorname{ofReal} (\operatorname{sSupNormIm} (f , l))^ {(1 - \frac{ z - \operatorname{ofReal} (l)}{\operatorname{ofReal} (u)- \operatorname{ofReal} (l)})}\times \operatorname{ofReal} (\operatorname{sSupNormIm} (f , u))^ {\frac{ z - \operatorname{ofReal} (l)}{\operatorname{ofReal} (u)- \operatorname{ofReal} (l)}})}$.

Complex.HadamardThreeLines.invInterpStripdefMathlib.Analysis.Complex.Hadamard, function or constant

Wording

no wording

English

Let $f$ be a function from complexes to elements of $E$. Let $z$ be a complex. Let $x_{1}$ be a real number. Then $\operatorname{invInterpStrip}$ applied to $f$, $z$ and $x_{1}$ is a complex defined as the product of the exponentiation of the sum of the natural inclusion of the real numbers into the complex numbers of $x_{1}$ and the natural inclusion of the real numbers into the complex numbers of the supremum norm imaginary part of $f$ and $0$ to $z - 1$ and the exponentiation of the sum of the natural inclusion of the real numbers into the complex numbers of $x_{1}$ and the natural inclusion of the real numbers into the complex numbers of the supremum norm imaginary part of $f$ and $1$ to $\operatorname{neg}$ applied to $z$.

Complex.HadamardThreeLines.sSupNormImdefMathlib.Analysis.Complex.Hadamard, function or constant

Wording

the supremum norm imaginary part of f and x1 (from the name)

English

Let $f$ be a function from complexes to elements of $E$. Let $x_{1}$ be a real number. Then the supremum norm imaginary part of $f$ and $x_{1}$ is a real number defined as the supremum of the image of $\operatorname{comp}$ applied to $\operatorname{norm}$ and $f$ and the preimage of $\operatorname{re}$ and $\operatorname{singleton}$ applied to $x_{1}$.

Complex.HadamardThreeLines.verticalClosedStripdefMathlib.Analysis.Complex.Hadamard, function or constant

Wording

the vertical closed strip of a and b (from the name)

English

Let $a$ and $b$ be real numbers. Then the vertical closed strip of $a$ and $b$ is an element of the power set of the set of complexes defined as the preimage of $\operatorname{re}$ and $\SetIccMACRoP {a}{b}$.

Complex.HadamardThreeLines.verticalStripdefMathlib.Analysis.Complex.Hadamard, function or constant

Wording

the vertical strip of a and b (from the name)

English

Let $a$ and $b$ be real numbers. Then the vertical strip of $a$ and $b$ is an element of the power set of the set of complexes defined as the preimage of $\operatorname{re}$ and the open interval of $a$ and $b$.

Mathlib.Analysis.Complex.HasPrimitives

Complex.IsConservativeOndefMathlib.Analysis.Complex.HasPrimitives, predicate

Wording

no wording

English

Let $f$ be a function from complexes to elements of $E$. Let $U$ be an element of the power set of the set of complexes. Then $\operatorname{IsConservativeOn}$ holds for $f$ and $U$, if for all complexes $z$ and $w$, if the rectangle of $z$ and $w$ is less than or equal to $U$, then the wedge integral of $w$ and $f$ is equal to $\operatorname{neg}$ applied to the wedge integral of $z$ and $f$.

Complex.IsExactOndefMathlib.Analysis.Complex.HasPrimitives, predicate

Wording

no wording

English

Let $f$ be a function from complexes to elements of $E$. Let $U$ be an element of the power set of the set of complexes. Then $\operatorname{IsExactOn}$ holds for $f$ and $U$, if there exists a function $g$ from complexes to elements of $E$, such that for all complexes $z$, if $z$ is an element of $U$, then $\mathrm{HasDerivAt}$ holds for $g$, $f$ applied to $z$ and $z$.

Complex.wedgeIntegraldefMathlib.Analysis.Complex.HasPrimitives, function or constant

Wording

the wedge integral of w and f (from the name)

English

Let $z$ and $w$ be complexes. Let $f$ be a function from complexes to elements of $E$. Then the wedge integral of $w$ and $f$ is an element of $E$ defined as $\mathrm{intervalIntegral} (\operatorname{re} (w), \operatorname{volume})+ \HSMulhSMulMACRoAL {\operatorname{I}}{\mathrm{intervalIntegral} (\operatorname{im} (w), \operatorname{volume})}$.

Mathlib.Analysis.Complex.IntegerCompl

Complex.integerComplementdefMathlib.Analysis.Complex.IntegerCompl, function or constant

Wording

the integer complement (from the name)

English

The integer complement is an element of the power set of the set of complexes defined as the complement of the range of $\operatorname{instIntCast}$.

Mathlib.Analysis.Complex.Isometry

rotationdefMathlib.Analysis.Complex.Isometry, function or constant

Wording

the rotation (from the name)

English

The rotation is a monoid homomorphism of the set of circles and the set of linear isometry equivalences of the set of complexes and the set of complexes.

rotationOfdefMathlib.Analysis.Complex.Isometry, function or constant

Wording

the rotation of e (from the name)

English

Let $e$ be a linear isometry equivalence of the set of complexes and the set of complexes. Then the rotation of $e$ is a circle defined as the quotient of $e$ applied to $1$ and the natural inclusion of the real numbers into the complex numbers of the norm of $e$ applied to $1$.

Mathlib.Analysis.Complex.LocallyUniformLimit

Complex.cderivdefMathlib.Analysis.Complex.LocallyUniformLimit, function or constant

Wording

no wording

English

Let $r$ be an element of $\Real$. Let $f$ be a function from complexes to elements of $E$. Let $z$ be a complex. Then $\operatorname{cderiv}$ applied to $r$, $f$ and $z$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (2 \times \operatorname{ofReal} (\operatorname{pi})\times \operatorname{I})}{\mathrm{circleIntegral} (z , r)}$.

Mathlib.Analysis.Complex.Norm

Complex.cauSeqConjdefMathlib.Analysis.Complex.Norm, function or constant

Wording

the complex conjugate of f (from the docstring)

English

Let $f$ be an element of $\mathrm{CauSeq}$ applied to the set of complexes and the function that maps $x_{1}$ to the norm of $x_{1}$. Then the complex conjugate of $f$ is an element of $\mathrm{CauSeq}$ applied to the set of complexes and the function that maps $x$ to the norm of $x$ defined as the function that maps $n$ to $\operatorname{starRingEnd}$ applied to the set of complexes and $n$.

Complex.cauSeqImdefMathlib.Analysis.Complex.Norm, function or constant

Wording

the imaginary part of f (from the docstring)

English

Let $f$ be an element of $\mathrm{CauSeq}$ applied to the set of complexes and the function that maps $x$ to the norm of $x$. 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 the imaginary part of $n$.

Complex.cauSeqNormdefMathlib.Analysis.Complex.Norm, function or constant

Wording

the norm of f (from the docstring)

English

Let $f$ be an element of $\mathrm{CauSeq}$ applied to the set of complexes and the function that maps $x$ to the norm of $x$. Then the norm of $f$ is an element of $\mathrm{CauSeq}$ applied to $\Real$ and $\mathrm{abs}$ defined as $\operatorname{comp}$ applied to the function that maps $x$ to the norm of $x$ and $f$.

Complex.cauSeqRedefMathlib.Analysis.Complex.Norm, function or constant

Wording

the real part of f (from the docstring)

English

Let $f$ be an element of $\mathrm{CauSeq}$ applied to the set of complexes and the function that maps $x$ to the norm of $x$. 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 the real part of $n$.

Mathlib.Analysis.Complex.Periodic

Function.Periodic.cuspFunctiondefMathlib.Analysis.Complex.Periodic, function or constant

Wording

the cusp function of f and x (from the name)

English

Let $h$ be a real number. Let $f$ be a function from complexes to complexes. Let $x$ be a complex. Then the cusp function of $f$ and $x$ is a complex defined as $\operatorname{update}$ applied to $\operatorname{comp}$ applied to $f$ and $\operatorname{invQParam}$ applied to $h$, $0$, $\operatorname{limUnder}$ applied to $\mathrm{nhdsWithin}$ applied to $0$ and the complement of $\operatorname{singleton}$ applied to $0$ and $\operatorname{comp}$ applied to $f$ and $\operatorname{invQParam}$ applied to $h$ and $x$.

Function.Periodic.invQParamdefMathlib.Analysis.Complex.Periodic, function or constant

Wording

no wording

English

Let $h$ be a real number. Let $q$ be a complex. Then $\operatorname{invQParam}$ applied to $h$ and $q$ is a complex defined as the product of the quotient of the natural inclusion of the real numbers into the complex numbers of $h$ and the product of $2$, the natural inclusion of the real numbers into the complex numbers of the product and $\operatorname{I}$ and the logarithm of $q$.

Function.Periodic.qParamdefMathlib.Analysis.Complex.Periodic, function or constant

Wording

no wording

English

Let $h$ be a real number. Let $z$ be a complex. Then $\operatorname{qParam}$ applied to $h$ and $z$ is a complex defined as the exponential of the quotient of the product of $2$, the natural inclusion of the real numbers into the complex numbers of the product, $\operatorname{I}$ and $z$ and the natural inclusion of the real numbers into the complex numbers of $h$.

Mathlib.Analysis.Complex.Poisson

herglotzRieszKerneldefMathlib.Analysis.Complex.Poisson, function or constant

Wording

no wording

English

Let $c$, $w$ and $z$ be complexes. Then $\mathrm{herglotzRieszKernel}$ applied to $c$, $w$ and $z$ is a complex defined as $\frac{ z - c + (w - c)}{z - c - (w - c)}$.

poissonKerneldefMathlib.Analysis.Complex.Poisson, function or constant

Wording

the Poisson kernel of w and z (from the name)

English

Let $c$, $w$ and $z$ be complexes. Then the Poisson kernel of $w$ and $z$ is a real number defined as the quotient of the difference between the exponentiation of the norm of $z - c$ to $2$ and the exponentiation of the norm of $w - c$ to $2$ and the exponentiation of the norm of $z - c - (w - c)$ to $2$.

Mathlib.Analysis.Complex.Polynomial.GaussLucas

Polynomial.derivRootWeightdefMathlib.Analysis.Complex.Polynomial.GaussLucas, function or constant

Wording

no wording

English

Let $P$ be a polynomial of the set of complexes. Let $z$ and $w$ be complexes. Then $\operatorname{derivRootWeight}$ applied to $P$, $z$ and $w$ is an element of $\Real$ defined as $\iteMACRoG {(\EqtMACRoH {\operatorname{eval} (z , P)}{0})}{\operatorname{single} (z , 1 , w)}{(\frac{ \operatorname{rootMultiplicity} (w , P)}{\operatorname{norm} (z - w)^ {2}})}$.

Mathlib.Analysis.Complex.Trigonometric

Complex.cosdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $z$ be a complex. Then $\operatorname{cos}$ applied to $z$ is a complex defined as the quotient of the sum of the exponential of $z \times \operatorname{I}$ and the exponential of $\operatorname{neg} (z)\times \operatorname{I}$ and $2$.

Complex.coshdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

the cosh of z (from the name)

English

Let $z$ be a complex. Then the cosh of $z$ is a complex defined as the quotient of the sum of the exponential of $z$ and the exponential of $\operatorname{neg}$ applied to $z$ and $2$.

Complex.cotdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $z$ be a complex. Then $\operatorname{cot}$ applied to $z$ is a complex defined as the quotient of $\operatorname{cos}$ applied to $z$ and the sin of $z$.

Complex.sindefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

the sin of z (from the name)

English

Let $z$ be a complex. Then the sin of $z$ is a complex defined as the quotient of the product of the difference between the exponential of $\operatorname{neg} (z)\times \operatorname{I}$ and the exponential of $z \times \operatorname{I}$ and $\operatorname{I}$ and $2$.

Complex.sinhdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $z$ be a complex. Then $\operatorname{sinh}$ applied to $z$ is a complex defined as the quotient of the difference between the exponential of $z$ and the exponential of $\operatorname{neg}$ applied to $z$ and $2$.

Complex.tandefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $z$ be a complex. Then $\operatorname{tan}$ applied to $z$ is a complex defined as the quotient of the sin of $z$ and $\operatorname{cos}$ applied to $z$.

Complex.tanhdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $z$ be a complex. Then $\operatorname{tanh}$ applied to $z$ is a complex defined as the quotient of $\operatorname{sinh}$ applied to $z$ and the cosh of $z$.

Real.cosdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{cos}$ applied to $x$ is a real number defined as the real part of $\operatorname{cos}$ applied to the natural inclusion of the real numbers into the complex numbers of $x$.

Real.coshdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

the cosh of x (from the name)

English

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

Real.cotdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{cot}$ applied to $x$ is a real number defined as the real part of $\operatorname{cot}$ applied to the natural inclusion of the real numbers into the complex numbers of $x$.

Real.sindefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

the sin of x (from the name)

English

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

Real.sinhdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{sinh}$ applied to $x$ is a real number defined as the real part of $\operatorname{sinh}$ applied to the natural inclusion of the real numbers into the complex numbers of $x$.

Real.tandefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{tan}$ applied to $x$ is a real number defined as the real part of $\operatorname{tan}$ applied to the natural inclusion of the real numbers into the complex numbers of $x$.

Real.tanhdefMathlib.Analysis.Complex.Trigonometric, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{tanh}$ applied to $x$ is a real number defined as the real part of $\operatorname{tanh}$ applied to the natural inclusion of the real numbers into the complex numbers of $x$.

Mathlib.Analysis.Complex.UnitDisc.Basic

Complex.UnitClosedDiscdefMathlib.Analysis.Complex.UnitDisc.Basic, type

Wording

unit closed disc (from the name)

English

A unit closed disc is an element of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{unitClosedBall} (\mathrm{Complex})}{x})}$.

Complex.UnitClosedDisc.casesOndefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

no wording

English

Let $\mathrm{mk}$ be a function from complexes $z_{1}$ and elements $\mathrm{hz}$ of $\mathrm{Proof}$ applied to the proposition that the norm of $z_{1}$ is less than or equal to $1$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $z_{1}$ and $\mathrm{hz}$. Let $z$ be a unit closed disc. Then $\operatorname{casesOn}$ applied to $z_{1}$, $\mathrm{hz}$, $\mathrm{mk}$ and $z$ is an element of $\mathrm{motive}$ applied to $z$ defined as the function that maps $\mathrm{mk}$ and $z$ to $z_{1}$ applied to the coercion of $\mathrm{hz}$, $\mathrm{Complex\_\_UnitClosedDisc\_\_norm\_le\_one}$ applied to $\mathrm{hz}$, $\mathrm{mk}$ and $z$.

Complex.UnitClosedDisc.coedefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

the coercion of x (from the name)

English

Let $x$ be a unit closed disc. Then the coercion of $x$ is a complex defined as the proposition that $x$ is an element of the unit closed ball of the set of complexes.

Complex.UnitClosedDisc.imdefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

the imaginary part of z (from the name)

English

Let $z$ be a unit closed disc. Then the imaginary part of $z$ is a real number defined as the imaginary part of the coercion of $z$.

Complex.UnitClosedDisc.mkdefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

no wording

English

Let $z$ be a complex such that the norm of $z$ is less than or equal to $1$. Then $\operatorname{mk}$ applied to $z$ and $\mathrm{hz}$ is a unit closed disc defined as $z$.

Complex.UnitClosedDisc.redefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

the real part of z (from the name)

English

Let $z$ be a unit closed disc. Then the real part of $z$ is a real number defined as the real part of the coercion of $z$.

Complex.UnitDiscdefMathlib.Analysis.Complex.UnitDisc.Basic, type

Wording

unit disc (from the name)

English

A unit disc is an element of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{unitBall} (\mathrm{Complex})}{x})}$.

Complex.UnitDisc.casesOndefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

no wording

English

Let $\mathrm{mk}$ be a function from complexes $z_{1}$ and elements $\mathrm{hz}$ of $\mathrm{Proof}$ applied to the proposition that the norm of $z_{1}$ is less than $1$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $z_{1}$ and $\mathrm{hz}$. Let $z$ be a unit disc. Then $\operatorname{casesOn}$ applied to $z_{1}$, $\mathrm{hz}$, $\mathrm{mk}$ and $z$ is an element of $\mathrm{motive}$ applied to $z$ defined as the function that maps $\mathrm{mk}$ and $z$ to $z_{1}$ applied to the coercion of $\mathrm{hz}$, $\mathrm{Complex\_\_UnitDisc\_\_norm\_lt\_one}$ applied to $\mathrm{hz}$, $\mathrm{mk}$ and $z$.

Complex.UnitDisc.coedefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

the coercion of x (from the name)

English

Let $x$ be a unit disc. Then the coercion of $x$ is a complex defined as the proposition that $x$ is an element of the unit ball of the set of complexes.

Complex.UnitDisc.imdefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

the imaginary part of z (from the name)

English

Let $z$ be a unit disc. Then the imaginary part of $z$ is a real number defined as the imaginary part of the coercion of $z$.

Complex.UnitDisc.mkdefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

no wording

English

Let $z$ be a complex such that the norm of $z$ is less than $1$. Then $\operatorname{mk}$ applied to $z$ and $\mathrm{hz}$ is a unit disc defined as $z$.

Complex.UnitDisc.redefMathlib.Analysis.Complex.UnitDisc.Basic, function or constant

Wording

the real part of z (from the name)

English

Let $z$ be a unit disc. Then the real part of $z$ is a real number defined as the real part of the coercion of $z$.

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

UpperHalfPlanestructureMathlib.Analysis.Complex.UpperHalfPlane.Basic, type

Wording

upper half plane (from the name)

English

The upper half planes are a basic type.

UpperHalfPlane.IdefMathlib.Analysis.Complex.UpperHalfPlane.Basic, function or constant

Wording

no wording

English

$\operatorname{I}$ is a upper half plane.

UpperHalfPlane.coedefMathlib.Analysis.Complex.UpperHalfPlane.Basic, function or constant

Wording

the coercion of self (from the name)

English

Let $\mathrm{self}$ be a upper half plane. Then the coercion of $\mathrm{self}$ is a complex defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

UpperHalfPlane.imdefMathlib.Analysis.Complex.UpperHalfPlane.Basic, function or constant

Wording

the imaginary part of z (from the name)

English

Let $z$ be a upper half plane. Then the imaginary part of $z$ is a real number defined as the imaginary part of the coercion of $z$.

UpperHalfPlane.redefMathlib.Analysis.Complex.UpperHalfPlane.Basic, function or constant

Wording

the real part of z (from the name)

English

Let $z$ be a upper half plane. Then the real part of $z$ is a real number defined as the real part of the coercion of $z$.

UpperHalfPlane.upperHalfPlaneSetdefMathlib.Analysis.Complex.UpperHalfPlane.Basic, function or constant

Wording

the upper half plane (from the docstring)

English

The upper half plane is an element of the power set of the set of complexes defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to the proposition that $0$ is less than the imaginary part of $z$.

UpperHalfPlane.ρdefMathlib.Analysis.Complex.UpperHalfPlane.Basic, function or constant

Wording

no wording

English

$\mathrm{UpperHalfPlane\_\_\_u3c1\_}$ is a upper half plane.

Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

UpperHalfPlane.fixedPtdefMathlib.Analysis.Complex.UpperHalfPlane.FixedPoints, function or constant

Wording

the unique fixed point of g and hell (from the docstring)

English

Let $g$ be an elliptic general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then the unique fixed point of $g$ and $\mathrm{hell}$ is a upper half plane.

Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

UpperHalfPlane.IsBoundedAtImInftydefMathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty, predicate

Wording

f is bounded at imaginary part infty (from the name)

English

Let $f$ be a function from upper half planes to elements of $x$. Then $f$ is bounded at imaginary part infty, if $\operatorname{BoundedAtFilter}$ holds for $\operatorname{atImInfty}$ and $f$.

UpperHalfPlane.IsZeroAtImInftydefMathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty, predicate

Wording

f is a zero at imaginary part infty (from the name)

English

Let $f$ be a function from upper half planes to elements of $x$. Then $f$ is a zero at imaginary part infty, if $f$ is a zero at filter with respect to $\operatorname{atImInfty}$.

UpperHalfPlane.atImInftydefMathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty, function or constant

Wording

no wording

English

$\operatorname{atImInfty}$ is a filter of the set of upper half planes defined as the preimage of $\operatorname{im}$ and $\operatorname{atTop}$.

UpperHalfPlane.boundedAtImInftySubalgebradefMathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{boundedAtImInftySubalgebra}$ applied to $x$ is a subalgebra of $x$ and the set of functions from upper half planes to elements of $x$ defined as the bounded filter subalgebra of $x$ and $\operatorname{atImInfty}$.

UpperHalfPlane.zeroAtImInftySubmoduledefMathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty, function or constant

Wording

the zero at imaginary part infty submodule of x (from the name)

English

Let $x$ be a set. Then the zero at imaginary part infty submodule of $x$ is a submodule of $x$ and the set of functions from upper half planes to elements of $x$ defined as the zero at filter submodule of $x$ and $\operatorname{atImInfty}$.

Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

UpperHalfPlane.smulFDerivdefMathlib.Analysis.Complex.UpperHalfPlane.Manifold, function or constant

Wording

the scalar multiple derivative of g and z (from the name)

English

Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$. Let $z$ be a complex. Then the scalar multiple derivative of $g$ and $z$ is a continuous linear map of the set of complexes and the set of complexes defined as the composition of the continuous linear map of the continuous linear equivalence of $\mathrm{UpperHalfPlane\_\_\_u3c3\_}$ applied to $g$ and $\operatorname{restrictScalars}$ applied to $\Real$ and the span singleton of the set of complexes and the quotient of the natural inclusion of the real numbers into the complex numbers of the underlying value in the base of $\operatorname{det}$ applied to $g$ and $\operatorname{denom} (g , z)^ {2}$.

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

UpperHalfPlane.centerdefMathlib.Analysis.Complex.UpperHalfPlane.Metric, function or constant

Wording

the center of z and r (from the name)

English

Let $z$ be a upper half plane. Let $r$ be a real number. Then the center of $z$ and $r$ is a upper half plane.

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

UpperHalfPlane.JdefMathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction, function or constant

Wording

no wording

English

$\operatorname{J}$ is a general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$.

UpperHalfPlane.denomdefMathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction, function or constant

Wording

no wording

English

Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$. Let $z$ be a complex. Then $\operatorname{denom}$ applied to $g$ and $z$ is a complex defined as the sum of the product of the natural inclusion of the real numbers into the complex numbers of the underlying value in the base of $g$ and $z$ and the natural inclusion of the real numbers into the complex numbers of the underlying value in the base of $g$.

UpperHalfPlane.numdefMathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction, function or constant

Wording

the numerator of g and z (from the name)

English

Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$. Let $z$ be a complex. Then the numerator of $g$ and $z$ is a complex defined as the sum of the product of the natural inclusion of the real numbers into the complex numbers of the underlying value in the base of $g$ and $z$ and the natural inclusion of the real numbers into the complex numbers of the underlying value in the base of $g$.

UpperHalfPlane.smulAux'defMathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction, function or constant

Wording

the scalar multiple of g and z (from the name)

English

Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$. Let $z$ be a complex. Then the scalar multiple of $g$ and $z$ is a complex defined as $\mathrm{UpperHalfPlane\_\_\_u3c3\_\_\_app}$ applied to $g$ and the quotient of the numerator of $g$ and $z$ and $\operatorname{denom}$ applied to $g$ and $z$.

UpperHalfPlane.toSL2RdefMathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction, function or constant

Wording

no wording

English

Let $z$ be a upper half plane. Then $\operatorname{toSL2R}$ applied to $z$ is a special linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$ defined as $\operatorname{of}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to the square root of the imaginary part of $z$ and $\operatorname{vecCons}$ applied to the quotient of the real part of $z$ and the square root of the imaginary part of $z$ and $\operatorname{vecEmpty}$ and $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecCons}$ applied to the quotient of $1$ and the square root of the imaginary part of $z$ and $\operatorname{vecEmpty}$ and $\operatorname{vecEmpty}$.

UpperHalfPlane.σdefMathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction, function or constant

Wording

no wording

English

Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $\Real$. Then $\mathrm{UpperHalfPlane\_\_\_u3c3\_}$ applied to $g$ is a continuous algebra isomorphism of the set of complexes and the set of complexes defined as $\iteMACRoG {\mathrm{Lt} (0 , \operatorname{val} (\operatorname{det} (g)))}{\operatorname{refl} (\Real , \mathrm{Complex})}{\operatorname{conjCAE}}$.

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

UpperHalfPlane.ofComplexdefMathlib.Analysis.Complex.UpperHalfPlane.Topology, function or constant

Wording

the upper half plane (from the name)

English

The upper half plane is an open partial homeomorphism of the set of complexes and the set of upper half planes defined as the inverse of the open partial homeomorphism of $\operatorname{coe}$ and $\mathrm{UpperHalfPlane\_\_isOpenEmbedding\_coe}$.

UpperHalfPlane.verticalStripdefMathlib.Analysis.Complex.UpperHalfPlane.Topology, function or constant

Wording

the vertical strip of A and B (from the name)

English

Let $A$ and $B$ be real numbers. Then the vertical strip of $A$ and $B$ is an element of the power set of the set of upper half planes defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to the proposition that the absolute value of the real part of $z$ is less than or equal to $A$ and $B$ is less than or equal to the imaginary part of $z$.

Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

ValueDistribution.characteristicdefMathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction, function or constant

Wording

the characteristic of a and x2 (from the name)

English

Let $f$ be a function from complexes to elements of $E$. Let $a$ be an element of $\mathrm{WithTop}$ applied to $E$. Let $x_{2}$ be a real number. Then the characteristic of $a$ and $x_{2}$ is a real number defined as $\mathrm{plus}$ applied to $\operatorname{proximity}$ applied to $a$, $\operatorname{logCounting}$ applied to $a$ and $x_{2}$.

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Function.locallyFinsuppWithin.logCountingdefMathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic, function or constant

Wording

the logarithm counting (from the name)

English

generation took over the time limit

Function.locallyFinsuppWithin.toClosedBalldefMathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic, function or constant

Wording

the closed ball of r (from the name)

English

generation took over the time limit

ValueDistribution.logCountingdefMathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic, function or constant

Wording

the logarithm counting of a and x4 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $a$ be an element of $\mathrm{WithTop}$ applied to $E$. Let $x_{4}$ be a real number. Then the logarithm counting of $a$ and $x_{4}$ is a real number defined as $\operatorname{recTopCoe}$ applied to $\operatorname{logCounting}$ applied to the negation part of the divisor of $f$ and the universal set, the function that maps $x_{5}$ to $\operatorname{logCounting}$ applied to the positive part part of the divisor of the function that maps $x_{6}$ to $f (x_{6})- x_{5}$ and the universal set, $a$ and $x_{4}$.

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Truncated

ValueDistribution.truncatedLogCountingdefMathlib.Analysis.Complex.ValueDistribution.LogCounting.Truncated, function or constant

Wording

the truncated logarithm counting of a and x4 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $a$ be an element of $\mathrm{WithTop}$ applied to $E$. Let $x_{4}$ be a real number. Then the truncated logarithm counting of $a$ and $x_{4}$ is a real number defined as $\operatorname{recTopCoe}$ applied to $\operatorname{logCounting}$ applied to $\mathrm{Function\_\_locallyFinsuppWithin\_\_truncate\_u2081\_}$ applied to the negation part of the divisor of $f$ and the universal set, the function that maps $x_{5}$ to $\operatorname{logCounting}$ applied to $\mathrm{Function\_\_locallyFinsuppWithin\_\_truncate\_u2081\_}$ applied to the positive part part of the divisor of the function that maps $x_{6}$ to $f (x_{6})- x_{5}$ and the universal set, $a$ and $x_{4}$.

Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

ValueDistribution.proximitydefMathlib.Analysis.Complex.ValueDistribution.Proximity.Basic, function or constant

Wording

the proximity of a and x1 (from the name)

English

Let $f$ be a function from complexes to elements of $E$. Let $a$ be an element of $\mathrm{WithTop}$ applied to $E$. Let $x_{1}$ be a real number. Then the proximity of $a$ and $x_{1}$ is a real number defined as $\operatorname{recTopCoe}$ applied to $\operatorname{circleAverage}$ applied to the function that maps $x_{1}$ to the positive part logarithm of the norm of $f$ applied to $x_{1}$ and $0$, the function that maps $x_{2}$ to $\operatorname{circleAverage}$ applied to the function that maps $x_{3}$ to the positive part logarithm of $\operatorname{inv}$ applied to the norm of $f (x_{3})- x_{2}$ and $0$, $a$ and $x_{1}$.

Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

ValueDistribution.Cartan.cartanKerneldefMathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation, function or constant

Wording

the Cartan kernel of x and x1 (from the name)

English

Let $f$ be a function from complexes to complexes. Let $R$, $x$ and $x_{1}$ be real numbers. Then the Cartan kernel of $x$ and $x_{1}$ is a real number defined as the logarithm of the norm of the difference between $f$ applied to the circle map of $R$ and $x_{1}$ and the circle map of $1$ and $x$.

Mathlib.Analysis.ConstantSpeed

HasConstantSpeedOnWithdefMathlib.Analysis.ConstantSpeed, predicate

Wording

no wording

English

Let $f$ be a function from real numbers to elements of $E$. Let $s$ be an element of $\wp \Real$. Let $l$ be an element of $\mathrm{NNReal}$. Then $\mathrm{HasConstantSpeedOnWith}$ holds for $f$, $s$ and $l$, if for all real numbers $x_{2}$, if $x_{2}$ is an element of $s$, then for all real numbers $y$, if $y$ is an element of $s$, then $\EqtMACRoH {\mathrm{eVariationOn} (f , \operatorname{inter} (s , \SetIccMACRoP {x_{2}}{y}))}{\operatorname{ofReal} (\operatorname{toReal} (l)\times (y - x_{2}))}$.

HasUnitSpeedOndefMathlib.Analysis.ConstantSpeed, predicate

Wording

no wording

English

Let $f$ be a function from real numbers to elements of $E$. Let $s$ be an element of $\wp \Real$. Then $\mathrm{HasUnitSpeedOn}$ holds for $f$ and $s$, if $\mathrm{HasConstantSpeedOnWith}$ holds for $f$, $s$ and $1$.

naturalParameterizationdefMathlib.Analysis.ConstantSpeed, function or constant

Wording

the natural parameterization of a and x4 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Let $x_{4}$ be a real number. Then the natural parameterization of $a$ and $x_{4}$ is an element of $E$ defined as $\operatorname{comp}$ applied to $f$, $\operatorname{invFunOn}$ applied to $\mathrm{variationOnFromTo}$ applied to $f$, $s$ and $a$ and $s$ and $x_{4}$.

Mathlib.Analysis.Convex.AmpleSet

AmpleSetdefMathlib.Analysis.Convex.AmpleSet, predicate

Wording

s is ample (from the docstring)

English

Let $s$ be an element of $\wp F$. Then $s$ is ample, if for all elements $x_{3}$ of $F$, if $x_{3}$ is an element of $s$, then $\operatorname{convexHull}$ applied to $\Real$ and $\mathrm{connectedComponentIn}$ applied to $s$ and $x_{3}$ is equal to the universal set.

Mathlib.Analysis.Convex.Basic

ConvexdefMathlib.Analysis.Convex.Basic, predicate

Wording

s is convex (from the name)

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Then $s$ is convex, if for all elements $x_{5}$ of $E$, if $x_{5}$ is an element of $s$, then $\mathrm{StarConvex}$ holds for $x$, $x_{5}$ and $s$.

convexAddSubmonoiddefMathlib.Analysis.Convex.Basic, function or constant

Wording

the convex additive submonoid of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the convex additive submonoid of $x$ and $E$ is an additive submonoid of $\wp E$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is convex and the function that maps $x_{5}$ and $x_{6}$ to $\operatorname{add}$ and $\mathrm{convex\_zero}$.

Mathlib.Analysis.Convex.Between

SbtwdefMathlib.Analysis.Convex.Between, predicate

Wording

no wording

English

Let $R$ be a set. Let $x_{5}$, $y$ and $z$ be elements of $P$. Then $\mathrm{Sbtw}$ holds for $R$, $x_{5}$, $y$ and $z$, if $\mathrm{Wbtw}$ holds for $R$, $x_{5}$, $y$ and $z$, $y \neq x_{5}$ and $y \neq z$.

WbtwdefMathlib.Analysis.Convex.Between, predicate

Wording

no wording

English

Let $R$ be a set. Let $x_{5}$, $y$ and $z$ be elements of $P$. Then $\mathrm{Wbtw}$ holds for $R$, $x_{5}$, $y$ and $z$, if $y$ is an element of the affine segment of $x_{5}$ and $z$.

affineSegmentdefMathlib.Analysis.Convex.Between, function or constant

Wording

the affine segment of x5 and y (from the name)

English

Let $R$ be a set. Let $x_{5}$ and $y$ be elements of $P$. Then the affine segment of $x_{5}$ and $y$ is an element of $\wp P$ defined as the image of $\operatorname{coe}$ applied to the line map of $x_{5}$ and $y$ and $\SetIccMACRoP {0}{1}$.

Mathlib.Analysis.Convex.BetweenList

List.SbtwdefMathlib.Analysis.Convex.BetweenList, predicate

Wording

no wording

English

Let $R$ be a set. Let $l$ be a list of elements of $P$. Then $\operatorname{Sbtw}$ holds for $R$ and $l$, if $\operatorname{Wbtw}$ holds for $R$ and $l$ and $\operatorname{Pairwise}$ holds for the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Neq} (x_{5} , x_{6})$ and $l$.

List.WbtwdefMathlib.Analysis.Convex.BetweenList, predicate

Wording

no wording

English

Let $R$ be a set. Let $l$ be a list of elements of $P$. Then $\operatorname{Wbtw}$ holds for $R$ and $l$, if $\operatorname{Triplewise}$ holds for $\mathrm{Wbtw}$ applied to $R$ and $l$.

Mathlib.Analysis.Convex.Body

ConvexBodystructureMathlib.Analysis.Convex.Body, type

Wording

convex body of V (from the name)

English

Let $V$ be a set. Then the convex bodies of $V$ are a basic type.

ConvexBody.carrierdefMathlib.Analysis.Convex.Body, function or constant

Wording

the carrier of self (from the name)

English

Let $\mathrm{self}$ be a convex body of $V$. Then the carrier of $\mathrm{self}$ is an element of $\wp V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Analysis.Convex.Combination

Finset.centerMassdefMathlib.Analysis.Convex.Combination, function or constant

Wording

the center mass of w and z (from the name)

English

Let $t$ be a finite set of $x$. Let $w$ be a function from elements of $x$ to elements of $R$. Let $z$ be a function from elements of $x$ to elements of $E$. Then the center mass of $w$ and $z$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (\FinsetSum {t}{i}{w (i)})}{(\FinsetSum {t}{i_{1}}{(\HSMulhSMulMACRoAL {w (i_{1})}{z (i_{1})})})}$.

convexHullAddMonoidHomdefMathlib.Analysis.Convex.Combination, function or constant

Wording

the additive monoid morphism under pointwise addition of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the additive monoid morphism under pointwise addition of $R$ and $E$ is an additive monoid homomorphism of $\wp E$ and $\wp E$.

Mathlib.Analysis.Convex.Cone.Basic

ProperConedefMathlib.Analysis.Convex.Cone.Basic, type

Wording

proper cone of R and E (from the name)

English

Let $R$ and $E$ be sets. Then a proper cone of $R$ and $E$ is an element of the function that maps $R$ and $E$ to the set of closed submodules of $\mathrm{Nonneg}$ applied to $R$ and $E$.

ProperCone.comapdefMathlib.Analysis.Convex.Cone.Basic, function or constant

Wording

the preimage of f and C (from the name)

English

Let $f$ be a continuous linear map of $E$ and $F$. Let $C$ be a proper cone of $R$ and $F$. Then the preimage of $f$ and $C$ is a proper cone of $R$ and $E$ defined as the preimage of $\operatorname{restrictScalars}$ applied to $\mathrm{Nonneg}$ applied to $R$ and $f$ and $C$.

ProperCone.mapdefMathlib.Analysis.Convex.Cone.Basic, function or constant

Wording

the map of f and C (from the name)

English

Let $f$ be a continuous linear map of $E$ and $F$. Let $C$ be a proper cone of $R$ and $E$. Then the map of $f$ and $C$ is a proper cone of $R$ and $F$ defined as the map of $\operatorname{restrictScalars}$ applied to $\mathrm{Nonneg}$ applied to $R$ and $f$ and $C$.

ProperCone.positivedefMathlib.Analysis.Convex.Cone.Basic, function or constant

Wording

the positive cone of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the positive cone of $R$ and $E$ is a proper cone of $R$ and $E$.

ProperCone.toPointedConedefMathlib.Analysis.Convex.Cone.Basic, function or constant

Wording

the pointed cone of C (from the name)

English

Let $C$ be a proper cone of $R$ and $E$. Then the pointed cone of $C$ is a pointed cone of $R$ and $E$ defined as $\operatorname{toSubmodule}$ applied to $C$.

Mathlib.Analysis.Convex.Cone.Closure

ConvexCone.closuredefMathlib.Analysis.Convex.Cone.Closure, function or constant

Wording

the closure of K (from the docstring)

English

Let $K$ be a convex cone of $x$ and $E$. Then the closure of $K$ is a convex cone of $x$ and $E$.

PointedCone.closuredefMathlib.Analysis.Convex.Cone.Closure, function or constant

Wording

the closure of K (from the docstring)

English

Let $K$ be a pointed cone of $x$ and $E$. Then the closure of $K$ is a pointed cone of $x$ and $E$.

Mathlib.Analysis.Convex.Cone.Dual

ProperCone.dualdefMathlib.Analysis.Convex.Cone.Dual, function or constant

Wording

the dual cone of p and s (from the docstring)

English

Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Let $s$ be an element of $\wp M$. Then the dual cone of $p$ and $s$ is a proper cone of $R$ and $N$.

Mathlib.Analysis.Convex.Cone.InnerDual

ProperCone.innerDualdefMathlib.Analysis.Convex.Cone.InnerDual, function or constant

Wording

the dual cone of s (from the docstring)

English

Let $s$ be an element of $\wp E$. Then the dual cone of $s$ is a proper cone of $\Real$ and $E$ defined as the dual cone of the inner product of $E$ and $s$.

Mathlib.Analysis.Convex.DoublyStochasticMatrix

doublyStochasticdefMathlib.Analysis.Convex.DoublyStochasticMatrix, function or constant

Wording

no wording

English

Let $R$ and $n$ be sets. Then $\mathrm{doublyStochastic}$ applied to $R$ and $n$ is a submonoid of the set of matrixes of $n$ and $R$.

Mathlib.Analysis.Convex.EGauge

egaugedefMathlib.Analysis.Convex.EGauge, function or constant

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $x_{3}$ be an element of $E$. Then $\mathrm{egauge}$ applied to $x$, $s$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $c$ to the infimum of the function that maps $h$ to the extended norm of $c$.

Mathlib.Analysis.Convex.Exposed

ContinuousLinearMap.toExposeddefMathlib.Analysis.Convex.Exposed, function or constant

Wording

no wording

English

Let $l$ be a strong dual of $x$ and $E$. Let $A$ be an element of $\wp E$. Then $\operatorname{toExposed}$ applied to $l$ and $A$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{7}$ to the proposition that $x_{7}$ is an element of $A$ and for all elements $y$ of $E$, if $y$ is an element of $A$, then $l (y)\leq l (x_{7})$.

IsExposeddefMathlib.Analysis.Convex.Exposed, predicate

Wording

B is exposed to A (from the name)

English

Let $x$ be a set. Let $A$ and $B$ be elements of $\wp E$. Then $B$ is exposed to $A$, if if $B$ is nonempty, then there exists a strong dual $l$ of $x$ and $E$, such that $\EqtMACRoH {B}{\operatorname{ofPred} (\lambda x_{7} . \mathrm{and} (\MembershipmemMACRoT {A}{x_{7}}, \mathrm{forall} (E , \lambda y . \mathrm{if} (\MembershipmemMACRoT {A}{y}, \mathrm{Leq} (l (y), l (x_{7}))))))}$.

Set.exposedPointsdefMathlib.Analysis.Convex.Exposed, function or constant

Wording

the exposed point of x and A (from the name)

English

Let $x$ be a set. Let $A$ be an element of $\wp E$. Then the exposed point of $x$ and $A$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{7}$ to the proposition that $x_{7}$ is an element of $A$ and there exists a strong dual $l$ of $x$ and $E$ such that for all elements $y$ of $E$, if $y$ is an element of $A$, then $l (y)\leq l (x_{7})$ and if $l (x_{7})\leq l (y)$, then $\EqtMACRoH {y}{x_{7}}$.

Mathlib.Analysis.Convex.Extreme

IsExtremestructureMathlib.Analysis.Convex.Extreme, predicate

Wording

no wording

English

Let $x$ be a set. Let $A$ and $B$ be elements of $\wp E$. Then we can say that $\mathrm{IsExtreme}$ holds for $x$, $A$ and $B$.

Set.extremePointsdefMathlib.Analysis.Convex.Extreme, function or constant

Wording

the extreme point of x and A (from the name)

English

Let $x$ be a set. Let $A$ be an element of $\wp E$. Then the extreme point of $x$ and $A$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{5}$ to the proposition that $x_{5}$ is an element of $A$ and for all elements $x_{6}$ of $E$, if $x_{6}$ is an element of $A$, then for all elements $x_{7}$ of $E$, if $x_{7}$ is an element of $A$, then if $x_{5}$ is an element of the open segment of $x_{6}$ and $x_{7}$, then $\EqtMACRoH {x_{6}}{x_{5}}$.

Mathlib.Analysis.Convex.Function

ConcaveOndefMathlib.Analysis.Convex.Function, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $f$ be a function from elements of $E$ to elements of $x_{1}$. Then $\mathrm{ConcaveOn}$ holds for $x$, $s$ and $f$, if $s$ is convex and for all elements $x_{9}$ of $E$, if $x_{9}$ is an element of $s$, then for all elements $y$ of $E$, if $y$ is an element of $s$, then for all elements $a$ of $x$, for all elements $b$ of $x$, if $0 \leq a$, then if $0 \leq b$, then if $a + b$ is equal to $1$, then $\HSMulhSMulMACRoAL {a}{f (x_{9})}+ \HSMulhSMulMACRoAL {b}{f (y)}\leq f (\HSMulhSMulMACRoAL {a}{x_{9}}+ \HSMulhSMulMACRoAL {b}{y})$.

ConvexOndefMathlib.Analysis.Convex.Function, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $f$ be a function from elements of $E$ to elements of $x_{1}$. Then $\mathrm{ConvexOn}$ holds for $x$, $s$ and $f$, if $s$ is convex and for all elements $x_{9}$ of $E$, if $x_{9}$ is an element of $s$, then for all elements $y$ of $E$, if $y$ is an element of $s$, then for all elements $a$ of $x$, for all elements $b$ of $x$, if $0 \leq a$, then if $0 \leq b$, then if $a + b$ is equal to $1$, then $f (\HSMulhSMulMACRoAL {a}{x_{9}}+ \HSMulhSMulMACRoAL {b}{y})\leq \HSMulhSMulMACRoAL {a}{f (x_{9})}+ \HSMulhSMulMACRoAL {b}{f (y)}$.

StrictConcaveOndefMathlib.Analysis.Convex.Function, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $f$ be a function from elements of $E$ to elements of $x_{1}$. Then $\mathrm{StrictConcaveOn}$ holds for $x$, $s$ and $f$, if $s$ is convex and for all elements $x_{9}$ of $E$, if $\MembershipmemMACRoT {s}{x_{9}}$, then for all elements $y$ of $E$, if $y$ is an element of $s$, then if $x_{9} \neq y$, then for all elements $a$ of $x$, for all elements $b$ of $x$, if $0 < a$, then if $0 < b$, then if $\EqtMACRoH {a + b}{1}$, then $\HSMulhSMulMACRoAL {a}{f (x_{9})}+ \HSMulhSMulMACRoAL {b}{f (y)}< f (\HSMulhSMulMACRoAL {a}{x_{9}}+ \HSMulhSMulMACRoAL {b}{y})$.

StrictConvexOndefMathlib.Analysis.Convex.Function, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $f$ be a function from elements of $E$ to elements of $x_{1}$. Then $\mathrm{StrictConvexOn}$ holds for $x$, $s$ and $f$, if $s$ is convex and for all elements $x_{9}$ of $E$, if $\MembershipmemMACRoT {s}{x_{9}}$, then for all elements $y$ of $E$, if $y$ is an element of $s$, then if $x_{9} \neq y$, then for all elements $a$ of $x$, for all elements $b$ of $x$, if $0 < a$, then if $0 < b$, then if $\EqtMACRoH {a + b}{1}$, then $f (\HSMulhSMulMACRoAL {a}{x_{9}}+ \HSMulhSMulMACRoAL {b}{y})< \HSMulhSMulMACRoAL {a}{f (x_{9})}+ \HSMulhSMulMACRoAL {b}{f (y)}$.

Mathlib.Analysis.Convex.Gauge

gaugedefMathlib.Analysis.Convex.Gauge, function or constant

Wording

the gauge of s and x2 (from the name)

English

Let $s$ be an element of $\wp E$. Let $x_{2}$ be an element of $E$. Then the gauge of $s$ and $x_{2}$ is a real number defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $r$ to the proposition that $0 < r$ and $x_{2}$ is an element of $\HSMulhSMulMACRoAL {r}{s}$.

gaugeSeminormdefMathlib.Analysis.Convex.Gauge, function or constant

Wording

the gauge seminorm of h2 and h3 (from the name)

English

Assume that $s$ is balanced. Assume that $s$ is convex. Assume that $\Real$ is absorbent. Then the gauge seminorm of $h_{2}$ and $h_{3}$ is a seminorm of $x$ and $E$ defined as $\operatorname{of}$ applied to $\mathrm{gauge}$ applied to $s$, $\mathrm{gauge\_add\_le}$ applied to $h_{2}$ and $h_{3}$ and $\mathrm{gauge\_smul}$ applied to $h_{1}$.

Mathlib.Analysis.Convex.GaugeRescale

gaugeRescaledefMathlib.Analysis.Convex.GaugeRescale, function or constant

Wording

no wording

English

Let $s$ and $t$ be elements of $\wp E$. Let $x_{2}$ be an element of $E$. Then $\mathrm{gaugeRescale}$ applied to $s$, $t$ and $x_{2}$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {(\frac{ \mathrm{gauge} (s , x_{2})}{\mathrm{gauge} (t , x_{2})})}{x_{2}}$.

gaugeRescaleEquivdefMathlib.Analysis.Convex.GaugeRescale, function or constant

Wording

no wording

English

Let $s$ and $t$ be elements of $\wp E$. Assume that $\Real$ is absorbent. Assume that $\operatorname{IsVonNBounded}$ holds for $\Real$ and $s$. Assume that $\Real$ is absorbent. Assume that $\operatorname{IsVonNBounded}$ holds for $\Real$ and $t$. Then $\mathrm{gaugeRescaleEquiv}$ applied to $s$, $t$, $\mathrm{hsa}$, $\mathrm{hsb}$, $\mathrm{hta}$ and $\mathrm{htb}$ is an equivalence from $E$ to $E$.

gaugeRescaleHomeomorphdefMathlib.Analysis.Convex.GaugeRescale, function or constant

Wording

no wording

English

Let $s$ and $t$ be elements of $\wp E$ such that $s$ is convex, $s$ is an element of the neighbourhood filter of $0$, $\operatorname{IsVonNBounded}$ holds for $\Real$ and $s$, $t$ is convex, $t$ is an element of the neighbourhood filter of $0$ and $\operatorname{IsVonNBounded}$ holds for $\Real$ and $t$. Then $\mathrm{gaugeRescaleHomeomorph}$ applied to $s$, $t$, $\mathrm{hsc}$, $h_{3}$, $\mathrm{hsb}$, $\mathrm{htc}$, $h_{4}$ and $\mathrm{htb}$ is a homeomorphism of $E$ and $E$.

Mathlib.Analysis.Convex.Hull

convexHulldefMathlib.Analysis.Convex.Hull, function or constant

Wording

the convex hull of x (from the docstring)

English

Let $x$ be a set. Then the convex hull of $x$ is a closure operator of $\wp E$.

Mathlib.Analysis.Convex.Independent

ConvexIndependentdefMathlib.Analysis.Convex.Independent, predicate

Wording

no wording

English

Let $x$ be a set. Let $p$ be a function from elements of $x_{1}$ to elements of $E$. Then $\mathrm{ConvexIndependent}$ holds for $x$ and $p$, if for all elements $s$ of $\wp x_{1}$, for all elements $x_{6}$ of $x_{1}$, if $p$ applied to $x_{6}$ is an element of $\operatorname{convexHull}$ applied to $x$ and the image of $p$ and $s$, then $x_{6}$ is an element of $s$.

Mathlib.Analysis.Convex.Intrinsic

intrinsicClosuredefMathlib.Analysis.Convex.Intrinsic, function or constant

Wording

the intrinsic closure of x and s (from the docstring)

English

Let $x$ be a set. Let $s$ be an element of $\wp P$. Then the intrinsic closure of $x$ and $s$ is an element of $\wp P$ defined as the image of the function that maps $x_{6}$ to the proposition that $x_{6}$ is an element of the affine span of $x$ and $s$ and the closure of the preimage of the function that maps $x_{7}$ to the proposition that $x_{7}$ is an element of the affine span of $x$ and $s$ and $s$.

intrinsicFrontierdefMathlib.Analysis.Convex.Intrinsic, function or constant

Wording

the intrinsic frontier of x and s (from the docstring)

English

Let $x$ be a set. Let $s$ be an element of $\wp P$. Then the intrinsic frontier of $x$ and $s$ is an element of $\wp P$ defined as the image of the function that maps $x_{6}$ to the proposition that $x_{6}$ is an element of the affine span of $x$ and $s$ and the frontier of the preimage of the function that maps $x_{7}$ to the proposition that $x_{7}$ is an element of the affine span of $x$ and $s$ and $s$.

intrinsicInteriordefMathlib.Analysis.Convex.Intrinsic, function or constant

Wording

the intrinsic interior of x and s (from the docstring)

English

Let $x$ be a set. Let $s$ be an element of $\wp P$. Then the intrinsic interior of $x$ and $s$ is an element of $\wp P$ defined as the image of the function that maps $x_{6}$ to the proposition that $x_{6}$ is an element of the affine span of $x$ and $s$ and the interior of the preimage of the function that maps $x_{7}$ to the proposition that $x_{7}$ is an element of the affine span of $x$ and $s$ and $s$.

Mathlib.Analysis.Convex.Join

convexJoindefMathlib.Analysis.Convex.Join, function or constant

Wording

the convex join of s and t (from the name)

English

Let $x$ be a set. Let $s$ and $t$ be elements of $\wp E$. Then the convex join of $s$ and $t$ is an element of $\wp E$ defined as the union of the function that maps $x_{5}$ to the union of the function that maps $h$ to the union of the function that maps $y$ to the union of the function that maps $h_{1}$ to the segment of $x_{5}$ and $y$.

Mathlib.Analysis.Convex.MetricSpace

Convexity.IsConvexDistclassMathlib.Analysis.Convex.MetricSpace, predicate

Wording

X is a convex distance (from the name)

English

Let $X$ be a set. Then we can say that $X$ is a convex distance.

Mathlib.Analysis.Convex.PathConnected

Path.segmentdefMathlib.Analysis.Convex.PathConnected, function or constant

Wording

the segment of a and b (from the name)

English

Let $a$ and $b$ be elements of $E$. Then the segment of $a$ and $b$ is a path of $a$ and $b$.

Mathlib.Analysis.Convex.Quasiconvex

QuasiconcaveOndefMathlib.Analysis.Convex.Quasiconvex, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $f$ be a function from elements of $E$ to elements of $x_{1}$. Then $\mathrm{QuasiconcaveOn}$ holds for $x$, $s$ and $f$, if for all elements $r$ of $x_{1}$, $\operatorname{ofPred}$ applied to the function that maps $x_{7}$ to the proposition that $x_{7}$ is an element of $s$ and $r \leq f (x_{7})$ is convex.

QuasiconvexOndefMathlib.Analysis.Convex.Quasiconvex, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $f$ be a function from elements of $E$ to elements of $x_{1}$. Then $\mathrm{QuasiconvexOn}$ holds for $x$, $s$ and $f$, if for all elements $r$ of $x_{1}$, $\operatorname{ofPred}$ applied to the function that maps $x_{7}$ to the proposition that $x_{7}$ is an element of $s$ and $f (x_{7})\leq r$ is convex.

QuasilinearOndefMathlib.Analysis.Convex.Quasiconvex, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp E$. Let $f$ be a function from elements of $E$ to elements of $x_{1}$. Then $\mathrm{QuasilinearOn}$ holds for $x$, $s$ and $f$, if $\mathrm{QuasiconvexOn}$ holds for $x$, $s$ and $f$ and $\mathrm{QuasiconcaveOn}$ holds for $x$, $s$ and $f$.

Mathlib.Analysis.Convex.Segment

openSegmentdefMathlib.Analysis.Convex.Segment, function or constant

Wording

the open segment of x5 and y (from the name)

English

Let $x$ be a set. Let $x_{5}$ and $y$ be elements of $E$. Then the open segment of $x_{5}$ and $y$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to the proposition that there exist elements $a$ and $b$ of $x$, such that $0 < a$, $0 < b$, $\EqtMACRoH {a + b}{1}$ and $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{5}}+ \HSMulhSMulMACRoAL {b}{y}}{z}$.

segmentdefMathlib.Analysis.Convex.Segment, function or constant

Wording

the segment of x5 and y (from the name)

English

Let $x$ be a set. Let $x_{5}$ and $y$ be elements of $E$. Then the segment of $x_{5}$ and $y$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to the proposition that there exist elements $a$ and $b$ of $x$, such that $0 \leq a$, $0 \leq b$, $\EqtMACRoH {a + b}{1}$ and $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{5}}+ \HSMulhSMulMACRoAL {b}{y}}{z}$.

Mathlib.Analysis.Convex.Side

AffineSubspace.SOppSidedefMathlib.Analysis.Convex.Side, predicate

Wording

no wording

English

Let $s$ be an affine subspace of $R$ and $P$. Let $x_{5}$ and $y$ be elements of $P$. Then $\operatorname{SOppSide}$ holds for $s$, $x_{5}$ and $y$, if $\operatorname{WOppSide}$ holds for $s$, $x_{5}$ and $y$, $x_{5}$ is not an element of $s$ and $y$ is not an element of $s$.

AffineSubspace.SSameSidedefMathlib.Analysis.Convex.Side, predicate

Wording

no wording

English

Let $s$ be an affine subspace of $R$ and $P$. Let $x_{5}$ and $y$ be elements of $P$. Then $\operatorname{SSameSide}$ holds for $s$, $x_{5}$ and $y$, if $\operatorname{WSameSide}$ holds for $s$, $x_{5}$ and $y$, $x_{5}$ is not an element of $s$ and $y$ is not an element of $s$.

AffineSubspace.WOppSidedefMathlib.Analysis.Convex.Side, predicate

Wording

no wording

English

Let $s$ be an affine subspace of $R$ and $P$. Let $x_{5}$ and $y$ be elements of $P$. Then $\operatorname{WOppSide}$ holds for $s$, $x_{5}$ and $y$, if there exists an element $x_{6}$ of $P$, such that $x_{6}$ is an element of $s$ and there exists an element $x_{7}$ of $P$ such that $x_{7}$ is an element of $s$ and $\mathrm{SameRay}$ holds for $R$, the vector difference of $x_{5}$ and $x_{6}$ and the vector difference of $x_{7}$ and $y$.

AffineSubspace.WSameSidedefMathlib.Analysis.Convex.Side, predicate

Wording

no wording

English

Let $s$ be an affine subspace of $R$ and $P$. Let $x_{5}$ and $y$ be elements of $P$. Then $\operatorname{WSameSide}$ holds for $s$, $x_{5}$ and $y$, if there exists an element $x_{6}$ of $P$, such that $x_{6}$ is an element of $s$ and there exists an element $x_{7}$ of $P$ such that $x_{7}$ is an element of $s$ and $\mathrm{SameRay}$ holds for $R$, the vector difference of $x_{5}$ and $x_{6}$ and the vector difference of $y$ and $x_{7}$.

Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Geometry.AbstractSimplicialComplex.ofSimpleGraphdefMathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion, function or constant

Wording

the abstract simplicial complex of G (from the name)

English

Let $G$ be a simple graph of $x$. Then the abstract simplicial complex of $G$ is an abstract simplicial complex of $x$.

Geometry.SimplicialComplex.ofAffineIndependentdefMathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion, function or constant

Wording

the simplicial complex of abstract and indep (from the name)

English

Let $\mathrm{abstract}$ be an abstract simplicial complex of $E$. Assume that $\mathrm{AffineIndependent}$ holds for $x$ and the function that maps $x_{6}$ to the proposition that $x_{6}$ is an element of the union of the function that maps $s$ to the union of the function that maps $h_{1}$ to $s$. Then the simplicial complex of $\mathrm{abstract}$ and $\mathrm{indep}$ is a simplicial complex of $x$ and $E$.

Geometry.SimplicialComplex.ofSimpleGraphdefMathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion, function or constant

Wording

the simplicial complex of G (from the name)

English

Let $G$ be a simple graph of $V$. Then the simplicial complex of $G$ is a simplicial complex of $x$ and $\FinsuppMACRoQ {V}{x}$ defined as $\operatorname{onFinsupp}$ applied to $\operatorname{toPreAbstractSimplicialComplex}$ applied to the abstract simplicial complex of $G$.

Geometry.SimplicialComplex.onFinsuppdefMathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion, function or constant

Wording

no wording

English

Let $\mathrm{abstract}$ be an abstract simplicial complex of $x_{1}$. Then $\operatorname{onFinsupp}$ applied to $\mathrm{abstract}$ is a simplicial complex of $x$ and $\FinsuppMACRoQ {x_{1}}{x}$.

Mathlib.Analysis.Convex.SimplicialComplex.Basic

Geometry.SimplicialComplexstructureMathlib.Analysis.Convex.SimplicialComplex.Basic, type

Wording

simplicial complex of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the simplicial complexes of $x$ and $E$ are a basic type.

Geometry.SimplicialComplex.facetsdefMathlib.Analysis.Convex.SimplicialComplex.Basic, function or constant

Wording

no wording

English

Let $K$ be a simplicial complex of $x$ and $E$. Then $\operatorname{facets}$ applied to $K$ is an element of the power set of the set of finite sets of $E$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is an element of the face of $\operatorname{toPreAbstractSimplicialComplex}$ applied to $K$ and for all finite sets $t$ of $E$, if $t$ is an element of the face of $\operatorname{toPreAbstractSimplicialComplex}$ applied to $K$, then if $s \leq t$, then $\EqtMACRoH {s}{t}$.

Geometry.SimplicialComplex.ofErasedefMathlib.Analysis.Convex.SimplicialComplex.Basic, function or constant

Wording

the simplicial complex of faces (from the name)

English

Let $\mathrm{faces}$ be an element of the power set of the set of finite sets of $E$ such that for all finite sets $s_{1}$ of $E$, if $s_{1}$ is an element of $\mathrm{faces}$, then $\mathrm{AffineIndependent}$ holds for $x$ and the function that maps $x_{5}$ to $\MembershipmemMACRoT {s_{1}}{x_{5}}$, $\mathrm{faces}$ is a lower set and for all finite sets $s$ of $E$, if $s$ is an element of $\mathrm{faces}$, then for all finite sets $t$ of $E$, if $t$ is an element of $\mathrm{faces}$, then $\operatorname{inter} (\operatorname{convexHull} (x , s), \operatorname{convexHull} (x , t))\leq \operatorname{convexHull} (x , \operatorname{inter} (s , t))$. Then the simplicial complex of $\mathrm{faces}$ is a simplicial complex of $x$ and $E$.

Geometry.SimplicialComplex.ofSubcomplexdefMathlib.Analysis.Convex.SimplicialComplex.Basic, function or constant

Wording

the simplicial complex of K and faces (from the name)

English

Let $K$ be a simplicial complex of $x$ and $E$. Let $\mathrm{faces}$ be an element of the power set of the set of finite sets of $E$ such that $\mathrm{faces}$ is less than or equal to the face of $\operatorname{toPreAbstractSimplicialComplex}$ applied to $K$ and $\mathrm{faces}$ is a lower set. Then the simplicial complex of $K$ and $\mathrm{faces}$ is a simplicial complex of $x$ and $E$.

Geometry.SimplicialComplex.spacedefMathlib.Analysis.Convex.SimplicialComplex.Basic, function or constant

Wording

the underlying space of K (from the docstring)

English

Let $K$ be a simplicial complex of $x$ and $E$. Then the underlying space of $K$ is an element of $\wp E$ defined as the union of the function that maps $s$ to the union of the function that maps $h$ to $\operatorname{convexHull}$ applied to $x$ and $s$.

Geometry.SimplicialComplex.verticesdefMathlib.Analysis.Convex.SimplicialComplex.Basic, function or constant

Wording

the vertice of K (from the name)

English

Let $K$ be a simplicial complex of $x$ and $E$. Then the vertice of $K$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{5}$ to the proposition that $\operatorname{singleton}$ applied to $x_{5}$ is an element of the face of $\operatorname{toPreAbstractSimplicialComplex}$ applied to $K$.

Mathlib.Analysis.Convex.Star

StarConvexdefMathlib.Analysis.Convex.Star, predicate

Wording

no wording

English

Let $x$ be a set. Let $x_{5}$ be an element of $E$. Let $s$ be an element of $\wp E$. Then $\mathrm{StarConvex}$ holds for $x$, $x_{5}$ and $s$, if for all elements $y$ of $E$, if $y$ is an element of $s$, then for all elements $a$ and $b$ of $x$, if $0 \leq a$, then if $0 \leq b$, then if $\EqtMACRoH {a + b}{1}$, then $\HSMulhSMulMACRoAL {a}{x_{5}}+ \HSMulhSMulMACRoAL {b}{y}$ is an element of $s$.

Mathlib.Analysis.Convex.Strict

StrictConvexdefMathlib.Analysis.Convex.Strict, predicate

Wording

x is strictly convex (from the docstring)

English

generation took over the time limit

Mathlib.Analysis.Convex.StrictConvexBetween

Isometry.affineIsometryOfStrictConvexSpacedefMathlib.Analysis.Convex.StrictConvexBetween, function or constant

Wording

the affine isometry of hi (from the name)

English

Assume that $f$ is an isometry. Then the affine isometry of $\mathrm{hi}$ is an affine isometry of $\mathrm{PF}$ and $\mathrm{PE}$.

Mathlib.Analysis.Convex.StrictConvexSpace

StrictConvexSpaceclassMathlib.Analysis.Convex.StrictConvexSpace, predicate

Wording

no wording

English

Let $x$ and $E$ be sets. Then we can say that $\mathrm{StrictConvexSpace}$ holds for $x$ and $E$.

Mathlib.Analysis.Convex.Strong

StrongConcaveOndefMathlib.Analysis.Convex.Strong, predicate

Wording

no wording

English

Let $s$ be an element of $\wp E$. Let $m$ be a real number. Let $x_{2}$ be a function from elements of $E$ to real numbers. Then $\mathrm{StrongConcaveOn}$ holds for $s$, $m$ and $x_{2}$, if $\mathrm{UniformConcaveOn}$ holds for $s$, the function that maps $r$ to $\frac{ m}{2}\times r ^ {2}$ and $x_{2}$.

StrongConvexOndefMathlib.Analysis.Convex.Strong, predicate

Wording

no wording

English

Let $s$ be an element of $\wp E$. Let $m$ be a real number. Let $x_{2}$ be a function from elements of $E$ to real numbers. Then $\mathrm{StrongConvexOn}$ holds for $s$, $m$ and $x_{2}$, if $\mathrm{UniformConvexOn}$ holds for $s$, the function that maps $r$ to $\frac{ m}{2}\times r ^ {2}$ and $x_{2}$.

UniformConcaveOndefMathlib.Analysis.Convex.Strong, predicate

Wording

no wording

English

Let $s$ be an element of $\wp E$. Let $x_{2}$ be a function from real numbers to real numbers. Let $f$ be a function from elements of $E$ to real numbers. Then $\mathrm{UniformConcaveOn}$ holds for $s$, $x_{2}$ and $f$, if $s$ is convex and for all elements $x_{3}$ of $E$, if $x_{3}$ is an element of $s$, then for all elements $y$ of $E$, if $y$ is an element of $s$, then for all elements $a$ of $\Real$, for all real numbers $b$, if $0 \leq a$, then if $0 \leq b$, then if $a + b = 1$, then the sum of $\HSMulhSMulMACRoAL {a}{f (x_{3})}+ \HSMulhSMulMACRoAL {b}{f (y)}$ and the product of $a \times b$ and $x_{2}$ applied to the norm of $x_{3} - y$ is less than or equal to $f$ applied to $\HSMulhSMulMACRoAL {a}{x_{3}}+ \HSMulhSMulMACRoAL {b}{y}$.

UniformConvexOndefMathlib.Analysis.Convex.Strong, predicate

Wording

no wording

English

Let $s$ be an element of $\wp E$. Let $x_{2}$ be a function from real numbers to real numbers. Let $f$ be a function from elements of $E$ to real numbers. Then $\mathrm{UniformConvexOn}$ holds for $s$, $x_{2}$ and $f$, if $s$ is convex and for all elements $x_{3}$ of $E$, if $x_{3}$ is an element of $s$, then for all elements $y$ of $E$, if $y$ is an element of $s$, then for all elements $a$ of $\Real$, for all real numbers $b$, if $0 \leq a$, then if $0 \leq b$, then if $a + b = 1$, then $f$ applied to $\HSMulhSMulMACRoAL {a}{x_{3}}+ \HSMulhSMulMACRoAL {b}{y}$ is less than or equal to the difference between $\HSMulhSMulMACRoAL {a}{f (x_{3})}+ \HSMulhSMulMACRoAL {b}{f (y)}$ and the product of $a \times b$ and $x_{2}$ applied to the norm of $x_{3} - y$.

Mathlib.Analysis.Convex.Topology

closedConvexHulldefMathlib.Analysis.Convex.Topology, function or constant

Wording

the convex closed hull of x (from the docstring)

English

Let $x$ be a set. Then the convex closed hull of $x$ is a closure operator of $\wp E$ defined as the closure operator of the function that maps $s$ to the proposition that $s$ is convex and closed and the function that maps $x_{6}$ to $\mathrm{convex\_closed\_sInter}$.

Mathlib.Analysis.Convex.Uniform

UniformConvexSpaceclassMathlib.Analysis.Convex.Uniform, predicate

Wording

E is a uniform convex space (from the name)

English

Let $E$ be a set. Then we can say that $E$ is a uniform convex space.

Mathlib.Analysis.Convex.Visible

IsVisibledefMathlib.Analysis.Convex.Visible, predicate

Wording

no wording

English

Let $x$ be a set. Let $s$ be an element of $\wp P$. Let $x_{6}$ and $y$ be elements of $P$. Then $\mathrm{IsVisible}$ holds for $x$, $s$, $x_{6}$ and $y$, if for all elements $z$ of $P$, if $z$ is an element of $s$, then it is not the case that $\mathrm{Sbtw}$ holds for $x$, $x_{6}$, $z$ and $y$.

Mathlib.Analysis.Convolution

MeasureTheory.ConvolutionExistsdefMathlib.Analysis.Convolution, predicate

Wording

no wording

English

Let $f$ be a function from elements of $G$ to elements of $E$. Let $g$ be a function from elements of $G$ to elements of $\mathrm{E'}$. Let $L$ be a continuous linear map of $E$ and the set of continuous linear maps of $\mathrm{E'}$ and $F$. Let $x_{10}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $G$ and $\mathrm{MeasureTheory\_\_ConvolutionExists\_\_\_auto\_1}$. Then $\operatorname{ConvolutionExists}$ holds for $f$, $g$, $L$ and $x_{10}$, if for all elements $x_{11}$ of $G$, $\operatorname{ConvolutionExistsAt}$ holds for $f$, $g$, $x_{11}$, $L$ and $x_{10}$.

MeasureTheory.ConvolutionExistsAtdefMathlib.Analysis.Convolution, predicate

Wording

no wording

English

Let $f$ be a function from elements of $G$ to elements of $E$. Let $g$ be a function from elements of $G$ to elements of $\mathrm{E'}$. Let $x_{10}$ be an element of $G$. Let $L$ be a continuous linear map of $E$ and the set of continuous linear maps of $\mathrm{E'}$ and $F$. Let $x_{11}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $G$ and $\mathrm{MeasureTheory\_\_ConvolutionExistsAt\_\_\_auto\_1}$. Then $\operatorname{ConvolutionExistsAt}$ holds for $f$, $g$, $x_{10}$, $L$ and $x_{11}$, if $\operatorname{Integrable}$ holds for the function that maps $t$ to $\operatorname{coe}$ applied to $L$, $f$ applied to $t$ and $g$ applied to $x_{10} - t$ and $x_{11}$.

MeasureTheory.convolutiondefMathlib.Analysis.Convolution, function or constant

Wording

the convolution of x11 and x12 (from the name)

English

Let $f$ be a function from elements of $G$ to elements of $E$. Let $g$ be a function from elements of $G$ to elements of $\mathrm{E'}$. Let $L$ be a continuous linear map of $E$ and the set of continuous linear maps of $\mathrm{E'}$ and $F$. Let $x_{11}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $G$ and $\mathrm{MeasureTheory\_\_convolution\_\_\_auto\_1}$. Let $x_{12}$ be an element of $G$. Then the convolution of $x_{11}$ and $x_{12}$ is an element of $F$ defined as the Bochner integral of $x_{11}$ and the function that maps $t$ to $\operatorname{coe}$ applied to $L$, $f$ applied to $t$ and $g$ applied to $x_{12} - t$.

MeasureTheory.posConvolutiondefMathlib.Analysis.Convolution, function or constant

Wording

the positive part convolution of x6 and x7 (from the name)

English

Let $f$ be a function from real numbers to elements of $E$. Let $g$ be a function from real numbers to elements of $\mathrm{E'}$. Let $L$ be a continuous linear map of $E$ and the set of continuous linear maps of $\mathrm{E'}$ and $F$. Let $x_{6}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $\Real$ and $\mathrm{MeasureTheory\_\_posConvolution\_\_\_auto\_1}$. Let $x_{7}$ be a real number. Then the positive part convolution of $x_{6}$ and $x_{7}$ is an element of $F$ defined as the indicator of the function that maps $x_{7}$ to the interval integral of $x_{7}$ and $x_{6}$ and $x_{7}$.

Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

ContDiffMapSupportedInstructureMathlib.Analysis.Distribution.ContDiffMapSupportedIn, type

Wording

no wording

English

Let $E$ and $F$ be sets. Let $n$ be a natural number. Let $K$ be a compact of $E$. Then the elements of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ are a basic type.

ContDiffMapSupportedIn.bilinLeftCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the map of B and hg (from the docstring)

English

Let $B$ be a continuous linear map of $x_{4}$ and the set of continuous linear maps of $x_{5}$ and $x_{6}$. Assume that $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to $n$ and $g$. Then the map of $B$ and $\mathrm{hg}$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $x_{4}$, $n$ and $K$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $x_{6}$, $n$ and $K$.

ContDiffMapSupportedIn.copydefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be an element of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$. Let $\mathrm{f'}$ be a function from elements of $E$ to elements of $F$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an element of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$.

ContDiffMapSupportedIn.fderivCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the derivative continuous linear map of n and k (from the name)

English

Let $x$ be a set. Let $n$ and $k$ be natural numbers. Then the derivative continuous linear map of $n$ and $k$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, the set of continuous linear maps of $E$ and $F$, $k$ and $K$.

ContDiffMapSupportedIn.fderivLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $x$ be a set. Let $n$ and $k$ be natural numbers. Then $\operatorname{fderivLM}$ applied to $x$, $n$ and $k$ is a linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, the set of continuous linear maps of $E$ and $F$, $k$ and $K$.

ContDiffMapSupportedIn.integralAgainstBilinCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $B$ be a continuous linear map of $x_{4}$ and the set of continuous linear maps of $x_{5}$ and $x_{6}$. Let $x_{15}$ be a measure of $E$. Let $x_{16}$ be a function from elements of $E$ to elements of $x_{5}$. Then $\operatorname{integralAgainstBilinCLM}$ applied to $B$, $x_{15}$ and $x_{16}$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $x_{4}$, $n$ and $K$ and $x_{6}$.

ContDiffMapSupportedIn.integralAgainstBilinLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $B$ be a continuous linear map of $x_{4}$ and the set of continuous linear maps of $x_{5}$ and $x_{6}$. Let $x_{15}$ be a measure of $E$. Let $x_{16}$ be a function from elements of $E$ to elements of $x_{5}$. Then $\operatorname{integralAgainstBilinLM}$ applied to $B$, $x_{15}$ and $x_{16}$ is a linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $x_{4}$, $n$ and $K$ and $x_{6}$.

ContDiffMapSupportedIn.iteratedFDerivLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $x$ be a set. Let $n$ and $k$ be natural numbers. Let $i$ be a natural number. Then $\operatorname{iteratedFDerivLM}$ applied to $x$, $n$, $k$ and $i$ is a linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, the set of continuous multilinear maps of the function that maps $x_{7}$ to $E$ and $F$, $k$ and $K$.

ContDiffMapSupportedIn.mkCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the continuous linear map of A (from the name)

English

Let $x$ be a set. Let $A$ be a function from elements of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$ and elements of $E$ to elements of $\mathrm{F'}$ such that for all elements $f_{4}$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$, for all elements $g$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$, for all elements $x_{16}$ of $E$, $\EqtMACRoH {A (f_{4} + g , x_{16})}{A (f_{4} , x_{16})+ A (g , x_{16})}$, for all elements $c$ of $x$, for all elements $f_{3}$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$, for all elements $x_{15}$ of $E$, $\EqtMACRoH {A (\HSMulhSMulMACRoAL {c}{f_{3}}, x_{15})}{\HSMulhSMulMACRoAL {c}{A (f_{3} , x_{15})}}$, for all elements $f_{2}$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$, $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to $x_{11}$ and $A$ applied to $f_{2}$, for all elements $f_{1}$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$, $\operatorname{EqOn}$ holds for $A$ applied to $f_{1}$, $0$ and the complement of $x_{13}$ and for all elements $i$ of $\Natural$, if $i \leq x_{11}$, then there exists a finite set $s$ of $\Natural$ such that there exists a real number $C$ such that $0 \leq C$ and for all elements $f$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$, for all elements $x_{14}$ of $E$, if $\MembershipmemMACRoT {x_{13}}{x_{14}}$, then the norm of the iterated derivative of $A$ applied to $f$ and $x_{14}$ is less than or equal to the product of $C$ and $\operatorname{sup}$ applied to $s$, the function that maps $j_{1}$ to the seminorm of $x_{12}$ and $j_{1}$ and $f$. Then the continuous linear map of $A$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{10}$ and $x_{12}$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $\mathrm{F'}$, $x_{11}$ and $x_{13}$.

ContDiffMapSupportedIn.mkCLMtoNormedSpacedefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $x$ be a set. Let $A$ be a function from elements of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ to elements of $G$ such that for all elements $f_{2}$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$, for all elements $g$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$, $\EqtMACRoH {A (f_{2} + g)}{A (f_{2})+ A (g)}$, for all elements $c$ of $x$, for all elements $f_{1}$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$, $\EqtMACRoH {A (\HSMulhSMulMACRoAL {c}{f_{1}})}{\HSMulhSMulMACRoAL {c}{A (f_{1})}}$ and there exists a finite set $s$ of $\Natural$ such that there exists a real number $C$ such that $0 \leq C$ and for all elements $f$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$, the norm of $A$ applied to $f$ is less than or equal to the product of $C$ and $\operatorname{sup}$ applied to $s$, the function that maps $i_{1}$ to the seminorm of $K$ and $i_{1}$ and $f$. Then $\operatorname{mkCLMtoNormedSpace}$ applied to $x$, $A$, $\mathrm{hadd}$, $\mathrm{hsmul}$ and $\mathrm{hbound}$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and $G$.

ContDiffMapSupportedIn.monoCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the monotone continuous linear map of x (from the name)

English

Let $x$ be a set. Then the monotone continuous linear map of $x$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{7}$ and $x_{9}$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{8}$ and $x_{10}$.

ContDiffMapSupportedIn.monoLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{monoLM}$ applied to $x$ is a linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{7}$ and $x_{9}$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $x_{8}$ and $x_{10}$.

ContDiffMapSupportedIn.of_support_subsetdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the support subset of hf and hsupp (from the name)

English

Assume that $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to $n$ and $f$. Assume that the support of $f$ is less than or equal to $K$. Then the support subset of $\mathrm{hf}$ and $\mathrm{hsupp}$ is an element of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$.

ContDiffMapSupportedIn.postcompCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the postcomposition continuous linear map of T (from the name)

English

Let $T$ be a continuous linear map of $F$ and $\mathrm{F'}$. Then the postcomposition continuous linear map of $T$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $\mathrm{F'}$, $n$ and $K$.

ContDiffMapSupportedIn.postcompLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $T$ be a continuous linear map of $F$ and $\mathrm{F'}$. Then $\operatorname{postcompLM}$ applied to $T$ is a linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $\mathrm{F'}$, $n$ and $K$.

ContDiffMapSupportedIn.seminormdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the seminorm of K and i (from the name)

English

Let $x$, $E$ and $F$ be sets. Let $n$ be a natural number. Let $K$ be a compact of $E$. Let $i$ be a natural number. Then the seminorm of $K$ and $i$ is a seminorm of $x$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ defined as the composition of the norm of $x$ and the set of bounded continuous functions of $E$ and the set of continuous multilinear maps of the function that maps $x_{7}$ to $E$ and $F$ and $\operatorname{structureMapLM}$ applied to $x$, $n$ and $i$.

ContDiffMapSupportedIn.structureMapCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the structure map continuous linear map of n and i (from the name)

English

Let $x$ be a set. Let $n$ be a natural number. Let $i$ be a natural number. Then the structure map continuous linear map of $n$ and $i$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and the set of bounded continuous functions of $E$ and the set of continuous multilinear maps of the function that maps $x_{7}$ to $E$ and $F$.

ContDiffMapSupportedIn.structureMapLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $x$ be a set. Let $n$ be a natural number. Let $i$ be a natural number. Then $\operatorname{structureMapLM}$ applied to $x$, $n$ and $i$ is a linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and the set of bounded continuous functions of $E$ and the set of continuous multilinear maps of the function that maps $x_{7}$ to $E$ and $F$ defined as the composition of $\operatorname{toBoundedContinuousFunctionLM}$ applied to $x$ and $\operatorname{iteratedFDerivLM}$ applied to $x$, $n$, $0$ and $i$.

ContDiffMapSupportedIn.supSeminormdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the supremum seminorm of K and i (from the name)

English

Let $x$, $E$ and $F$ be sets. Let $n$ be a natural number. Let $K$ be a compact of $E$. Let $i$ be a natural number. Then the supremum seminorm of $K$ and $i$ is a seminorm of $x$ and $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ defined as the supremum of $\FinsetIicMACRoAJ {i}$ and $\operatorname{seminorm}$ applied to $K$.

ContDiffMapSupportedIn.toBoundedContinuousFunctionCLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

the bounded continuous function continuous linear map of x (from the name)

English

Let $x$ be a set. Then the bounded continuous function continuous linear map of $x$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and the set of bounded continuous functions of $E$ and $F$.

ContDiffMapSupportedIn.toBoundedContinuousFunctionLMdefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{toBoundedContinuousFunctionLM}$ applied to $x$ is a linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and the set of bounded continuous functions of $E$ and $F$.

ContDiffMapSupportedIn.toFundefMathlib.Analysis.Distribution.ContDiffMapSupportedIn, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$. Let $x_{4}$ be an element of $E$. Then $\operatorname{toFun}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

ContDiffMapSupportedInClassclassMathlib.Analysis.Distribution.ContDiffMapSupportedIn, predicate

Wording

no wording

English

Let $B$ be a set. Let $E$ and $F$ be elements of $\mathrm{outParam}$ applied to the set of sets. Let $n$ be an element of $\mathrm{outParam}$ applied to the set of natural numbers. Let $K$ be an element of $\mathrm{outParam}$ applied to the set of compacts of $E$. Then we can say that $\mathrm{ContDiffMapSupportedInClass}$ holds for $B$, $E$, $F$, $n$ and $K$.

Mathlib.Analysis.Distribution.DerivNotation

ContinuousLineDerivclassMathlib.Analysis.Distribution.DerivNotation, predicate

Wording

F is a continuous line derivative (from the name)

English

Let $V$ and $E$ be sets. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a continuous line derivative.

LaplacianclassMathlib.Analysis.Distribution.DerivNotation, predicate

Wording

F is a Laplacian (from the name)

English

Let $E$ be a set. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a Laplacian.

Laplacian.laplaciandefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

the Laplacian of x (from the docstring)

English

Let $x$ be an element of $E$. Then the Laplacian of $x$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

LineDerivclassMathlib.Analysis.Distribution.DerivNotation, predicate

Wording

F is a line derivative (from the name)

English

Let $V$ and $E$ be sets. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a line derivative.

LineDeriv.bilinearLineDerivTwodefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be an element of $x$. Then $\operatorname{bilinearLineDerivTwo}$ applied to $R$ and $f$ is a linear map of $E$ and the set of linear maps of $E$ and $x_{2}$.

LineDeriv.iteratedLineDerivOpdefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

the iterated line derivative opposite of x1 and x2 (from the name)

English

Let $x_{1}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $V$. Let $x_{2}$ be an element of $E$. Then the iterated line derivative opposite of $x_{1}$ and $x_{2}$ is an element of $E$ defined as $\operatorname{recOn}$ applied to $n$, the function that maps $x_{1}$ to $\mathrm{id}$, the function that maps $x_{2}$, $\mathrm{rec}$ and $y$ to $\operatorname{comp}$ applied to $\operatorname{lineDerivOp}$ applied to $y$ applied to $0$ and $\mathrm{rec}$ applied to $\operatorname{tail}$ applied to $y$, $x_{1}$ and $x_{2}$.

LineDeriv.iteratedLineDerivOpCLMdefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

the iterated line derivative opposite continuous linear map of m (from the name)

English

Let $R$ and $E$ be sets. Let $m$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $V$. Then the iterated line derivative opposite continuous linear map of $m$ is a continuous linear map of $E$ and $E$.

LineDeriv.laplacianCLMdefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

the Laplacian continuous linear map of E and x (from the name)

English

Let $R$, $E$ and $x$ be sets. Then the Laplacian continuous linear map of $E$ and $x$ is a continuous linear map of $x$ and $x_{2}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{comp} (\operatorname{lineDerivOpCLM} (\operatorname{stdOrthonormalBasis} (\Real , E , i)), \operatorname{lineDerivOpCLM} (\operatorname{stdOrthonormalBasis} (\Real , E , i)))}$.

LineDeriv.lineDerivOpdefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

the line derivative opposite of x and x1 (from the name)

English

Let $x$ be an element of $V$. Let $x_{1}$ be an element of $E$. Then the line derivative opposite of $x$ and $x_{1}$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

LineDeriv.lineDerivOpCLMdefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

the line derivative opposite continuous linear map of m (from the name)

English

Let $R$ and $E$ be sets. Let $m$ be an element of $V$. Then the line derivative opposite continuous linear map of $m$ is a continuous linear map of $E$ and $F$.

LineDeriv.tensorLineDerivTwodefMathlib.Analysis.Distribution.DerivNotation, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be an element of $x$. Then $\operatorname{tensorLineDerivTwo}$ applied to $R$ and $f$ is a linear map of the set of tensor products of $E$ and $E$ and $x_{2}$ defined as the lift of $\operatorname{bilinearLineDerivTwo}$ applied to $R$ and $f$.

LineDerivAddclassMathlib.Analysis.Distribution.DerivNotation, predicate

Wording

F is a line derivative sum (from the name)

English

Let $V$ and $E$ be sets. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a line derivative sum.

LineDerivLeftSMulclassMathlib.Analysis.Distribution.DerivNotation, predicate

Wording

F is a line derivative left product (from the name)

English

Let $R$, $V$ and $E$ be sets. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a line derivative left product.

LineDerivSMulclassMathlib.Analysis.Distribution.DerivNotation, predicate

Wording

F is a line derivative product (from the name)

English

Let $R$, $V$ and $E$ be sets. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a line derivative product.

Mathlib.Analysis.Distribution.Distribution

DistributiondefMathlib.Analysis.Distribution.Distribution, type

Wording

distribution of F and n (from the name)

English

Let $x_{2}$ be an open of $E$. Let $F$ be a set. Let $n$ be a natural number. Then a distribution of $F$ and $n$ is an element of the function that maps $x_{2}$, $F$ and $n$ to the set of compact convergence continuous linear maps of the set of test functions of $\Real$ and $n$ and $F$.

Distribution.deltadefMathlib.Analysis.Distribution.Distribution, function or constant

Wording

the Dirac delta distribution of x3 (from the docstring)

English

Let $x_{3}$ be an element of $E$. Then the Dirac delta distribution of $x_{3}$ is a distribution of $\Real$ and $n$.

Distribution.lineDerivCLMdefMathlib.Analysis.Distribution.Distribution, function or constant

Wording

the line derivative continuous linear map of v (from the name)

English

Let $v$ be an element of $E$. Then the line derivative continuous linear map of $v$ is a continuous linear map of the set of distributions of $F$ and $k$ and the set of distributions of $F$ and $n$ defined as $\operatorname{neg}$ applied to the precomposition compact convergence continuous linear map of $F$ and the line derivative continuous linear map of $\Real$ and $v$.

Distribution.mapCLMdefMathlib.Analysis.Distribution.Distribution, function or constant

Wording

the map continuous linear map of A (from the name)

English

Let $A$ be a continuous linear map of $F$ and $\mathrm{F'}$. Then the map continuous linear map of $A$ is a continuous linear map of the set of distributions of $F$ and $n$ and the set of distributions of $\mathrm{F'}$ and $n$ defined as the postcomposition compact convergence continuous linear map of the set of test functions of $\Real$ and $n$ and $A$.

Distribution.ofFundefMathlib.Analysis.Distribution.Distribution, function or constant

Wording

the distribution of x6 and n (from the name)

English

Let $x_{2}$ be an open of $E$. Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{6}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{Distribution\_\_ofFun\_\_\_auto\_1}$. Let $n$ be a natural number. Then the distribution of $x_{6}$ and $n$ is a distribution of $F$ and $n$ defined as $\operatorname{integralAgainstBilinCLM}$ applied to $\operatorname{lsmul}$ applied to $\Real$ and $\Real$, $x_{6}$ and $f$.

Mathlib.Analysis.Distribution.FourierMultiplier

SchwartzMap.fourierMultiplierCLMdefMathlib.Analysis.Distribution.FourierMultiplier, function or constant

Wording

the Fourier multiplier continuous linear map of F and g (from the name)

English

Let $F$ be a set. Let $g$ be a function from elements of $E$ to elements of $x$. Then the Fourier multiplier continuous linear map of $F$ and $g$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $E$ and $F$ defined as the composition of the inverse Fourier transform of $x$ and the set of Schwartz maps of $E$ and $F$ and the composition of the map of $F$ and $g$ and the Fourier transform of $x$ and the set of Schwartz maps of $E$ and $F$.

TemperedDistribution.fourierMultiplierCLMdefMathlib.Analysis.Distribution.FourierMultiplier, function or constant

Wording

the Fourier multiplier continuous linear map of F and g (from the name)

English

Let $F$ be a set. Let $g$ be a function from elements of $E$ to complexes. Then the Fourier multiplier continuous linear map of $F$ and $g$ is a continuous linear map of the set of tempered distributions of $E$ and $F$ and the set of tempered distributions of $E$ and $F$ defined as the composition of the inverse Fourier transform of the set of complexes and the set of tempered distributions of $E$ and $F$ and the composition of the scalar multiple left continuous linear map of $F$ and $g$ and the Fourier transform of the set of complexes and the set of tempered distributions of $E$ and $F$.

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

HasCompactSupport.toSchwartzMapdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the Schwartz map of h and h1 (from the name)

English

Assume that $f$ has compact supports. Assume that $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to the top and $f$. Then the Schwartz map of $h$ and $h_{1}$ is a Schwartz map of $E$ and $F$.

SchwartzMapstructureMathlib.Analysis.Distribution.SchwartzSpace.Basic, type

Wording

Schwartz map of E and F (from the name)

English

Let $E$ and $F$ be sets. Then the Schwartz maps of $E$ and $F$ are a basic type.

SchwartzMap.bilinLeftCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the map of B and hg (from the docstring)

English

Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Assume that $g$ has temperate growths. Then the map of $B$ and $\mathrm{hg}$ is a continuous linear map of the set of Schwartz maps of $D$ and $E$ and the set of Schwartz maps of $D$ and $G$.

SchwartzMap.compCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the composition continuous linear map of hg and hg_upper (from the name)

English

Let $x$ be a set. Assume that $g$ has temperate growths. Assume that there exists a natural number $k$, such that there exists a real number $C$, such that for all elements $x_{9}$ of $D$, the norm of $x_{9}$ is less than or equal to the product of $C$ and the exponentiation of the sum of $1$ and the norm of $g$ applied to $x_{9}$ to $k$. Then the composition continuous linear map of $\mathrm{hg}$ and $\mathrm{hg\_upper}$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $D$ and $F$.

SchwartzMap.compCLMOfAntilipschitzdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the composition continuous linear map of hg and #3 (from the name)

English

Let $x$ be a set. Assume that $g$ has temperate growths. Assume that $\mathrm{AntilipschitzWith}$ holds for $K$ and $g$. Then the composition continuous linear map of $\mathrm{hg}$ and $\mathrm{h'g}$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $D$ and $F$.

SchwartzMap.compCLMOfContinuousLinearEquivdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the composition continuous linear map of x and g (from the name)

English

Let $x$ be a set. Let $g$ be a continuous linear equivalence of $D$ and $E$. Then the composition continuous linear map of $x$ and $g$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $D$ and $F$.

SchwartzMap.compSubConstCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the composition difference constant continuous linear map of x and a (from the name)

English

Let $x$ be a set. Let $a$ be an element of $E$. Then the composition difference constant continuous linear map of $x$ and $a$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $E$ and $F$.

SchwartzMap.evalCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the evaluation continuous linear map of m (from the name)

English

Let $x$, $E$ and $G$ be sets. Let $m$ be an element of $F$. Then the evaluation continuous linear map of $m$ is a continuous linear map of the set of Schwartz maps of $E$ and the set of continuous linear maps of $F$ and $G$ and the set of Schwartz maps of $E$ and $G$.

SchwartzMap.integralCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the integral of x and x8 (from the docstring)

English

Let $x$ be a set. Let $x_{8}$ be a measure of $D$. Then the integral of $x$ and $x_{8}$ is a continuous linear map of the set of Schwartz maps of $D$ and $V$ and $V$.

SchwartzMap.mkCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the continuous linear map of A (from the name)

English

Let $A$ be a function from Schwartz maps of $D$ and $E$ and elements of $F$ to elements of $G$ such that for all Schwartz maps $f_{3}$ of $D$ and $E$, for all Schwartz maps $g$ of $D$ and $E$, for all elements $x_{17}$ of $F$, $\EqtMACRoH {A (f_{3} + g , x_{17})}{A (f_{3} , x_{17})+ A (g , x_{17})}$, for all elements $a$ of $x$, for all Schwartz maps $f_{2}$ of $D$ and $E$, for all elements $x_{16}$ of $F$, $\EqtMACRoH {A (\HSMulhSMulMACRoAL {a}{f_{2}}, x_{16})}{\HSMulhSMulMACRoAL {x_{14} (a)}{A (f_{2} , x_{16})}}$, for all Schwartz maps $f_{1}$ of $D$ and $E$, $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to the top and $A$ applied to $f_{1}$ and for all elements $n$ of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$, there exists a finite set $s$ of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ such that there exists an element $C$ of $\Real$ such that $0 \leq C$ and for all Schwartz maps $f$ of $D$ and $E$, for all elements $x_{15}$ of $F$, the product of the exponentiation of the norm of $x_{15}$ to $\ProdfstMACRoZ {n}$ and the norm of the iterated derivative of $A$ applied to $f$ and $x_{15}$ is less than or equal to the product of $C$ and $\operatorname{sup}$ applied to $s$, the Schwartz seminorm family of $D$ and $E$ and $f$. Then the continuous linear map of $A$ is a continuous linear map of the set of Schwartz maps of $D$ and $E$ and the set of Schwartz maps of $F$ and $G$.

SchwartzMap.mkCLMtoNormedSpacedefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

no wording

English

Let $A$ be a function from Schwartz maps of $D$ and $E$ to elements of $G$ such that for all Schwartz maps $f_{2}$ of $D$ and $E$, for all Schwartz maps $g$ of $D$ and $E$, $\EqtMACRoH {A (f_{2} + g)}{A (f_{2})+ A (g)}$, for all elements $a$ of $x$, for all Schwartz maps $f_{1}$ of $D$ and $E$, $\EqtMACRoH {A (\HSMulhSMulMACRoAL {a}{f_{1}})}{\HSMulhSMulMACRoAL {x_{11} (a)}{A (f_{1})}}$ and there exists a finite set $s$ of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ such that there exists a real number $C$ such that $0 \leq C$ and for all Schwartz maps $f$ of $D$ and $E$, the norm of $A$ applied to $f$ is less than or equal to the product of $C$ and $\operatorname{sup}$ applied to $s$, the Schwartz seminorm family of $D$ and $E$ and $f$. Then $\operatorname{mkCLMtoNormedSpace}$ applied to $A$, $\mathrm{hadd}$, $\mathrm{hsmul}$ and $\mathrm{hbound}$ is a continuous linear map of the set of Schwartz maps of $D$ and $E$ and $G$.

SchwartzMap.mkLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

no wording

English

Let $A$ be a function from Schwartz maps of $D$ and $E$ and elements of $F$ to elements of $G$ such that for all Schwartz maps $f_{3}$ of $D$ and $E$, for all Schwartz maps $g$ of $D$ and $E$, for all elements $x_{17}$ of $F$, $\EqtMACRoH {A (f_{3} + g , x_{17})}{A (f_{3} , x_{17})+ A (g , x_{17})}$, for all elements $a$ of $x$, for all Schwartz maps $f_{2}$ of $D$ and $E$, for all elements $x_{16}$ of $F$, $\EqtMACRoH {A (\HSMulhSMulMACRoAL {a}{f_{2}}, x_{16})}{\HSMulhSMulMACRoAL {x_{14} (a)}{A (f_{2} , x_{16})}}$, for all Schwartz maps $f_{1}$ of $D$ and $E$, $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to the top and $A$ applied to $f_{1}$ and for all elements $n$ of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$, there exists a finite set $s$ of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ such that there exists an element $C$ of $\Real$ such that $0 \leq C$ and for all Schwartz maps $f$ of $D$ and $E$, for all elements $x_{15}$ of $F$, the product of the exponentiation of the norm of $x_{15}$ to $\ProdfstMACRoZ {n}$ and the norm of the iterated derivative of $A$ applied to $f$ and $x_{15}$ is less than or equal to the product of $C$ and $\operatorname{sup}$ applied to $s$, the Schwartz seminorm family of $D$ and $E$ and $f$. Then $\operatorname{mkLM}$ applied to $A$, $\mathrm{hadd}$, $\mathrm{hsmul}$, $\mathrm{hsmooth}$ and $\mathrm{hbound}$ is a linear map of the set of Schwartz maps of $D$ and $E$ and the set of Schwartz maps of $F$ and $G$.

SchwartzMap.pairingdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the pairing of B (from the name)

English

Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then the pairing of $B$ is a linear map of the set of Schwartz maps of $D$ and $E$ and the set of continuous linear maps of the set of Schwartz maps of $D$ and $F$ and the set of Schwartz maps of $D$ and $G$.

SchwartzMap.postcompCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the postcomposition continuous linear map of L (from the name)

English

Let $L$ be a continuous linear map of $F$ and $G$. Then the postcomposition continuous linear map of $L$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $E$ and $G$.

SchwartzMap.seminormdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the seminorm of k and n (from the name)

English

Let $x$ be a set. Let $k$ and $n$ be natural numbers. Then the seminorm of $k$ and $n$ is a seminorm of $x$ and the set of Schwartz maps of $E$ and $F$.

SchwartzMap.smulLeftCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the map of F and g (from the docstring)

English

Let $F$ be a set. Let $g$ be a function from elements of $E$ to elements of $x$. Then the map of $F$ and $g$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $E$ and $F$ defined as $\mathrm{dite}$ applied to the proposition that $g$ has temperate growths, the function that maps $\mathrm{hg}$ to the map of the flip of $\operatorname{lsmul}$ applied to $x$ and $x$ and $\mathrm{hg}$ and the function that maps $\mathrm{hg1}$ to $0$.

SchwartzMap.smulRightCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the scalar multiple right continuous linear map of L (from the name)

English

Let $x$ and $F$ be sets. Let $L$ be a continuous linear map of $E$ and the set of continuous linear maps of $G$ and $\Real$. Then the scalar multiple right continuous linear map of $L$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $E$ and the set of continuous linear maps of $G$ and $F$.

SchwartzMap.toBoundedContinuousFunctiondefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the bounded continuous function of f (from the name)

English

Let $f$ be a Schwartz map of $E$ and $F$. Then the bounded continuous function of $f$ is a bounded continuous function of $E$ and $F$.

SchwartzMap.toBoundedContinuousFunctionCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the bounded continuous function continuous linear map of E and F (from the name)

English

Let $x$, $E$ and $F$ be sets. Then the bounded continuous function continuous linear map of $E$ and $F$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of bounded continuous functions of $E$ and $F$.

SchwartzMap.toContinuousMapdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the continuous map of f (from the name)

English

Let $f$ be a Schwartz map of $E$ and $F$. Then the continuous map of $f$ is a continuous map of $E$ and $F$ defined as $\operatorname{toContinuousMap}$ applied to the bounded continuous function of $f$.

SchwartzMap.toFundefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the Schwartz map of self and x4 (from the name)

English

Let $\mathrm{self}$ be a Schwartz map of $E$ and $F$. Let $x_{4}$ be an element of $E$. Then the Schwartz map of $\mathrm{self}$ and $x_{4}$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

SchwartzMap.toLpdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

no wording

English

Let $f$ be a Schwartz map of $E$ and $F$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{SchwartzMap\_\_toLp\_\_\_auto\_1}$. Then $\operatorname{toLp}$ applied to $f$, $p$ and $x_{5}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{5})}{x_{6}})}$ defined as $\operatorname{toLp}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{memLp}$ applied to $f$, $p$ and $x_{5}$.

SchwartzMap.toLpCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

no wording

English

Let $x$ and $F$ be sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{8}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{SchwartzMap\_\_toLpCLM\_\_\_auto\_1}$. Then $\operatorname{toLpCLM}$ applied to $x$, $F$, $p$ and $x_{8}$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{8})}{x_{9}})}$.

SchwartzMap.toZeroAtInftydefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the zero at infty of f (from the name)

English

Let $f$ be a Schwartz map of $E$ and $F$. Then the zero at infty of $f$ is a zero at infty continuous map of $E$ and $F$.

SchwartzMap.toZeroAtInftyCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the zero at infty continuous linear map of E and F (from the name)

English

Let $x$, $E$ and $F$ be sets. Then the zero at infty continuous linear map of $E$ and $F$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of zero at infty continuous maps of $E$ and $F$.

schwartzSeminormFamilydefMathlib.Analysis.Distribution.SchwartzSpace.Basic, function or constant

Wording

the Schwartz seminorm family of E and F (from the name)

English

Let $x$, $E$ and $F$ be sets. Then the Schwartz seminorm family of $E$ and $F$ is a seminorm family of the set of Schwartz maps of $E$ and $F$ and $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as the function that maps $m$ to the seminorm of $\ProdfstMACRoZ {m}$ and $\ProdsndMACRoAA {m}$.

Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

SchwartzMap.derivCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Deriv, function or constant

Wording

the derivative continuous linear map of x and F (from the name)

English

Let $x$ and $F$ be sets. Then the derivative continuous linear map of $x$ and $F$ is a continuous linear map of the set of Schwartz maps of $\Real$ and $F$ and the set of Schwartz maps of $\Real$ and $F$.

SchwartzMap.fderivCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Deriv, function or constant

Wording

the derivative continuous linear map of E and F (from the name)

English

Let $x$, $E$ and $F$ be sets. Then the derivative continuous linear map of $E$ and $F$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of Schwartz maps of $E$ and the set of continuous linear maps of $E$ and $F$.

Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

SchwartzMap.fourierTransformCLMdefMathlib.Analysis.Distribution.SchwartzSpace.Fourier, function or constant

Wording

the Fourier transform continuous linear map of x (from the name)

English

Let $x$ be a set. Then the Fourier transform continuous linear map of $x$ is a continuous linear map of the set of Schwartz maps of $V$ and $E$ and the set of Schwartz maps of $V$ and $E$.

Mathlib.Analysis.Distribution.Sobolev

TemperedDistribution.MemSobolevdefMathlib.Analysis.Distribution.Sobolev, predicate

Wording

no wording

English

Let $s$ be an element of $\Real$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be a tempered distribution of $E$ and $F$. Then $\operatorname{MemSobolev}$ holds for $s$, $p$ and $f$, if there exists an element $\mathrm{f'}$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{volume})}{x_{5}})}$, such that $\EqtMACRoH {\operatorname{besselPotential} (E , F , s , f)}{\operatorname{toTemperedDistribution} (\mathrm{f'})}$.

TemperedDistribution.besselPotentialdefMathlib.Analysis.Distribution.Sobolev, function or constant

Wording

no wording

English

Let $E$ and $F$ be sets. Let $s$ be a real number. Then $\operatorname{besselPotential}$ applied to $E$, $F$ and $s$ is a continuous linear map of the set of tempered distributions of $E$ and $F$ and the set of tempered distributions of $E$ and $F$ defined as the Fourier multiplier continuous linear map of $F$ and the function that maps $x_{5}$ to the natural inclusion of the real numbers into the complex numbers of the exponentiation of the sum of $1$ and the exponentiation of the norm of $x_{5}$ to $2$ to $\frac{ s}{2}$.

Mathlib.Analysis.Distribution.Support

Distribution.IsVanishingOndefMathlib.Analysis.Distribution.Support, predicate

Wording

no wording

English

Let $f$ be a function from elements of $F$ to elements of $V$. Let $s$ be an element of $\wp x$. Then $\operatorname{IsVanishingOn}$ holds for $f$ and $s$, if for all elements $u$ of $F$, if $\mathrm{tsupport}$ applied to $\operatorname{coe}$ applied to $u$ is less than or equal to $s$, then $\EqtMACRoH {f (u)}{0}$.

Distribution.dsupportdefMathlib.Analysis.Distribution.Support, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $F$ to elements of $V$. Then $\operatorname{dsupport}$ applied to $f$ is an element of $\wp x$ defined as the intersection of $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $\operatorname{IsVanishingOn}$ holds for $f$ and the complement of $s$ and $s$ is closed.

Mathlib.Analysis.Distribution.TemperateGrowth

Function.HasTemperateGrowthdefMathlib.Analysis.Distribution.TemperateGrowth, predicate

Wording

f has temperate growths (from the name)

English

Let $f$ be a function from elements of $E$ to elements of $F$. Then $f$ has temperate growths, if $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to the top and $f$ and for all natural numbers $n$, there exists a natural number $k$ such that there exists a real number $C$ such that for all elements $x_{4}$ of $E$, the norm of the iterated derivative of $f$ and $x_{4}$ is less than or equal to the product of $C$ and the exponentiation of the sum of $1$ and the norm of $x_{4}$ to $k$.

MeasureTheory.Measure.HasTemperateGrowthclassMathlib.Analysis.Distribution.TemperateGrowth, predicate

Wording

x2 has temperate growths (from the name)

English

Let $x_{2}$ be a measure of $E$. Then we can say that $x_{2}$ has temperate growths.

MeasureTheory.Measure.integrablePowerdefMathlib.Analysis.Distribution.TemperateGrowth, function or constant

Wording

the integrable power of x2 (from the name)

English

Let $x_{2}$ be a measure of $E$. Then the integrable power of $x_{2}$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that $x_{2}$ has temperate growths, the function that maps $h$ to $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_HasTemperateGrowth\_\_exists\_integrable}$ and the function that maps $h_{1}$ to $0$.

Mathlib.Analysis.Distribution.TemperedDistribution

Function.HasTemperateGrowth.toTemperedDistributiondefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the tempered distribution of x5 and hf (from the name)

English

Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{\_private\_\_Mathlib\_\_Analysis\_\_Distribution\_\_TemperedDistribution\_\_0\_\_\_auto\_39}$. Assume that $f$ has temperate growths. Then the tempered distribution of $x_{5}$ and $\mathrm{hf}$ is a tempered distribution of $E$ and $F$ defined as $\operatorname{toPointwiseConvergenceCLM}$ applied to the set of complexes, the identity ring homomorphism of the set of complexes, the set of Schwartz maps of $E$ and the set of complexes, $F$ and the composition of the integral of the set of complexes and $x_{5}$ and the map of $\operatorname{lsmul}$ applied to the set of complexes and the set of complexes and $\mathrm{hf}$.

MeasureTheory.Lp.toTemperedDistributiondefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the tempered distribution of f (from the name)

English

Let $f$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{5})}{x_{6}})}$. Then the tempered distribution of $f$ is a tempered distribution of $E$ and $F$ defined as $\operatorname{toPointwiseConvergenceCLM}$ applied to the set of complexes, the identity ring homomorphism of the set of complexes, the set of Schwartz maps of $E$ and the set of complexes, $F$ and the composition of $\operatorname{lpPairing}$ applied to $x_{5}$, $p$, $\operatorname{inv}$ applied to $1 - \operatorname{inv} (p)$, the flip of $\operatorname{lsmul}$ applied to the set of complexes and the set of complexes and $f$ and $\operatorname{toLpCLM}$ applied to the set of complexes, the set of complexes, $\operatorname{inv}$ applied to $1 - \operatorname{inv} (p)$ and $x_{5}$.

MeasureTheory.Lp.toTemperedDistributionCLMdefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the tempered distribution continuous linear map of x5 and p (from the name)

English

Let $F$ be a set. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{MeasureTheory\_\_Lp\_\_toTemperedDistributionCLM\_\_\_auto\_1}$. Let $p$ be an element of $\mathrm{ENNReal}$. Then the tempered distribution continuous linear map of $x_{5}$ and $p$ is a continuous linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{5})}{x_{6}})}$ and the set of tempered distributions of $E$ and $F$.

MeasureTheory.Measure.toTemperedDistributiondefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the tempered distribution of x3 (from the name)

English

Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{\_private\_\_Mathlib\_\_Analysis\_\_Distribution\_\_TemperedDistribution\_\_0\_\_\_auto\_26}$. Then the tempered distribution of $x_{3}$ is a tempered distribution of $E$ and the set of complexes defined as $\operatorname{toPointwiseConvergenceCLM}$ applied to the set of complexes, the identity ring homomorphism of the set of complexes, the set of Schwartz maps of $E$ and the set of complexes, the set of complexes and the integral of the set of complexes and $x_{3}$.

SchwartzMap.toTemperedDistributionCLMdefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the tempered distribution continuous linear map of x5 (from the name)

English

Let $E$ and $F$ be sets. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{SchwartzMap\_\_toTemperedDistributionCLM\_\_\_auto\_1}$. Then the tempered distribution continuous linear map of $x_{5}$ is a continuous linear map of the set of Schwartz maps of $E$ and $F$ and the set of tempered distributions of $E$ and $F$.

TemperedDistributiondefMathlib.Analysis.Distribution.TemperedDistribution, type

Wording

tempered distribution of E and F (from the name)

English

Let $E$ and $F$ be sets. Then a tempered distribution of $E$ and $F$ is an element of the function that maps $E$ and $F$ to the set of pointwise convergence continuous linear maps of the set of Schwartz maps of $E$ and the set of complexes and $F$.

TemperedDistribution.deltadefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the Dirac delta distribution of x2 (from the docstring)

English

Let $x_{2}$ be an element of $E$. Then the Dirac delta distribution of $x_{2}$ is a tempered distribution of $E$ and the set of complexes defined as $\operatorname{toPointwiseConvergenceCLM}$ applied to the set of complexes, the identity ring homomorphism of the set of complexes, the set of Schwartz maps of $E$ and the set of complexes, the set of complexes and the composition of the evaluation continuous linear map of the set of complexes and $x_{2}$ and the bounded continuous function continuous linear map of $E$ and the set of complexes.

TemperedDistribution.derivCLMdefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the derivative continuous linear map of F (from the name)

English

Let $F$ be a set. Then the derivative continuous linear map of $F$ is a continuous linear map of the set of tempered distributions of $\Real$ and $F$ and the set of tempered distributions of $\Real$ and $F$ defined as the precomposition of $F$ and $\operatorname{neg}$ applied to the derivative continuous linear map of the set of complexes and the set of complexes.

TemperedDistribution.smulLeftCLMdefMathlib.Analysis.Distribution.TemperedDistribution, function or constant

Wording

the scalar multiple left continuous linear map of F and g (from the name)

English

Let $F$ be a set. Let $g$ be a function from elements of $E$ to complexes. Then the scalar multiple left continuous linear map of $F$ and $g$ is a continuous linear map of the set of tempered distributions of $E$ and $F$ and the set of tempered distributions of $E$ and $F$ defined as the precomposition of $F$ and the map of the set of complexes and $g$.

Mathlib.Analysis.Distribution.TestFunction

TestFunctionstructureMathlib.Analysis.Distribution.TestFunction, type

Wording

test function of F and n (from the name)

English

Let $x_{2}$ be an open of $E$. Let $F$ be a set. Let $n$ be a natural number. Then the test functions of $F$ and $n$ are a basic type.

TestFunction.bilinLeftCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the map of B and hg (from the docstring)

English

Let $B$ be a continuous linear map of $x_{5}$ and the set of continuous linear maps of $x_{6}$ and $x_{7}$. Assume that $\mathrm{ContDiff}$ holds for $\Real$, $\operatorname{some}$ applied to $n$ and $g$. Then the map of $B$ and $\mathrm{hg}$ is a continuous linear map of the set of test functions of $x_{5}$ and $n$ and the set of test functions of $x_{7}$ and $n$.

TestFunction.copydefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a test function of $F$ and $n$. Let $\mathrm{f'}$ be a function from elements of $E$ to elements of $F$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a test function of $F$ and $n$.

TestFunction.fderivCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the derivative continuous linear map of n and k (from the name)

English

Let $x$ be a set. Let $n$ and $k$ be natural numbers. Then the derivative continuous linear map of $n$ and $k$ is a continuous linear map of the set of test functions of $F$ and $n$ and the set of test functions of the set of continuous linear maps of $E$ and $F$ and $k$.

TestFunction.integralAgainstBilinCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

no wording

English

Let $B$ be a continuous linear map of $x_{5}$ and the set of continuous linear maps of $x_{6}$ and $x_{7}$. Let $x_{17}$ be a measure of $E$. Let $x_{18}$ be a function from elements of $E$ to elements of $x_{6}$. Then $\operatorname{integralAgainstBilinCLM}$ applied to $B$, $x_{17}$ and $x_{18}$ is a continuous linear map of the set of test functions of $x_{5}$ and $n$ and $x_{7}$.

TestFunction.limitCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the limit continuous linear map of toFun and T (from the name)

English

Let $x$ be a set. Let $\mathrm{toFun}$ be a function from test functions of $F$ and $n$ to elements of $V$. Let $T$ be a function from compacts $K_{1}$ of $E$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (K_{1} , x_{4})$ to continuous linear maps of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K_{1}$ and $V$ such that for all compacts $K$ of $E$, for all elements $h_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (K , x_{4})$, for all elements $f$ of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$, $\mathrm{toFun}$ applied to the test function of $h_{5}$ and $f$ is equal to $T$ applied to $K$, $h_{5}$ and $f$. Then the limit continuous linear map of $\mathrm{toFun}$ and $K_{1}$ is a continuous linear map of the set of test functions of $F$ and $n$ and $V$.

TestFunction.lineDerivCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the line derivative continuous linear map of x and v (from the name)

English

Let $x$ be a set. Let $v$ be an element of $E$. Then the line derivative continuous linear map of $x$ and $v$ is a continuous linear map of the set of test functions of $F$ and $n$ and the set of test functions of $F$ and $k$.

TestFunction.mkCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the continuous linear map of toFun (from the name)

English

Let $x$ be a set. Let $\mathrm{toFun}$ be a function from test functions of $F$ and $n$ to elements of $V$ such that for all test functions $f_{1}$ of $F$ and $n$, for all test functions $g$ of $F$ and $n$, $\EqtMACRoH {\mathrm{toFun} (f_{1} + g)}{\mathrm{toFun} (f_{1})+ \mathrm{toFun} (g)}$, for all elements $c$ of $x$, for all test functions $f$ of $F$ and $n$, $\EqtMACRoH {\mathrm{toFun} (\HSMulhSMulMACRoAL {c}{f})}{\HSMulhSMulMACRoAL {c}{\mathrm{toFun} (f)}}$ and for all compacts $K$ of $E$, for all elements $h_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (K , x_{4})$, $\operatorname{comp}$ applied to $\mathrm{toFun}$ and $\operatorname{ofSupportedIn}$ applied to $h_{5}$ is continuous. Then the continuous linear map of $\mathrm{toFun}$ is a continuous linear map of the set of test functions of $F$ and $n$ and $V$.

TestFunction.monoCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the monotone continuous linear map of x (from the name)

English

Let $x$ be a set. Then the monotone continuous linear map of $x$ is a continuous linear map of the set of test functions of $F$ and $x_{9}$ and the set of test functions of $F$ and $x_{10}$.

TestFunction.ofSupportedIndefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the test function of h and f (from the name)

English

Assume that $K \leq x_{2}$. Let $f$ be an element of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$. Then the test function of $h$ and $f$ is a test function of $F$ and $n$.

TestFunction.ofSupportedInCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the test function of x and h1 (from the name)

English

Let $x$ be a set. Assume that $K \leq x_{4}$. Then the test function of $x$ and $h_{1}$ is a continuous linear map of $\mathrm{ContDiffMapSupportedIn}$ applied to $E$, $F$, $n$ and $K$ and the set of test functions of $F$ and $n$.

TestFunction.postcompCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the postcomposition continuous linear map of T (from the name)

English

Let $T$ be a continuous linear map of $F$ and $\mathrm{F'}$. Then the postcomposition continuous linear map of $T$ is a continuous linear map of the set of test functions of $F$ and $n$ and the set of test functions of $\mathrm{F'}$ and $n$.

TestFunction.toBoundedContinuousFunctionCLMdefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the bounded continuous function continuous linear map of x (from the name)

English

Let $x$ be a set. Then the bounded continuous function continuous linear map of $x$ is a continuous linear map of the set of test functions of $F$ and $n$ and the set of bounded continuous functions of $E$ and $F$.

TestFunction.toFundefMathlib.Analysis.Distribution.TestFunction, function or constant

Wording

the underlying function of self and x5 (from the docstring)

English

Let $\mathrm{self}$ be a test function of $F$ and $n$. Let $x_{5}$ be an element of $E$. Then the underlying function of $\mathrm{self}$ and $x_{5}$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{5}$.

TestFunctionClassclassMathlib.Analysis.Distribution.TestFunction, predicate

Wording

no wording

English

Let $B$ be a set. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of opens of $E$. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $n$ be an element of $\mathrm{outParam}$ applied to the set of natural numbers. Then we can say that $\mathrm{TestFunctionClass}$ holds for $B$, $x_{2}$, $F$ and $n$.

Mathlib.Analysis.Fourier.AddCircle

AddCircle.haarAddCircledefMathlib.Analysis.Fourier.AddCircle, function or constant

Wording

the Haar additive circle (from the name)

English

generation took over the time limit

fourierdefMathlib.Analysis.Fourier.AddCircle, function or constant

Wording

the Fourier of n (from the name)

English

Let $n$ be an integer. Then the Fourier of $n$ is a continuous map of the set of additive circles of $T$ and the set of complexes.

fourierBasisdefMathlib.Analysis.Fourier.AddCircle, function or constant

Wording

the Fourier basis (from the name)

English

The Fourier basis is a Hilbert basis of the set of complexes and $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{Lp} (\mathrm{Complex} , 2 , \operatorname{haarAddCircle})}{x})}$.

fourierCoeffdefMathlib.Analysis.Fourier.AddCircle, function or constant

Wording

the Fourier coefficient of f and n (from the name)

English

Let $f$ be a function from additive circles of $T$ to elements of $E$. Let $n$ be an integer. Then the Fourier coefficient of $f$ and $n$ is an element of $E$ defined as the Bochner integral of the Haar additive circle and the function that maps $t$ to $\HSMulhSMulMACRoAL {\operatorname{fourier} (\operatorname{neg} (n), t)}{f (t)}$.

fourierCoeffOndefMathlib.Analysis.Fourier.AddCircle, function or constant

Wording

no wording

English

Assume that $a < b$. Let $f$ be a function from real numbers to elements of $E$. Let $n$ be an integer. Then $\mathrm{fourierCoeffOn}$ applied to $\mathrm{hab}$, $f$ and $n$ is an element of $E$ defined as the Fourier coefficient of $\operatorname{liftIoc}$ applied to $b - a$, $a$ and $f$ and $n$.

fourierLpdefMathlib.Analysis.Fourier.AddCircle, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{ENNReal}$. Let $n$ be an element of $\Integer$. Then $\mathrm{fourierLp}$ applied to $p$ and $n$ is an element of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{Lp} (\mathrm{Complex} , p , \operatorname{haarAddCircle})}{x})}$ defined as $\operatorname{toLp}$ applied to $p$, the Haar additive circle, the set of complexes and the Fourier of $n$.

fourierSubalgebradefMathlib.Analysis.Fourier.AddCircle, function or constant

Wording

the Fourier subalgebra (from the name)

English

The Fourier subalgebra is a star subalgebra of the set of complexes and the set of continuous maps of the set of additive circles of $T$ and the set of complexes.

Mathlib.Analysis.Fourier.AddCircleMulti

UnitAddTorus.mFourierdefMathlib.Analysis.Fourier.AddCircleMulti, function or constant

Wording

the Fourier of n (from the name)

English

Let $n$ be a function from elements of $d$ to integers. Then the Fourier of $n$ is a continuous map of the set of unit additive toruses of $d$ and the set of complexes.

UnitAddTorus.mFourierBasisdefMathlib.Analysis.Fourier.AddCircleMulti, function or constant

Wording

the Fourier basis (from the name)

English

The Fourier basis is a Hilbert basis of the set of complexes and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{Lp} (\mathrm{Complex} , 2 , \operatorname{volume})}{x_{2}})}$.

UnitAddTorus.mFourierCoeffdefMathlib.Analysis.Fourier.AddCircleMulti, function or constant

Wording

the Fourier coefficient of f and n (from the name)

English

Let $f$ be a function from unit additive toruses of $d$ to elements of $E$. Let $n$ be a function from elements of $d$ to integers. Then the Fourier coefficient of $f$ and $n$ is an element of $E$ defined as the Bochner integral of the volume and the function that maps $t$ to $\HSMulhSMulMACRoAL {\operatorname{mFourier} (\operatorname{neg} (n), t)}{f (t)}$.

UnitAddTorus.mFourierLpdefMathlib.Analysis.Fourier.AddCircleMulti, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{ENNReal}$. Let $n$ be a function from elements of $d$ to elements of $\Integer$. Then $\operatorname{mFourierLp}$ applied to $p$ and $n$ is an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{Lp} (\mathrm{Complex} , p , \operatorname{volume})}{x_{1}})}$ defined as $\operatorname{toLp}$ applied to $p$, the volume, the set of complexes and the Fourier of $n$.

UnitAddTorus.mFourierSubalgebradefMathlib.Analysis.Fourier.AddCircleMulti, function or constant

Wording

the star subalgebra of d (from the docstring)

English

Let $d$ be a set. Then the star subalgebra of $d$ is a star subalgebra of the set of complexes and the set of continuous maps of the set of unit additive toruses of $d$ and the set of complexes.

UnitAddTorus.measurableEquivPiIocdefMathlib.Analysis.Fourier.AddCircleMulti, function or constant

Wording

no wording

English

Let $b$ be a function from elements of $x$ to real numbers. Then $\operatorname{measurableEquivPiIoc}$ applied to $b$ is a measurable equivalence of the set of unit additive toruses of $x$ and $\SubtypeSet {x_{1}}{\mathrm{forall} (x , \lambda i . \MembershipmemMACRoT {\operatorname{Ioc} (b (i), b (i)+ 1)}{x_{1} (i)})}$ defined as the composition of the right product congruence of the function that maps $i$ to $\operatorname{measurableEquivIoc}$ applied to $1$ and $b$ applied to $i$ and the inverse of the subtype product equivalence product.

Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

BoundedContinuousFunction.chardefMathlib.Analysis.Fourier.BoundedContinuousFunctionChar, function or constant

Wording

the characteristic of w (from the name)

English

Assume that $\operatorname{coe}$ applied to $e$ is continuous. Assume that the function that maps $p$ to $\operatorname{coe}$ applied to $L$, $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$ is continuous. Let $w$ be an element of $W$. Then the characteristic of $w$ is a bounded continuous function of $V$ and the set of complexes.

BoundedContinuousFunction.charAlgHomdefMathlib.Analysis.Fourier.BoundedContinuousFunctionChar, function or constant

Wording

the characteristic algebra homomorphism of he and hL (from the name)

English

Assume that $\operatorname{coe}$ applied to $e$ is continuous. Assume that the function that maps $p$ to $\operatorname{coe}$ applied to $L$, $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$ is continuous. Then the characteristic algebra homomorphism of $\mathrm{he}$ and $\mathrm{hL}$ is an algebra homomorphism of the set of additive monoid algebras of the set of complexes and $W$ and the set of bounded continuous functions of $V$ and the set of complexes defined as $\operatorname{lift}$ applied to the set of complexes, the set of bounded continuous functions of $V$ and the set of complexes, $W$ and the characteristic monoid homomorphism of $\mathrm{he}$ and $\mathrm{hL}$.

BoundedContinuousFunction.charMonoidHomdefMathlib.Analysis.Fourier.BoundedContinuousFunctionChar, function or constant

Wording

the characteristic monoid homomorphism of he and hL (from the name)

English

Assume that $\operatorname{coe}$ applied to $e$ is continuous. Assume that the function that maps $p$ to $\operatorname{coe}$ applied to $L$, $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$ is continuous. Then the characteristic monoid homomorphism of $\mathrm{he}$ and $\mathrm{hL}$ is a monoid homomorphism of the set of multiplicatives of $W$ and the set of bounded continuous functions of $V$ and the set of complexes defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $w$ to the characteristic of $\operatorname{toAdd}$ applied to $w$ and $\mathrm{BoundedContinuousFunction\_\_char\_zero\_eq\_one}$ and $\mathrm{BoundedContinuousFunction\_\_char\_add\_eq\_mul}$.

BoundedContinuousFunction.charPolydefMathlib.Analysis.Fourier.BoundedContinuousFunctionChar, function or constant

Wording

the characteristic polynomial of he and hL (from the name)

English

Assume that $\operatorname{coe}$ applied to $e$ is continuous. Assume that the function that maps $p$ to $\operatorname{coe}$ applied to $L$, $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$ is continuous. Then the characteristic polynomial of $\mathrm{he}$ and $\mathrm{hL}$ is a star subalgebra of the set of complexes and the set of bounded continuous functions of $V$ and the set of complexes defined as $\operatorname{mk}$ applied to the range of the characteristic algebra homomorphism of $\mathrm{he}$ and $\mathrm{hL}$ and the function that maps $x_{6}$ and $\mathrm{hx}$ to $\mathrm{BoundedContinuousFunction\_\_star\_mem\_range\_charAlgHom}$ applied to $\mathrm{he}$, $\mathrm{hL}$ and $\mathrm{hx}$.

Mathlib.Analysis.Fourier.Convolution

SchwartzMap.convolutiondefMathlib.Analysis.Fourier.Convolution, function or constant

Wording

the convolution of B (from the name)

English

Let $B$ be a continuous linear map of $x_{1}$ and the set of continuous linear maps of $x_{2}$ and $x_{3}$. Then the convolution of $B$ is a linear map of the set of Schwartz maps of $E$ and $x_{1}$ and the set of continuous linear maps of the set of Schwartz maps of $E$ and $x_{2}$ and the set of Schwartz maps of $E$ and $x_{3}$.

Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

AddChar.circleEquivComplexdefMathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality, function or constant

Wording

the circle equivalence complex (from the name)

English

The circle equivalence complex is an additive equivalence of the set of additive characteristics of $x$ and the set of circles and the set of additive characteristics of $x$ and the set of complexes.

AddChar.complexBasisdefMathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality, function or constant

Wording

the complex basis of x (from the name)

English

Let $x$ be a set. Then the complex basis of $x$ is a basis of the set of complexes and the set of functions from elements of $x$ to complexes.

AddChar.doubleDualEquivdefMathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality, function or constant

Wording

the double dual isomorphism (from the docstring)

English

The double dual isomorphism is an additive equivalence of $x$ and the set of additive characteristics of the set of additive characteristics of $x$ and the set of complexes and the set of complexes defined as the additive equivalence of the double dual embedding and $\mathrm{AddChar\_\_doubleDualEmb\_bijective}$.

AddChar.zmoddefMathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality, function or constant

Wording

the integer modulo of n and x (from the name)

English

Let $n$ be a natural number. Let $x$ be an element of $\mathrm{ZMod}$ applied to $n$. Then the integer modulo of $n$ and $x$ is an additive characteristic of $\mathrm{ZMod}$ applied to $n$ and the set of circles.

AddChar.zmodAddEquivdefMathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality, function or constant

Wording

the integer modulo additive equivalence (from the name)

English

The integer modulo additive equivalence is an additive equivalence of $\mathrm{ZMod}$ applied to $n$ and the set of additive characteristics of $\mathrm{ZMod}$ applied to $n$ and the set of complexes.

AddChar.zmodHomdefMathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality, function or constant

Wording

the integer modulo homomorphism (from the name)

English

The integer modulo homomorphism is an additive characteristic of $\mathrm{ZMod}$ applied to $n$ and the set of additive characteristics of $\mathrm{ZMod}$ applied to $n$ and the set of circles.

Mathlib.Analysis.Fourier.FourierTransform

Fourier.fourierIntegraldefMathlib.Analysis.Fourier.FourierTransform, function or constant

Wording

the Fourier integral of f and w (from the name)

English

Let $e$ be an additive characteristic of $x$ and the set of circles. Let $x_{5}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Let $w$ be an element of $x$. Then the Fourier integral of $f$ and $w$ is an element of $E$ defined as the Fourier integral of $f$ and $w$.

Real.Lp.fourierTransformdefMathlib.Analysis.Fourier.FourierTransform, function or constant

Wording

the Fourier transform of f (from the name)

English

Let $f$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , \operatorname{volume})}{x_{5}})}$. Then the Fourier transform of $f$ is a bounded continuous function of $V$ and $E$.

Real.Lp.fourierTransformCLMdefMathlib.Analysis.Fourier.FourierTransform, function or constant

Wording

the Fourier transform continuous linear map of V and E (from the name)

English

Let $V$ and $E$ be sets. Then the Fourier transform continuous linear map of $V$ and $E$ is a continuous linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , \operatorname{volume})}{x_{5}})}$ and the set of bounded continuous functions of $V$ and $E$.

Real.Lp.fourierTransformInvdefMathlib.Analysis.Fourier.FourierTransform, function or constant

Wording

the Fourier transform inverse of f (from the name)

English

Let $f$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , \operatorname{volume})}{x_{5}})}$. Then the Fourier transform inverse of $f$ is a bounded continuous function of $V$ and $E$ defined as $\operatorname{compContinuous}$ applied to the Fourier transform of $f$ and $\operatorname{neg}$ applied to the identity of $V$.

Real.Lp.fourierTransformInvCLMdefMathlib.Analysis.Fourier.FourierTransform, function or constant

Wording

the Fourier transform inverse continuous linear map of V and E (from the name)

English

Let $V$ and $E$ be sets. Then the Fourier transform inverse continuous linear map of $V$ and $E$ is a continuous linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , \operatorname{volume})}{x_{5}})}$ and the set of bounded continuous functions of $V$ and $E$ defined as the composition of the composition continuous continuous linear map of $\operatorname{neg}$ applied to the identity of $V$ and the Fourier transform continuous linear map of $V$ and $E$.

VectorFourier.fourierIntegraldefMathlib.Analysis.Fourier.FourierTransform, function or constant

Wording

the Fourier integral of f and w (from the name)

English

Let $e$ be an additive characteristic of $x$ and the set of circles. Let $x_{9}$ be a measure of $V$. Let $L$ be a linear map of $V$ and the set of linear maps of $W$ and $x$. Let $f$ be a function from elements of $V$ to elements of $E$. Let $w$ be an element of $W$. Then the Fourier integral of $f$ and $w$ is an element of $E$ defined as the Bochner integral of $x_{9}$ and the function that maps $v$ to $\HSMulhSMulMACRoAL {e (\operatorname{neg} (\operatorname{coe} (L , v , w)))}{f (v)}$.

Mathlib.Analysis.Fourier.FourierTransformDeriv

VectorFourier.fourierPowSMulRightdefMathlib.Analysis.Fourier.FourierTransformDeriv, function or constant

Wording

the right Fourier power multiplicative of f and v (from the name)

English

Let $L$ be a continuous linear map of $V$ and the set of continuous linear maps of $W$ and $\Real$. Let $f$ be a function from elements of $V$ to elements of $E$. Let $v$ be an element of $V$. Then the right Fourier power multiplicative of $f$ and $v$ is a formal multilinear series of $W$ and $E$ defined as the function that maps $n$ to $\HSMulhSMulMACRoAL {(\operatorname{neg} (2 \times \operatorname{ofReal} (\operatorname{pi})\times \operatorname{I})^ {n})}{\operatorname{compContinuousLinearMap} (\operatorname{mkPiRing} (f (v)), \lambda x_{6} . L (v))}$.

VectorFourier.fourierSMulRightdefMathlib.Analysis.Fourier.FourierTransformDeriv, function or constant

Wording

the right Fourier multiplicative of f and v (from the name)

English

Let $L$ be a continuous linear map of $V$ and the set of continuous linear maps of $W$ and $\Real$. Let $f$ be a function from elements of $V$ to elements of $E$. Let $v$ be an element of $V$. Then the right Fourier multiplicative of $f$ and $v$ is a continuous linear map of $W$ and $E$ defined as $\HSMulhSMulMACRoAL {\operatorname{neg} (2 \times \operatorname{ofReal} (\operatorname{pi})\times \operatorname{I})}{\operatorname{smulRight} (L (v), f (v))}$.

Mathlib.Analysis.Fourier.LpSpace

MeasureTheory.Lp.fourierTransformₗᵢdefMathlib.Analysis.Fourier.LpSpace, function or constant

Wording

the Fourier transform of E and F (from the name)

English

Let $E$ and $F$ be sets. Then the Fourier transform of $E$ and $F$ is a linear isometry equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , 2 , \operatorname{volume})}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , 2 , \operatorname{volume})}{x_{6}})}$.

Mathlib.Analysis.Fourier.Notation

ContinuousFourierclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a continuous Fourier (from the name)

English

Let $E$ be a set. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a continuous Fourier.

ContinuousFourierInvclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a continuous Fourier inverse (from the name)

English

Let $E$ be a set. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a continuous Fourier inverse.

FourierAddclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a Fourier sum (from the name)

English

Let $E$ be a set. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a Fourier sum.

FourierInvAddclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a Fourier inverse sum (from the name)

English

Let $E$ be a set. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a Fourier inverse sum.

FourierInvPairclassMathlib.Analysis.Fourier.Notation, predicate

Wording

no wording

English

Let $E$ and $F$ be sets. Then we can say that $\mathrm{FourierInvPair}$ holds for $E$ and $F$.

FourierInvSMulclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a Fourier inverse product (from the name)

English

Let $R$ and $E$ be sets. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a Fourier inverse product.

FourierPairclassMathlib.Analysis.Fourier.Notation, predicate

Wording

no wording

English

Let $E$ and $F$ be sets. Then we can say that $\mathrm{FourierPair}$ holds for $E$ and $F$.

FourierSMulclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a Fourier product (from the name)

English

Let $R$ and $E$ be sets. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a Fourier product.

FourierTransformclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a Fourier transform (from the name)

English

Let $E$ be a set. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a Fourier transform.

FourierTransform.fourierdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the Fourier transform of x (from the docstring)

English

Let $x$ be an element of $E$. Then the Fourier transform of $x$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

FourierTransform.fourierCLEdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the Fourier transform of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the Fourier transform of $R$ and $E$ is a continuous linear equivalence of $E$ and $F$.

FourierTransform.fourierCLMdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the Fourier transform of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the Fourier transform of $R$ and $E$ is a continuous linear map of $E$ and $F$.

FourierTransform.fourierEquivdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the Fourier transform of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the Fourier transform of $R$ and $E$ is a linear equivalence of $E$ and $F$ defined as $\operatorname{mk}$ applied to the Fourier transform of $R$ and $E$, $\operatorname{fourierInv}$, $\mathrm{FourierPair\_\_fourierInv\_fourier\_eq}$ and $\mathrm{FourierInvPair\_\_fourier\_fourierInv\_eq}$.

FourierTransform.fourierInvCLMdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the inverse Fourier transform of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the inverse Fourier transform of $R$ and $E$ is a continuous linear map of $E$ and $F$.

FourierTransform.fourierInvₗdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the inverse Fourier transform of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the inverse Fourier transform of $R$ and $E$ is a linear map of $E$ and $F$.

FourierTransform.fourierₗdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the Fourier transform of R and E (from the docstring)

English

Let $R$ and $E$ be sets. Then the Fourier transform of $R$ and $E$ is a linear map of $E$ and $F$.

FourierTransformInvclassMathlib.Analysis.Fourier.Notation, predicate

Wording

F is a Fourier transform inverse (from the name)

English

Let $E$ be a set. Let $F$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $F$ is a Fourier transform inverse.

FourierTransformInv.fourierInvdefMathlib.Analysis.Fourier.Notation, function or constant

Wording

the inverse Fourier transform of x (from the docstring)

English

Let $x$ be an element of $E$. Then the inverse Fourier transform of $x$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

Mathlib.Analysis.Fourier.ZMod

ZMod.dftdefMathlib.Analysis.Fourier.ZMod, function or constant

Wording

no wording

English

$\operatorname{dft}$ is a linear equivalence of the set of functions from elements of $\mathrm{ZMod}$ applied to $N$ to elements of $E$ and the set of functions from elements of $\mathrm{ZMod}$ applied to $N$ to elements of $E$.

Mathlib.Analysis.FunctionalSpaces.BesselPotentialSpace

BesselPotentialSpacestructureMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, type

Wording

no wording

English

Let $E$ and $F$ be sets. Let $s$ be a real number. Let $p$ be an element of $\mathrm{ENNReal}$. Then the elements of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$ are a basic type.

BesselPotentialSpace.coeAddMonoidHomdefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

the coercion additive monoid homomorphism of s and p (from the name)

English

Let $E$ and $F$ be sets. Let $s$ be a real number. Let $p$ be an element of $\mathrm{ENNReal}$. Then the coercion additive monoid homomorphism of $s$ and $p$ is an additive monoid homomorphism of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$ and the set of tempered distributions of $E$ and $F$.

BesselPotentialSpace.copydefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

the copy of f and hs (from the name)

English

Let $\mathrm{s'}$ be a real number. Let $f$ be an element of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (s , \mathrm{s'})$ and $\mathrm{BesselPotentialSpace\_\_copy\_\_\_auto\_1}$. Then the copy of $\mathrm{s'}$ and $f$ is an element of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $\mathrm{s'}$ and $p$.

BesselPotentialSpace.ofLpdefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

no wording

English

Let $s$ be an element of $\Real$. Let $f$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{volume})}{x_{5}})}$. Then $\operatorname{ofLp}$ applied to $s$ and $f$ is an element of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$.

BesselPotentialSpace.toDistrdefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

the underlying tempered distribution of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$. Then the underlying tempered distribution of $\mathrm{self}$ is a tempered distribution of $E$ and $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

BesselPotentialSpace.toLpdefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$. Then $\operatorname{toLp}$ applied to $\mathrm{self}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{volume})}{x_{5}})}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

BesselPotentialSpace.toLpₗdefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

no wording

English

Let $E$ and $F$ be sets. Let $s$ be an element of $\Real$. Let $p$ be an element of $\mathrm{ENNReal}$. Then $\mathrm{BesselPotentialSpace\_\_toLp\_u2097\_}$ applied to $E$, $F$, $s$ and $p$ is a linear map of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{volume})}{x_{5}})}$.

BesselPotentialSpace.toLpₗᵢdefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

no wording

English

Let $E$ and $F$ be sets. Let $s$ be an element of $\Real$. Let $p$ be an element of $\mathrm{ENNReal}$. Then $\mathrm{BesselPotentialSpace\_\_toLp\_u2097\_\_u1d62\_}$ applied to $E$, $F$, $s$ and $p$ is a linear isometry equivalence of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{volume})}{x_{5}})}$.

TemperedDistribution.MemSobolev.toBesselPotentialSpacedefMathlib.Analysis.FunctionalSpaces.BesselPotentialSpace, function or constant

Wording

no wording

English

Assume that $\operatorname{MemSobolev}$ holds for $s$, $p$ and $f$. Then $\operatorname{toBesselPotentialSpace}$ applied to $\mathrm{hf}$ is an element of $\mathrm{BesselPotentialSpace}$ applied to $E$, $F$, $s$ and $p$.

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

MeasureTheory.GridLines.TdefMathlib.Analysis.FunctionalSpaces.SobolevInequality, function or constant

Wording

no wording

English

Let $x_{2}$ be a function from elements $i_{2}$ of $x$ to measures of $A$ applied to $i_{2}$. Let $p$ be a real number. Let $f$ be a function from functions from elements $i_{1}$ of $x$ to elements of $A$ applied to $i_{1}$ to elements of $\mathrm{ENNReal}$. Let $s$ be a finite set of $x$. Let $x_{4}$ be a function from elements $i$ of $x$ to elements of $A$ applied to $i$. Then $\operatorname{T}$ applied to $i_{2}$, $x_{2}$, $p$, $f$, $s$, $i$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as the function that maps $i$ and $x_{4}$ to $\operatorname{lmarginal}$ applied to $i_{2}$, $f$, $p ^ {(1 - (\FinsetcardMACRoM {f}- 1)\times x_{2})}\times \FinsetProd {f}{i}{x_{4}}{\mathrm{pow} (\operatorname{lmarginal} (i_{2} , \operatorname{singleton} (i), p), x_{2} , x_{4})}$, $s$, $i$ and $x_{4}$.

MeasureTheory.SNormLESNormFDerivOfEqConstdefMathlib.Analysis.FunctionalSpaces.SobolevInequality, function or constant

Wording

no wording

English

Let $F$ be a set. Let $x_{5}$ be a measure of $E$. Let $p$ be a real number. Then $\operatorname{SNormLESNormFDerivOfEqConst}$ applied to $F$, $x_{5}$ and $p$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_FunctionalSpaces\_\_SobolevInequality\_\_99221531\_\_\_hygCtx\_\_\_hyg\_\_76}$, $F$, $x_{5}$ and $p$.

MeasureTheory.eLpNormLESNormFDerivOfEqInnerConstdefMathlib.Analysis.FunctionalSpaces.SobolevInequality, function or constant

Wording

no wording

English

Let $x_{3}$ be a measure of $E$. Let $p$ be a real number. Then $\operatorname{eLpNormLESNormFDerivOfEqInnerConst}$ applied to $x_{3}$ and $p$ is an element of $\mathrm{NNReal}$ defined as the product of $\operatorname{eLpNormLESNormFDerivOneConst}$ applied to $x_{3}$ and $\operatorname{toReal}$ applied to the conjugate exponent of the rank of $\Real$ and $E$ and $\operatorname{toNNReal}$ applied to the quotient of the product of $p$ and the difference between the rank of $\Real$ and $E$ and $1$ and the difference between the rank of $\Real$ and $E$ and $p$.

MeasureTheory.eLpNormLESNormFDerivOfLeConstdefMathlib.Analysis.FunctionalSpaces.SobolevInequality, function or constant

Wording

no wording

English

Let $F$ be a set. Let $x_{5}$ be a measure of $E$. Let $s$ be an element of $\wp E$. Let $p$ and $q$ be elements of $\mathrm{NNReal}$. Then $\operatorname{eLpNormLESNormFDerivOfLeConst}$ applied to $F$, $x_{5}$, $s$, $p$ and $q$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_FunctionalSpaces\_\_SobolevInequality\_\_2519355312\_\_\_hygCtx\_\_\_hyg\_\_76}$, $F$, $x_{5}$, $s$, $p$ and $q$.

MeasureTheory.eLpNormLESNormFDerivOneConstdefMathlib.Analysis.FunctionalSpaces.SobolevInequality, function or constant

Wording

no wording

English

Let $x_{3}$ be a measure of $E$. Let $p$ be a real number. Then $\operatorname{eLpNormLESNormFDerivOneConst}$ applied to $x_{3}$ and $p$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_FunctionalSpaces\_\_SobolevInequality\_\_1730801410\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{3}$ and $p$.

MeasureTheory.lintegralPowLePowLIntegralFDerivConstdefMathlib.Analysis.FunctionalSpaces.SobolevInequality, function or constant

Wording

no wording

English

Let $x_{3}$ be a measure of $E$. Let $p$ be a real number. Then $\operatorname{lintegralPowLePowLIntegralFDerivConst}$ applied to $x_{3}$ and $p$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_FunctionalSpaces\_\_SobolevInequality\_\_3051830255\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{3}$ and $p$.

Mathlib.Analysis.InnerProductSpace.Adjoint

ContinuousLinearMap.adjointdefMathlib.Analysis.InnerProductSpace.Adjoint, function or constant

Wording

the adjoint (from the docstring)

English

The adjoint is a linear isometry equivalence of the set of continuous linear maps of $E$ and $F$ and the set of continuous linear maps of $F$ and $E$.

LinearIsometryEquiv.conjStarAlgEquivdefMathlib.Analysis.InnerProductSpace.Adjoint, function or constant

Wording

the conjugate star algebra isomorphism of e (from the name)

English

Let $e$ be a linear isometry equivalence of $H$ and $K$. Then the conjugate star algebra isomorphism of $e$ is a star algebra isomorphism of the set of continuous linear maps of $H$ and $H$ and the set of continuous linear maps of $K$ and $K$.

LinearMap.IsSymmetric.toSelfAdjointdefMathlib.Analysis.InnerProductSpace.Adjoint, function or constant

Wording

the self adjoint of hT (from the name)

English

Assume that $T$ is symmetric. Then the self adjoint of $\mathrm{hT}$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (\mathrm{ContinuousLinearMap} (E , E))}{x_{4}})}$ defined as $\operatorname{mk}$ applied to $T$ and $\operatorname{continuous}$ applied to $\mathrm{hT}$.

LinearMap.adjointdefMathlib.Analysis.InnerProductSpace.Adjoint, function or constant

Wording

the adjoint (from the docstring)

English

The adjoint is a linear equivalence of the set of linear maps of $E$ and $F$ and the set of linear maps of $F$ and $E$ defined as the composition of the composition of the continuous linear map induced by a linear map and $\operatorname{toLinearEquiv}$ applied to the adjoint and the inverse of the continuous linear map induced by a linear map.

LinearMap.toMatrixOrthonormaldefMathlib.Analysis.InnerProductSpace.Adjoint, function or constant

Wording

no wording

English

Let $x_{6}$ be an orthonormal basis of $x$ and $E$. Then $\operatorname{toMatrixOrthonormal}$ applied to $x_{6}$ is a star algebra isomorphism of the set of linear maps of $E$ and $E$ and the set of matrixes of $n$ and $x$.

Unitary.linearIsometryEquivdefMathlib.Analysis.InnerProductSpace.Adjoint, function or constant

Wording

the linear isometry equivalence (from the name)

English

The linear isometry equivalence is a multiplicative equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{unitary} (\mathrm{ContinuousLinearMap} (H , H))}{x_{4}})}$ and the set of linear isometry equivalences of $H$ and $H$.

Mathlib.Analysis.InnerProductSpace.Basic

innerₗdefMathlib.Analysis.InnerProductSpace.Basic, function or constant

Wording

the inner product of F (from the docstring)

English

Let $F$ be a set. Then the inner product of $F$ is a linear map of $F$ and the set of linear maps of $F$ and $\Real$ defined as the inner product of $\Real$.

innerₛₗdefMathlib.Analysis.InnerProductSpace.Basic, function or constant

Wording

the inner product of x (from the docstring)

English

Let $x$ be a set. Then the inner product of $x$ is a linear map of $E$ and the set of linear maps of $E$ and $x$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_'\_u209b\_\_u2097\_}$ applied to the star ring end of $x$, the identity ring homomorphism of $x$, the function that maps $v$ and $w$ to $\operatorname{inner}$ applied to $x$, $v$ and $w$, $\mathrm{inner\_add\_left}$, the function that maps $x_{4}$, $x_{5}$ and $x_{6}$ to $\mathrm{inner\_smul\_left}$ applied to $x_{5}$, $x_{6}$ and $x_{4}$, $\mathrm{inner\_add\_right}$ and the function that maps $x_{7}$, $x_{8}$ and $x_{9}$ to $\mathrm{inner\_smul\_right}$ applied to $x_{8}$, $x_{9}$ and $x_{7}$.

Mathlib.Analysis.InnerProductSpace.Calculus

fderivInnerCLMdefMathlib.Analysis.InnerProductSpace.Calculus, function or constant

Wording

the derivative inner continuous linear map of x and p (from the name)

English

Let $x$ be a set. Let $p$ be an element of $\mathrm{Prod}$ applied to $E$ and $E$. Then the derivative inner continuous linear map of $x$ and $p$ is a continuous linear map of $\mathrm{Prod}$ applied to $E$ and $E$ and $x$.

Mathlib.Analysis.InnerProductSpace.CanonicalTensor

InnerProductSpace.canonicalContravariantTensordefMathlib.Analysis.InnerProductSpace.CanonicalTensor, function or constant

Wording

the canonical contravariant tensor corresponding to the inner product of E (from the docstring)

English

Let $E$ be a set. Then the canonical contravariant tensor corresponding to the inner product of $E$ is a linear map of the set of tensor products of $E$ and $E$ and $\Real$ defined as the lift of the inner product of $E$.

InnerProductSpace.canonicalCovariantTensordefMathlib.Analysis.InnerProductSpace.CanonicalTensor, function or constant

Wording

the canonical covariant tensor of E (from the name)

English

Let $E$ be a set. Then the canonical covariant tensor of $E$ is a tensor product of $E$ and $E$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{tmul} (\Real , \operatorname{stdOrthonormalBasis} (\Real , E , i), \operatorname{stdOrthonormalBasis} (\Real , E , i))}$.

Mathlib.Analysis.InnerProductSpace.Defs

HilbertSpacestructureMathlib.Analysis.InnerProductSpace.Defs, type

Wording

Hilbert space of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the Hilbert spaces of $x$ and $E$ are a basic type.

InnerclassMathlib.Analysis.InnerProductSpace.Defs, predicate

Wording

no wording

English

Let $x$ and $E$ be sets. Then we can say that $\mathrm{Inner}$ holds for $x$ and $E$.

Inner.innerdefMathlib.Analysis.InnerProductSpace.Defs, function or constant

Wording

no wording

English

Let $x$ be a set. Let $x_{1}$ and $x_{2}$ be elements of $E$. Then $\operatorname{inner}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

InnerProductSpaceclassMathlib.Analysis.InnerProductSpace.Defs, predicate

Wording

no wording

English

Let $x$ and $E$ be sets. Then we can say that $\mathrm{InnerProductSpace}$ holds for $x$ and $E$.

InnerProductSpace.CoreclassMathlib.Analysis.InnerProductSpace.Defs, predicate

Wording

no wording

English

Let $x$ and $F$ be sets. Then we can say that $\operatorname{Core}$ holds for $x$ and $F$.

InnerProductSpace.Core.normSqdefMathlib.Analysis.InnerProductSpace.Defs, function or constant

Wording

the norm square of x4 (from the name)

English

Let $x_{4}$ be an element of $F$. Then the norm square of $x_{4}$ is a real number defined as $\operatorname{re}$ applied to $\operatorname{inner}$ applied to $x$, $x_{4}$ and $x_{4}$.

PreInnerProductSpace.CoreclassMathlib.Analysis.InnerProductSpace.Defs, predicate

Wording

no wording

English

Let $x$ and $F$ be sets. Then we can say that $\operatorname{Core}$ holds for $x$ and $F$.

Mathlib.Analysis.InnerProductSpace.Dual

InnerProductSpace.continuousLinearMapOfBilindefMathlib.Analysis.InnerProductSpace.Dual, function or constant

Wording

the continuous linear map of B (from the name)

English

Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $E$ and $x$. Then the continuous linear map of $B$ is a continuous linear map of $E$ and $E$ defined as the composition of the continuous linear map of the continuous linear equivalence of the inverse of the dual of $x$ and $E$ and $B$.

InnerProductSpace.toDualdefMathlib.Analysis.InnerProductSpace.Dual, function or constant

Wording

the dual of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the dual of $x$ and $E$ is a linear isometry equivalence of $E$ and the set of strong duals of $x$ and $E$.

InnerProductSpace.toDualMapdefMathlib.Analysis.InnerProductSpace.Dual, function or constant

Wording

the dual map of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the dual map of $x$ and $E$ is a linear isometry of $E$ and the set of strong duals of $x$ and $E$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to the inner product of $x$ and $\mathrm{innerSL\_apply\_norm}$ applied to $x$.

Mathlib.Analysis.InnerProductSpace.EuclideanDist

Euclidean.balldefMathlib.Analysis.InnerProductSpace.EuclideanDist, function or constant

Wording

the ball of x3 and r (from the name)

English

Let $x_{3}$ be an element of $E$. Let $r$ be a real number. Then the ball of $x_{3}$ and $r$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the distance of $y$ and $x_{3}$ is less than $r$.

Euclidean.closedBalldefMathlib.Analysis.InnerProductSpace.EuclideanDist, function or constant

Wording

the closed ball of x3 and r (from the name)

English

Let $x_{3}$ be an element of $E$. Let $r$ be a real number. Then the closed ball of $x_{3}$ and $r$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the distance of $y$ and $x_{3}$ is less than or equal to $r$.

Euclidean.distdefMathlib.Analysis.InnerProductSpace.EuclideanDist, function or constant

Wording

the distance of x3 and y (from the name)

English

Let $x_{3}$ and $y$ be elements of $E$. Then the distance of $x_{3}$ and $y$ is a real number defined as the distance of $\operatorname{toEuclidean}$ applied to $x_{3}$ and $\operatorname{toEuclidean}$ applied to $y$.

toEuclideandefMathlib.Analysis.InnerProductSpace.EuclideanDist, function or constant

Wording

no wording

English

$\mathrm{toEuclidean}$ is a continuous linear equivalence of $E$ and the set of Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to the rank of $\Real$ and $E$.

Mathlib.Analysis.InnerProductSpace.ExteriorPower

OrthonormalBasis.exteriorPowerdefMathlib.Analysis.InnerProductSpace.ExteriorPower, function or constant

Wording

the exterior power of b and n (from the name)

English

Let $b$ be an orthonormal basis of $\Real$ and $E$. Let $n$ be an element of $\Natural$. Then the exterior power of $b$ and $n$ is an orthonormal basis of $\Real$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{4}})}$.

Mathlib.Analysis.InnerProductSpace.GramMatrix

Matrix.gramdefMathlib.Analysis.InnerProductSpace.GramMatrix, function or constant

Wording

the Gram of x and v (from the name)

English

Let $x$ be a set. Let $v$ be a function from elements of $n$ to elements of $E$. Then the Gram of $x$ and $v$ is a matrix of $n$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\operatorname{inner}$ applied to $x$, $v$ applied to $i_{1}$ and $v$ applied to $j_{1}$.

Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

InnerProductSpace.gramSchmidtdefMathlib.Analysis.InnerProductSpace.GramSchmidtOrtho, function or constant

Wording

the Gram Schmidt of f and n (from the name)

English

Let $x$ be a set. Let $f$ be a function from elements of $x_{4}$ to elements of $E$. Let $n$ be an element of $x_{4}$. Then the Gram Schmidt of $f$ and $n$ is an element of $E$.

InnerProductSpace.gramSchmidtBasisdefMathlib.Analysis.InnerProductSpace.GramSchmidtOrtho, function or constant

Wording

the Gram Schmidt basis of b (from the name)

English

Let $b$ be a basis of $x$ and $E$. Then the Gram Schmidt basis of $b$ is a basis of $x$ and $E$.

InnerProductSpace.gramSchmidtNormeddefMathlib.Analysis.InnerProductSpace.GramSchmidtOrtho, function or constant

Wording

no wording

English

Let $x$ be a set. Let $f$ be a function from elements of $x_{4}$ to elements of $E$. Let $n$ be an element of $x_{4}$. Then $\operatorname{gramSchmidtNormed}$ applied to $x$, $f$ and $n$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (\operatorname{ofReal} (\operatorname{norm} (\operatorname{gramSchmidt} (f , n))))}{\operatorname{gramSchmidt} (f , n)}$.

InnerProductSpace.gramSchmidtOrthonormalBasisdefMathlib.Analysis.InnerProductSpace.GramSchmidtOrtho, function or constant

Wording

the Gram Schmidt orthonormal basis of h1 and f (from the name)

English

Assume that the rank of $x$ and $E$ is equal to the cardinality of $x_{4}$. Let $f$ be a function from elements of $x_{4}$ to elements of $E$. Then the Gram Schmidt orthonormal basis of $h_{1}$ and $f$ is an orthonormal basis of $x$ and $E$.

Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

InnerProductSpace.HarmonicAtdefMathlib.Analysis.InnerProductSpace.Harmonic.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{4}$ be an element of $E$. Then $\operatorname{HarmonicAt}$ holds for $f$ and $x_{4}$, if $\mathrm{ContDiffAt}$ holds for $\Real$, $2$, $f$ and $x_{4}$ and $\operatorname{EventuallyEq}$ holds for the neighbourhood filter of $x_{4}$, the Laplacian of $f$ and $0$.

Mathlib.Analysis.Complex.Basic

Mathlib.Analysis.Complex.CanonicalDecomposition

Mathlib.Analysis.Complex.Circle

Mathlib.Analysis.Complex.Conformal

Mathlib.Analysis.Complex.Exponential

Mathlib.Analysis.Complex.Hadamard

Mathlib.Analysis.Complex.HasPrimitives

Mathlib.Analysis.Complex.IntegerCompl

Mathlib.Analysis.Complex.Isometry

Mathlib.Analysis.Complex.LocallyUniformLimit

Mathlib.Analysis.Complex.Norm

Mathlib.Analysis.Complex.Periodic

Mathlib.Analysis.Complex.Poisson

Mathlib.Analysis.Complex.Polynomial.GaussLucas

Mathlib.Analysis.Complex.Trigonometric

Mathlib.Analysis.Complex.UnitDisc.Basic

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Truncated

Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Mathlib.Analysis.ConstantSpeed

Mathlib.Analysis.Convex.AmpleSet

Mathlib.Analysis.Convex.Basic

Mathlib.Analysis.Convex.Between

Mathlib.Analysis.Convex.BetweenList

Mathlib.Analysis.Convex.Body

Mathlib.Analysis.Convex.Combination

Mathlib.Analysis.Convex.Cone.Basic

Mathlib.Analysis.Convex.Cone.Closure

Mathlib.Analysis.Convex.Cone.Dual

Mathlib.Analysis.Convex.Cone.InnerDual

Mathlib.Analysis.Convex.DoublyStochasticMatrix

Mathlib.Analysis.Convex.EGauge

Mathlib.Analysis.Convex.Exposed

Mathlib.Analysis.Convex.Extreme

Mathlib.Analysis.Convex.Function

Mathlib.Analysis.Convex.Gauge

Mathlib.Analysis.Convex.GaugeRescale

Mathlib.Analysis.Convex.Hull

Mathlib.Analysis.Convex.Independent

Mathlib.Analysis.Convex.Intrinsic

Mathlib.Analysis.Convex.Join

Mathlib.Analysis.Convex.MetricSpace

Mathlib.Analysis.Convex.PathConnected

Mathlib.Analysis.Convex.Quasiconvex

Mathlib.Analysis.Convex.Segment

Mathlib.Analysis.Convex.Side

Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Mathlib.Analysis.Convex.SimplicialComplex.Basic

Mathlib.Analysis.Convex.Star

Mathlib.Analysis.Convex.Strict

Mathlib.Analysis.Convex.StrictConvexBetween

Mathlib.Analysis.Convex.StrictConvexSpace

Mathlib.Analysis.Convex.Strong

Mathlib.Analysis.Convex.Topology

Mathlib.Analysis.Convex.Uniform

Mathlib.Analysis.Convex.Visible

Mathlib.Analysis.Convolution

Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Mathlib.Analysis.Distribution.DerivNotation

Mathlib.Analysis.Distribution.Distribution

Mathlib.Analysis.Distribution.FourierMultiplier

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Mathlib.Analysis.Distribution.Sobolev

Mathlib.Analysis.Distribution.Support

Mathlib.Analysis.Distribution.TemperateGrowth

Mathlib.Analysis.Distribution.TemperedDistribution

Mathlib.Analysis.Distribution.TestFunction

Mathlib.Analysis.Fourier.AddCircle

Mathlib.Analysis.Fourier.AddCircleMulti