Volume of sections of solutions of the Monge–Ampère equation

Let E be a real inner product space of finite dimension n ≥ 1 with an additive Haar measure μ, and let v be convex on a bounded open set G, continuous on its closure. The Monge–Ampère mass of v on G, the volume of G and the depth of v below its boundary values control each other, with constants depending only on E and μ:

• if v ≥ 0 on the frontier of G, then (max 0 (-v x₀)) ^ n ≤ C μ(G) MA_v(G) for every x₀ ∈ G;
• if v ≤ 0 on the frontier of G, v ≥ -h on G and MA_v ≥ λ μ on G, then λ μ(G)² ≤ C hⁿ.

So a convex function with λ ≤ MA_v ≤ Λ vanishing on the boundary of G has depth comparable to μ(G) ^ (2 / n). Both bounds are affine invariant. They are proved for a domain normalized by an affine equivalence T between the balls of radii r and 1 about 0 (TauCeti.exists_affineEquiv_ball_subset_image_subset_ball), and transferred back by the change of variables MA_{v ∘ T⁻¹}(s) = |det L| MA_v(T⁻¹ '' s), where L is the linear part of T⁻¹ (TauCeti.mongeAmpereMeasure_comp_affineEquiv_apply), together with μ(T⁻¹ '' s) = |det L| μ(s). In the normalized position the first bound is the Aleksandrov maximum principle (TauCeti.ofReal_neg_pow_mul_addHaar_ball_le_mul_mongeAmpereMeasure), and the second is the comparison principle (TauCeti.le_of_mongeAmpereMeasure_le_of_le_frontier) against the quadratic y ↦ (a / 2) (‖y‖² - r²) whose Monge–Ampère measure is aⁿ μ (TauCeti.mongeAmpereMeasure_ite_mul_norm_sq_add).

Applied to v = u - u x - ℓ (· - x) - h on a section S = {y ∈ Ω | u y < u x + ℓ (y - x) + h} whose closure lies in the domain Ω of u, these give the volume estimates for sections: if λ ≤ MA_u ≤ Λ on Ω and ℓ is a supporting slope at x, then λ μ(S)² ≤ C hⁿ and hⁿ ≤ C Λ μ(S)², i.e. μ(S) is comparable to h ^ (n / 2). These estimates are the starting point for the geometry of sections used in the regularity theory of the Monge–Ampère equation.

Main statements

• TauCeti.mongeAmpereMeasure_ite_mul_norm_sq_add — the Monge–Ampère measure of y ↦ (a / 2) ‖y‖² + c on an open convex set is aⁿ μ;

• TauCeti.mongeAmpereMeasure_ite_convexSection_add_linearMap — subtracting a plane from u on a section S restricts the Monge–Ampère measure of u to S;

• TauCeti.exists_ofReal_neg_pow_le_mul_ofReal_mul_measure_mul_mongeAmpereMeasure — the depth bound (max 0 (-v x₀)) ^ n ≤ C d μ(G) MA_v(G) when d bounds the distance to the boundary in every normalized position;

• TauCeti.exists_ofReal_neg_pow_le_mul_measure_mul_mongeAmpereMeasure — the depth bound (max 0 (-v x₀)) ^ n ≤ C μ(G) MA_v(G);

• TauCeti.exists_mul_measure_sq_le_mul_ofReal_pow — the volume bound λ μ(G)² ≤ C hⁿ;

• TauCeti.exists_ofReal_pow_le_mul_measure_convexSection_mul_mongeAmpereMeasure and TauCeti.exists_mul_measure_convexSection_sq_le_mul_ofReal_pow — the corresponding lower and upper volume estimates hⁿ ≤ C μ(S) MA_u(S) and λ μ(S)² ≤ C hⁿ for sections.

• TauCeti.abs_sub_le_on_convexSection_of_smul_le_mongeAmpereMeasure_le_smul — a quantitative comparison on a section with a given zero-boundary reference.

References

• L. A. Caffarelli, A localization property of viscosity solutions to the Monge–Ampère equation and their strict convexity, Ann. of Math. 131 (1990), 129–134.
• C. E. Gutiérrez, The Monge–Ampère Equation, 2nd ed., Progress in Nonlinear Differential Equations and Their Applications 89, Birkhäuser, 2016, §3.2.
• A. Figalli, The Monge–Ampère Equation and Its Applications, Zurich Lectures in Advanced Mathematics, EMS, 2017, Chapter 4.

theorem TauCeti.mongeAmpereMeasure_ite_mul_norm_sq_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {U : Set E} [DecidablePred fun (x : E) => x ∈ U] (hU : IsOpen U) (hUc : Convex ℝ U) {a : ℝ} (ha : 0 ≤ a) (c : ℝ) : (mongeAmpereMeasure μ fun (y : E) => if y ∈ U then ↑(a / 2 * ‖y‖ ^ 2 + c) else ⊤) = ENNReal.ofReal (a ^ Module.finrank ℝ E) • μ.restrict U

