The comparison principle for the Monge–Ampère equation

Let Ω be a bounded open convex subset of a finite-dimensional real inner product space E, and let u and v be convex on Ω and continuous on its closure, with Aleksandrov Monge–Ampère measures MA_u and MA_v (of u and v extended by ⊤ off Ω).

• If u ≤ v on Ω and v ≤ u on the frontier of Ω, then every subgradient of v relative to Ω is a subgradient of u relative to Ω, so MA_v(Ω) ≤ MA_u(Ω): the lower function carries more Monge–Ampère mass.
• The comparison principle. If MA_u ≤ MA_v and v ≤ u on the frontier of Ω, then v ≤ u on Ω. Hence a convex function on Ω, continuous on the closure, is determined by its Monge–Ampère measure and its boundary values; this is the uniqueness half of the Dirichlet problem for the Monge–Ampère equation.

The comparison principle is proved by contradiction. If u x₀ < v x₀, then for small ε > 0 the function w = (1 + ε) v + b of TauCeti.exists_convexOn_lt_frontier_of_lt lies above u at x₀ and strictly below u on the frontier, so the open set G = {u < w} of TauCeti.exists_isOpen_subset_pos_forall_frontier_le has closure inside Ω, and w ≤ u on its frontier. By TauCeti.exists_forall_add_inner_add_le_of_forall_frontier_le, the subgradients of w on G are subgradients of u on G, as are their small perturbations, which form an open ball. The scaling law (MeasureTheory.Measure.mongeAmpereMeasure_ite_mul_add_of_pos) gives MA_w(G) = (1 + ε)^n MA_v(G). Comparing measures, (1 + ε) ^ n MA_v(G) ≤ MA_u(G) ≤ MA_v(G) with 0 < MA_u(G) and MA_v(G) < ∞, which is impossible.

Main statements

• TauCeti.mongeAmpereMeasure_le_of_le_of_le_frontier — a convex function lying below another, with the reverse inequality on the frontier, has larger Monge–Ampère mass;
• TauCeti.le_of_mongeAmpereMeasure_le_of_le_frontier — the comparison principle;
• TauCeti.eqOn_of_mongeAmpereMeasure_eq_of_eqOn_frontier — two convex functions with the same Monge–Ampère measure and the same boundary values agree.
• TauCeti.abs_sub_le_of_smul_le_mongeAmpereMeasure_le_smul — two-sided measure bounds give a quantitative comparison with a zero-boundary reference.

References

• C. E. Gutiérrez, The Monge–Ampère Equation, 2nd ed., Progress in Nonlinear Differential Equations and Their Applications 89, Birkhäuser, 2016, §1.4.
• A. Figalli, The Monge–Ampère Equation and Its Applications, Zurich Lectures in Advanced Mathematics, EMS, 2017, Chapter 2.
• G. De Philippis and A. Figalli, The Monge–Ampère equation and its link to optimal transportation, §2.4, the perturbation argument.
• The density bracketing follows the KLS formalization.

theorem TauCeti.mongeAmpereMeasure_le_of_le_of_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : Set E} [DecidablePred fun (x : E) => x ∈ Ω] {u v : E → ℝ} (μ : MeasureTheory.Measure E) {ν : MeasureTheory.Measure E} [ν.IsAddHaarMeasure] (hμ : μ.AbsolutelyContinuous ν) (hΩo : IsOpen Ω) (hΩ : Bornology.IsBounded Ω) (hu : ConvexOn ℝ Ω u) (hv : ConvexOn ℝ Ω v) (huc : ContinuousOn u (closure Ω)) (hvc : ContinuousOn v (closure Ω)) (hle : ∀ x ∈ Ω, u x ≤ v x) (hfr : ∀ x ∈ frontier Ω, v x ≤ u x) : (mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(v x) else ⊤) Ω ≤ (mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(u x) else ⊤) Ω

