Proof of Basic Properties of a Wasserstein-Coercive Penalty Pair
lemmalem:w2-coercive-penalty-pair-basic-wasserstein-2026aThe second moment is bounded on a sublevel set because the square root of the second moment is continuous on a compact set; the lower bound and the lower semicontinuity of the penalty follow, and the delta-envelopes are exact because a semicontinuous function is its own envelope.
Each result cited is universally quantified over the data in its own statement and is applied here to the data named in the statement of the lemma.
Claim 1. Let and put . If is empty the assertion holds with , there being no to test. Suppose then that is nonempty. By Wasserstein-Coercive Penalty Pairs §coercive, read at the level , the set is sequentially compact in , hence compact by A Sequentially Compact Subset of a Metric Space is Compact.
The function with , the square root being that of Existence and Uniqueness of the Nonnegative Square Root applied to the nonnegative , is continuous on : given and a positive , every with satisfies by claim 2 of The Coordinate Fields of a Coupling, and the Second Moment as a Lipschitz Function of the Wasserstein Distance, read with , the symmetry of (a metric axiom of Metric Space) and mixed transitivity (claim 2 of Elementary Order Arithmetic in an Ordered Field). Its restriction to is continuous on by claim 4 of Semicontinuity and Continuity Under Composition with a Continuous Map.
By Extreme Value Theorem on a Compact Subset of a Metric Space the restriction of to the nonempty compact attains a greatest value, at some ; put . For one has , and both are nonnegative, so claim 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field gives , that is , the squares of the square roots being the numbers themselves by Existence and Uniqueness of the Nonnegative Square Root. This is claim 1.
Claim 2. Let be nonnegative as in Penalty Pairs on the Wasserstein Space: the Penalty, Its Score, and Their Domains §bound, so that for every , where is the second moment. Fix , which is possible because is nonempty, and put . By claim 1, read at this level , there is such that for every with . Let be the least of the two real numbers and , which exists by claim 9 of Elementary Order Arithmetic in an Ordered Field.
Let . The order of is total (an axiom of Ordered Field), so or . In the second case by the transitivity of (Total Order on a Set). In the first case , hence by the compatibility of the order with addition (an axiom of Ordered Field), hence by claim 5 of Elementary Arithmetic in an Ordered Field applied with the nonnegative multiplier . Both this inequality and are equivalent, by claim 3 of Elementary Arithmetic in an Ordered Field, to , so the latter holds; with Penalty Pairs on the Wasserstein Space: the Penalty, Its Score, and Their Domains §bound and the transitivity of (Total Order on a Set), . In both cases , which is claim 2.
Claim 3. Let and let be positive; we verify the defining condition of Lower Semicontinuous Function on a Subset of a Metric Space at relative to in for this . Suppose, to the contrary, that for every positive there is with for which fails, that is, with , the two being complementary because the order of is total. Put and
For the inverse exists and is positive by claim 3 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field, so taking in the contrary assumption shows that the set
is nonempty for every . By Axiom of Countable Choice there is a sequence with for every ; each lies in and satisfies .
The sequence converges to in . Indeed, let be positive. By claim 2 of The Archimedean Property of the Real Numbers there is with . Let satisfy . By the trichotomy of the order of (claim 3 of Properties of the Order on the Natural Numbers) either , or and then by claim 6 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field; in both cases . Multiplying by the nonnegative (claim 5 of Elementary Arithmetic in an Ordered Field) gives , hence by mixed transitivity (claim 2 of Elementary Order Arithmetic in an Ordered Field). Multiplying by the positive (claim 10 of Elementary Order Arithmetic in an Ordered Field) and using gives , so by mixed transitivity.
By Wasserstein-Coercive Penalty Pairs §coercive, read at the level , the set is sequentially compact in , so there are and a strictly increasing sequence in such that converges to in . By A Subsequence of a Convergent Sequence Has the Same Limit the same subsequence converges to , so by Uniqueness of Limits in a Metric Space, and therefore , that is, . By claim 3 of Elementary Arithmetic in an Ordered Field this is equivalent to and hence, by the same claim, to ; with and the antisymmetry of the order (an axiom of Ordered Field) this gives , contradicting the positivity of .
Hence there is a positive such that every with satisfies . As and were arbitrary, is lower semicontinuous on in , which is claim 3.
Claim 4. Every satisfies , so is bounded above near each point of , the constant serving on every ball; hence is defined on by The Delta-Envelopes of a Function on the Wasserstein Space Relative to a Penalty Pair §minus. Likewise for every , so is bounded below near each point and is defined on by The Delta-Envelopes of a Function on the Wasserstein Space Relative to a Penalty Pair §plus.
The restriction of to is upper semicontinuous on relative to by claim 4 of Semicontinuity and Continuity Under Composition with a Continuous Map. By claim 3 the function is lower semicontinuous on relative to , so is lower semicontinuous there by claim 3 of Sums and Nonnegative Multiples of Semicontinuous Functions, applied with the nonnegative multiplier , and is upper semicontinuous by Semicontinuity Under Negation and Characterization of Continuity. Hence , the sum of two upper semicontinuous functions on , is upper semicontinuous on relative to by claim 1 of Sums and Nonnegative Multiples of Semicontinuous Functions. An upper semicontinuous function is its own upper semicontinuous envelope by Properties of the Upper Semicontinuous Envelope §fixed, so
Symmetrically, the restriction of to is lower semicontinuous relative to by claim 4 of Semicontinuity and Continuity Under Composition with a Continuous Map, is lower semicontinuous as just shown, their sum is lower semicontinuous on relative to by claim 3 of Sums and Nonnegative Multiples of Semicontinuous Functions, and a lower semicontinuous function is its own lower semicontinuous envelope by Properties of the Lower Semicontinuous Envelope, by Duality §fixed, so for every . No continuity of or of has been used. This is claim 4.
Loading…
Prerequisites
c788021e-4d08-4fba-8bc8-e9a5a396dc27