TheoremBase

The trace is monotone for the semidefinite order and the common-noise intensity is nonnegative, so the only term depending on the matrix argument is nonincreasing in it.

Proof

Each result cited is universally quantified over the data in its own statement.

Let (ν,q)∈V(DΣ)(\nu,q)\in\mathcal{V}(\mathcal{D}_{\Sigma}), let r∈Rr\in\mathbb{R} and let X,Y∈S(d)X,Y\in\mathcal{S}(d) satisfy X⪯YX\preceq Y. By The Trace as a Sum of Quadratic Forms, its Monotonicity and a Norm Bound (iv), tr X≤tr Y\mathrm{tr}\,X\le\mathrm{tr}\,Y.

The multiplier κ2\tfrac{\kappa}{2}, the product of κ\kappa with the multiplicative inverse of 22, is nonnegative: that inverse is positive by claims 8 and 7 of Elementary Order Arithmetic in an Ordered Field, and claim 5 of Elementary Arithmetic in an Ordered Field, applied to 0≤κ0\le\kappa with it as the nonnegative multiplier, gives 0≤κ20\le\tfrac{\kappa}{2}, since the product of it with 00 is 00 by claim 1 of Zero Products and Elementary Identities in a Field and multiplication is commutative in the ordered field R\mathbb{R}. Hence claim 5 of Elementary Arithmetic in an Ordered Field gives

κ2 tr X≤κ2 tr Y,\frac{\kappa}{2}\,\mathrm{tr}\,X\le\frac{\kappa}{2}\,\mathrm{tr}\,Y ,

and claim 3 of that lemma, used in both directions, gives

−κ2 tr Y≤−κ2 tr X.-\frac{\kappa}{2}\,\mathrm{tr}\,Y\le-\frac{\kappa}{2}\,\mathrm{tr}\,X .

Adding to both sides the real number λ0 r+θ2∥q∥ν2+⟨Σ(ν),q⟩ν−g(ν)\lambda_{0}\,r+\tfrac{\theta}{2}\lVert q\rVert_{\nu}^{2}+\langle\Sigma(\nu),q\rangle_{\nu}-g(\nu), which does not depend on the matrix argument — the compatibility of the order with addition, an axiom of Ordered Field — and reading off the value of the operator from The Discounted Hamilton-Jacobi Equation with Common Noise and a Penalty Drift on the Wasserstein Space (i) gives

F(ν,r,q,Y)≤F(ν,r,q,X).F(\nu,r,q,Y)\le F(\nu,r,q,X).

Since (ν,q)(\nu,q), rr, XX and YY were arbitrary, FF is degenerate elliptic by Degenerate Elliptic Second-Order Equation Operators on the Wasserstein Space (i).

Citations

Loading…

Dependencies

Uses0

Loading…

Comments

Log in to comment.

Loading…