Let be a natural number with and let be the real numbers, a Dedekind complete ordered field, with the order , the strict order and the quotient notation fixed there; write for the real number , which satisfies by claim 8 of Elementary Order Arithmetic in an Ordered Field, so that is defined. For a real number write for the power .
Regard Euclidean space as a real vector space, with the sum of points and the scalar multiple, write for the difference of points, and let be the Euclidean norm on .
Let be a function whose set of values has an upper bound in , and let satisfy . For put
This set is nonempty, and every upper bound for the values of is an upper bound for it: for each the real number is nonnegative, by claim 1 of Elementary Properties of the Euclidean Norm on together with claim 5 of Elementary Arithmetic in an Ordered Field and claim 1 of Zero Products and Elementary Identities in a Field, so that . Since is Dedekind complete, has a least upper bound in .
The sup-convolution of with parameter is the function whose value at is the least upper bound of , written
In the symbol the superscript is a label, not an exponent.
Loading…
Prerequisites
No prerequisites tracked.
Dependents
No dependents yet.
Dependent proofs
No dependent proofs yet.
No relations recorded yet.