The engulfing property of sections of Monge–Ampère solutions

Let E be a real inner product space of finite dimension n ≥ 1 with an additive Haar measure μ, and let u be convex on an open set Ω with λ μ ≤ MA_u ≤ Λ μ on Ω, where MA_u is the Aleksandrov Monge–Ampère measure of u and 0 < λ. Write S(x, h) = {y ∈ Ω | u y < u x + ℓ (y - x) + h} for the section of u at x with a supporting slope ℓ and height h. This file proves Caffarelli's engulfing property: there is a constant C, depending only on E and μ, such that whenever S(x, 2h) is bounded with closure inside Ω, every y ∈ S(x, h) and every supporting slope m of u at y satisfy

S(x, h) ⊆ S(y, θ h) with θ = 1 + C Λ / λ,

where S(y, θ h) is taken with the slope m. So every section centred at a point of S(x, h), of height θ h, swallows S(x, h). Together with the volume estimates for sections (TauCeti.exists_mul_measure_convexSection_sq_le_mul_ofReal_pow), this is the property that lets sections play the role of balls in Caffarelli's interior regularity theory.

The engulfing property rests on an affine invariant interior estimate (TauCeti.exists_add_smul_sub_mem_of_mongeAmpereMeasure_le). Let v be convex on a bounded open set G, continuous on its closure, vanishing on its frontier and bounded below by -k, with λ μ ≤ MA_v on G and MA_v(G) ≤ Λ μ(G). If v y ≤ -h and z ∈ G, then G contains the points y + t (y - z) for every t ≥ 0 with C Λ kⁿ t < λ hⁿ: a point where v is deep is uniformly far from the boundary of G, measured along chords. In a position normalized by an affine equivalence (TauCeti.exists_affineEquiv_ball_subset_image_subset_ball), the point y is within 2 t of the boundary if y + t (y - z) leaves G (TauCeti.infDist_image_compl_le_of_add_smul_sub_notMem). The depth bound (TauCeti.exists_ofReal_neg_pow_le_mul_ofReal_mul_measure_mul_mongeAmpereMeasure) then bounds hⁿ by t times the volume and the Monge–Ampère mass, and the volume estimate bounds their product in terms of kⁿ.

For the engulfing property apply this to v = u - u x - ℓ (· - x) - 2h on G = S(x, 2h), with k = 2h, at y ∈ S(x, h), where v y < -h. For z ∈ S(x, h) the point w = y + t (y - z) lies in G for a fixed t comparable to λ / Λ, and the supporting plane at y with slope m lies below u w < u x + ℓ (w - x) + 2h. Along the line through z, y and w this bounds m (y - z) from above, which is the inequality u z < u y + m (z - y) + θ h.

Main statements

• TauCeti.infDist_image_compl_le_of_add_smul_sub_notMem — distance to the boundary along a chord, in normalized position;
• TauCeti.exists_add_smul_sub_mem_of_mongeAmpereMeasure_le — the interior estimate along chords;
• TauCeti.exists_convexSection_subset_convexSection — the engulfing property of sections.

References

• L. A. Caffarelli, Some regularity properties of solutions of Monge Ampère equation, Comm. Pure Appl. Math. 44 (1991), 965–969.
• C. E. Gutiérrez, The Monge–Ampère Equation, 2nd ed., Progress in Nonlinear Differential Equations and Their Applications 89, Birkhäuser, 2016, §3.3 (the engulfing property).
• A. Figalli, The Monge–Ampère Equation and Its Applications, Zurich Lectures in Advanced Mathematics, EMS, 2017, Chapter 4.

theorem TauCeti.infDist_image_compl_le_of_add_smul_sub_notMem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Set E} (T : E ≃ᵃ[ℝ] E) (hT : ⇑T '' G ⊆ Metric.ball 0 1) {y z : E} (hy : y ∈ G) (hz : z ∈ G) {t : ℝ} (ht : 0 ≤ t) (hw : y + t • (y - z) ∉ G) : Metric.infDist (T y) (⇑T '' G)ᶜ ≤ 2 * t

Distance to the boundary along a chord, in normalized position. Let T be an affine equivalence mapping G into the unit ball. If y, z ∈ G and the point y + t (y - z), with t ≥ 0, lies outside G, then T y is within 2 t of the complement of T '' G.

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

Deep points are far from the boundary along chords. 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, vanishing on its frontier and bounded below by -k on G, such that the Monge–Ampère measure of v (extended by ⊤ off G) is at least λ μ on G and has mass MA_v(G) ≤ Λ μ(G). If y, z ∈ G and v y ≤ -h with 0 ≤ h, then y + t (y - z) ∈ G for every t ≥ 0 with C Λ kⁿ t < λ hⁿ, where n = finrank ℝ E.

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

The engulfing property of sections. There is a constant C, depending only on E and μ, with the following property. Let u be convex on an open set Ω, with λ μ ≤ MA_u ≤ Λ μ on Ω for the Monge–Ampère measure of u extended by ⊤ off Ω and 0 < λ, let ℓ be a supporting slope of u at x, and let the section S(x, 2h) be bounded with closure inside Ω. Then for every y ∈ S(x, h) and every supporting slope m of u at y, the section S(x, h) is contained in the section of u at y with slope m and height (1 + C Λ / λ) h.