A lower convex function with the reverse boundary inequality has more Monge–Ampère mass. Let Ω be a bounded open set, and let u and v be convex on Ω and continuous on its closure, with u ≤ v on Ω and v ≤ u on the frontier of Ω. Then MA_v(Ω) ≤ MA_u(Ω) for the Monge–Ampère measures of u and v (extended by ⊤ off Ω) with respect to any measure μ absolutely continuous with respect to an additive Haar measure.

theorem TauCeti.le_of_mongeAmpereMeasure_le_of_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : Set E} [DecidablePred fun (x : E) => x ∈ Ω] {u v : E → ℝ} [Nontrivial E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hΩo : IsOpen Ω) (hΩ : Bornology.IsBounded Ω) (hu : ConvexOn ℝ Ω u) (hv : ConvexOn ℝ Ω v) (huc : ContinuousOn u (closure Ω)) (hvc : ContinuousOn v (closure Ω)) (hMA : (mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(u x) else ⊤) ≤ mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(v x) else ⊤) (hfr : ∀ x ∈ frontier Ω, v x ≤ u x) {x₀ : E} (hx₀ : x₀ ∈ Ω) : v x₀ ≤ u x₀

The comparison principle for the Monge–Ampère equation. Let Ω be a bounded open subset of a real inner product space E of finite dimension n ≥ 1, and let u and v be convex on Ω and continuous on its closure. If MA_u ≤ MA_v for their Aleksandrov Monge–Ampère measures (of u and v extended by ⊤ off Ω, with respect to an additive Haar measure μ) and v ≤ u on the frontier of Ω, then v ≤ u on Ω.

theorem TauCeti.eqOn_of_mongeAmpereMeasure_eq_of_eqOn_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : Set E} [DecidablePred fun (x : E) => x ∈ Ω] {u v : E → ℝ} [Nontrivial E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hΩo : IsOpen Ω) (hΩ : Bornology.IsBounded Ω) (hu : ConvexOn ℝ Ω u) (hv : ConvexOn ℝ Ω v) (huc : ContinuousOn u (closure Ω)) (hvc : ContinuousOn v (closure Ω)) (hMA : (mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(u x) else ⊤) = mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(v x) else ⊤) (hfr : Set.EqOn u v (frontier Ω)) : Set.EqOn u v Ω

Uniqueness for the Dirichlet problem for the Monge–Ampère equation. Let Ω be a bounded open subset of a real inner product space of finite dimension n ≥ 1, and let u and v be convex on Ω and continuous on its closure. If u and v have the same Aleksandrov Monge–Ampère measure (extended by ⊤ off Ω, with respect to an additive Haar measure μ) and agree on the frontier of Ω, then they agree on Ω.

theorem TauCeti.abs_sub_le_of_smul_le_mongeAmpereMeasure_le_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : Set E} [DecidablePred fun (x : E) => x ∈ Ω] {u v : E → ℝ} [Nontrivial E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu : ConvexOn ℝ Ω u) (hv : ConvexOn ℝ Ω v) (huc : ContinuousOn u (closure Ω)) (hvc : ContinuousOn v (closure Ω)) (hu0 : ∀ x ∈ frontier Ω, u x = 0) (hv0 : ∀ x ∈ frontier Ω, v x = 0) {ν : MeasureTheory.Measure E} {ε : ℝ} (hε : 0 ≤ ε) (hε1 : ε < 1) (hlo : ENNReal.ofReal ((1 - ε) ^ Module.finrank ℝ E) • ν ≤ mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(u x) else ⊤) (hhi : (mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(u x) else ⊤) ≤ ENNReal.ofReal ((1 + ε) ^ Module.finrank ℝ E) • ν) (href : (mongeAmpereMeasure μ fun (x : E) => if x ∈ Ω then ↑(v x) else ⊤) = ν) (x : E) : x ∈ Ω → |u x - v x| ≤ ε * |v x|

Quantitative comparison. On a bounded open set, suppose the convex potentials u and v are continuous on the closure and vanish on the frontier. If the Monge–Ampère measure of v is ν and that of u lies between (1 - ε)^n • ν and (1 + ε)^n • ν for 0 ≤ ε < 1, then |u - v| ≤ ε |v| pointwise.