The Monge–Ampère measure of a quadratic. For a ≥ 0, the function y ↦ (a / 2) ‖y‖² + c on an open convex set U, extended by ⊤ off U, has Monge–Ampère measure aⁿ μ on U with respect to an additive Haar measure μ, where n = finrank ℝ E: its gradient is y ↦ a • y.

theorem TauCeti.mongeAmpereMeasure_ite_const {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] {U : Set E} [DecidablePred fun (x : E) => x ∈ U] (hU : IsOpen U) (hUc : Convex ℝ U) (c : ℝ) : (mongeAmpereMeasure μ fun (y : E) => if y ∈ U then ↑c else ⊤) = 0

On a positive-dimensional space, a constant potential on an open convex set, extended by ⊤ outside it, has zero Monge–Ampère measure.

theorem TauCeti.mongeAmpereMeasure_ite_convexSection_add_linearMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {Ω : Set E} [DecidablePred fun (x : E) => x ∈ Ω] {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} [DecidablePred fun (x_1 : E) => x_1 ∈ convexSection Ω u x ℓ h] (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) (L : E →ₗ[ℝ] ℝ) (c : ℝ) : (mongeAmpereMeasure μ fun (y : E) => if y ∈ convexSection Ω u x ℓ h then ↑(u y + L y + c) else ⊤) = (mongeAmpereMeasure μ fun (y : E) => if y ∈ Ω then ↑(u y) else ⊤).restrict (convexSection Ω u x ℓ h)

Subtracting a plane on a section. Let u be convex on an open set Ω, and let S = {y ∈ Ω | u y < u x + ℓ (y - x) + h}. The Monge–Ampère measure of u + L + c, extended by ⊤ off S, is the restriction to S of the Monge–Ampère measure of u extended by ⊤ off Ω. With L = -ℓ and c = ℓ x - u x - h this is the potential u - u x - ℓ (· - x) - h, which vanishes on the frontier of S.

theorem TauCeti.smul_restrict_le_mongeAmpereMeasure_ite_convexSection_add_linearMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {Ω : Set E} [DecidablePred fun (x : E) => x ∈ Ω] {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} [DecidablePred fun (x_1 : E) => x_1 ∈ convexSection Ω u x ℓ h] (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) (L : E →ₗ[ℝ] ℝ) (c : ℝ) {a : ENNReal} (hMA : a • μ.restrict Ω ≤ mongeAmpereMeasure μ fun (y : E) => if y ∈ Ω then ↑(u y) else ⊤) : a • μ.restrict (convexSection Ω u x ℓ h) ≤ mongeAmpereMeasure μ fun (y : E) => if y ∈ convexSection Ω u x ℓ h then ↑(u y + L y + c) else ⊤

A lower bound a μ ≤ MA_u on Ω gives the lower bound a μ ≤ MA_{u + L + c} on a section S of u, for the Monge–Ampère measures of u extended by ⊤ off Ω and of u + L + c extended by ⊤ off S.

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

Quantitative comparison on a section. Subtract the defining plane and height of a bounded section whose closure is in the original open domain. If the Monge–Ampère measure restricted to that section lies between (1 - ε)^n • ν and (1 + ε)^n • ν, the resulting zero-boundary potential differs from a zero-boundary reference v with measure ν by at most ε |v| on the section.

theorem TauCeti.exists_ofReal_neg_pow_le_mul_ofReal_mul_measure_mul_mongeAmpereMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] : ∃ (C : NNReal), ∀ (G : Set E) [inst : DecidablePred fun (x : E) => x ∈ G] (v : E → ℝ) (d : ℝ), IsOpen G → Bornology.IsBounded G → ConvexOn ℝ G v → ContinuousOn v (closure G) → (∀ x ∈ frontier G, 0 ≤ v x) → ∀ x₀ ∈ G, (∀ (T : E ≃ᵃ[ℝ] E), ⇑T '' G ⊆ Metric.ball 0 1 → Metric.infDist (T x₀) (⇑T '' G)ᶜ ≤ d) → ENNReal.ofReal (-v x₀) ^ Module.finrank ℝ E ≤ ↑C * ENNReal.ofReal d * μ G * (mongeAmpereMeasure μ fun (x : E) => if x ∈ G then ↑(v x) else ⊤) G

The depth of a convex function is controlled by its distance to the boundary, volume and Monge–Ampère mass. There is a constant C, depending only on E and μ, with the following property. Let G be a bounded open set, v convex on G, continuous on its closure and nonnegative on its frontier, and x₀ ∈ G. If d bounds the distance from T x₀ to the complement of T '' G for every affine equivalence T mapping G into the unit ball, then (max 0 (-v x₀)) ^ n ≤ C d μ(G) MA_v(G) for the Monge–Ampère measure of v extended by ⊤ off G, where n = finrank ℝ E. Both the hypothesis and the conclusion are invariant under affine changes of coordinates.

theorem TauCeti.exists_ofReal_neg_pow_le_mul_measure_mul_mongeAmpereMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] : ∃ (C : NNReal), ∀ (G : Set E) [inst : DecidablePred fun (x : E) => x ∈ G] (v : E → ℝ), IsOpen G → Bornology.IsBounded G → ConvexOn ℝ G v → ContinuousOn v (closure G) → (∀ x ∈ frontier G, 0 ≤ v x) → ∀ x₀ ∈ G, ENNReal.ofReal (-v x₀) ^ Module.finrank ℝ E ≤ ↑C * μ G * (mongeAmpereMeasure μ fun (x : E) => if x ∈ G then ↑(v x) else ⊤) G

The depth of a convex function is controlled by its volume and Monge–Ampère mass. There is a constant C, depending only on E and μ, such that for every bounded open set G, every v convex on G, continuous on its closure and nonnegative on its frontier, and every x₀ ∈ G, (max 0 (-v x₀)) ^ n ≤ C μ(G) MA_v(G) for the Monge–Ampère measure of v extended by ⊤ off G, where n = finrank ℝ E. Unlike the Aleksandrov maximum principle it involves no diameter or distance, so it is invariant under affine changes of coordinates.

theorem TauCeti.exists_mul_measure_sq_le_mul_ofReal_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] : ∃ (C : NNReal), ∀ (G : Set E) [inst : DecidablePred fun (x : E) => x ∈ G] (v : E → ℝ) (lam : NNReal) (h : ℝ), IsOpen G → Bornology.IsBounded G → ConvexOn ℝ G v → ContinuousOn v (closure G) → (∀ x ∈ frontier G, v x ≤ 0) → (∀ x ∈ G, -h ≤ v x) → (↑lam • μ.restrict G ≤ mongeAmpereMeasure μ fun (x : E) => if x ∈ G then ↑(v x) else ⊤) → ↑lam * μ G ^ 2 ≤ ↑C * ENNReal.ofReal h ^ Module.finrank ℝ E

The volume of a domain is controlled by the depth of a convex function on it. There is a constant C, depending only on E and μ, with the following property. Let G be a bounded open set and v convex on G, continuous on its closure, with v ≤ 0 on the frontier of G and v ≥ -h on G. If the Monge–Ampère measure of v (extended by ⊤ off G) is at least λ μ on G, then λ μ(G)² ≤ C hⁿ, where n = finrank ℝ E.

Sections

theorem TauCeti.exists_ofReal_pow_le_mul_measure_convexSection_mul_mongeAmpereMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] : ∃ (C : NNReal), ∀ (Ω : Set E) [inst : DecidablePred fun (x : E) => x ∈ Ω] (u : E → ℝ) (x : E) (ℓ : E →ₗ[ℝ] ℝ) (h : ℝ), IsOpen Ω → ConvexOn ℝ Ω u → x ∈ Ω → Bornology.IsBounded (convexSection Ω u x ℓ h) → closure (convexSection Ω u x ℓ h) ⊆ Ω → ENNReal.ofReal h ^ Module.finrank ℝ E ≤ ↑C * μ (convexSection Ω u x ℓ h) * (mongeAmpereMeasure μ fun (y : E) => if y ∈ Ω then ↑(u y) else ⊤) (convexSection Ω u x ℓ h)

Lower volume estimate for sections. There is a constant C, depending only on E and μ, with the following property. Let u be convex on an open set Ω, let x ∈ Ω, and let S = {y ∈ Ω | u y < u x + ℓ (y - x) + h} be a bounded section whose closure lies in Ω. Then hⁿ ≤ C μ(S) MA_u(S) for the Monge–Ampère measure of u extended by ⊤ off Ω, where n = finrank ℝ E. In particular, if MA_u ≤ Λ μ on Ω, then hⁿ ≤ C Λ μ(S)².

theorem TauCeti.exists_mul_measure_convexSection_sq_le_mul_ofReal_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] : ∃ (C : NNReal), ∀ (Ω : Set E) [inst : DecidablePred fun (x : E) => x ∈ Ω] (u : E → ℝ) (x : E) (ℓ : E →ₗ[ℝ] ℝ) (h : ℝ) (lam : NNReal), IsOpen Ω → ConvexOn ℝ Ω u → (∀ y ∈ Ω, u x + (ℓ y - ℓ x) ≤ u y) → Bornology.IsBounded (convexSection Ω u x ℓ h) → closure (convexSection Ω u x ℓ h) ⊆ Ω → (↑lam • μ.restrict Ω ≤ mongeAmpereMeasure μ fun (y : E) => if y ∈ Ω then ↑(u y) else ⊤) → ↑lam * μ (convexSection Ω u x ℓ h) ^ 2 ≤ ↑C * ENNReal.ofReal h ^ Module.finrank ℝ E

Upper volume estimate for sections. There is a constant C, depending only on E and μ, with the following property. Let u be convex on an open set Ω, let ℓ be a supporting slope of u at x, and let S = {y ∈ Ω | u y < u x + ℓ (y - x) + h} be a bounded section whose closure lies in Ω. If the Monge–Ampère measure of u (extended by ⊤ off Ω) is at least λ μ on Ω, then λ μ(S)² ≤ C hⁿ, where n = finrank ℝ E.