The Monge–Ampère measure of a cone

Let E be a finite-dimensional real inner product space, a : E and 0 ≤ r, and let μ be a measure on E absolutely continuous with respect to a Haar measure. In positive dimension, the cone u x = r * ‖x - a‖ with vertex a and slope r is the basic example of a convex function whose Aleksandrov Monge–Ampère measure is singular: all of its mass sits at the vertex,

MA_u = μ (closedBall 0 r) • δ_a

(TauCeti.mongeAmpereMeasure_mul_norm_sub; this formula holds in every dimension). The subdifferential of the cone at x is the set of y with ‖y‖ ≤ r and ⟪x - a, y⟫ = r * ‖x - a‖ (TauCeti.mem_subdifferential_mul_norm_sub_iff). At the vertex this is the whole closed ball of radius r, while at every other point it is the single gradient (r / ‖x - a‖) • (x - a), which lies on the sphere of radius r. In positive dimension spheres are null for a Haar measure, so only the vertex carries mass.

The cone is also the standard example showing that the pointwise Hessian determinant does not determine the Aleksandrov measure. The cone is twice differentiable away from its vertex, and there its Hessian has determinant 0, because the gradient is constant along each ray from a (TauCeti.det_fderiv_gradient_mul_norm_sub_eq_zero). In positive dimension and for a Haar measure μ, this gives det D²u = 0 almost everywhere, yet for r > 0 the Aleksandrov measure is not det (D²u) dμ (TauCeti.mongeAmpereMeasure_mul_norm_sub_ne_withDensity_det): it is mutually singular with μ (TauCeti.mutuallySingular_mongeAmpereMeasure_mul_norm_sub). So an identity det D²u = f almost everywhere is strictly weaker than MA_u = f dμ.

Main statements

• TauCeti.mem_subdifferential_mul_norm_sub_iff — the subdifferential of the cone;
• TauCeti.subdifferential_mul_norm_sub_self and TauCeti.subdifferential_mul_norm_sub_of_ne — it is the closed ball of radius r at the vertex and the gradient elsewhere;
• TauCeti.mongeAmpereMeasure_mul_norm_sub — for μ absolutely continuous with respect to a Haar measure, the Monge–Ampère measure of the cone is μ (closedBall 0 r) • δ_a;
• TauCeti.mutuallySingular_mongeAmpereMeasure_mul_norm_sub — in positive dimension this measure is mutually singular with μ;
• TauCeti.differentiableAt_gradient_mul_norm_sub and TauCeti.det_fderiv_gradient_mul_norm_sub_eq_zero — away from the vertex the cone is twice differentiable and its Hessian has determinant 0;
• TauCeti.mongeAmpereMeasure_mul_norm_sub_ne_withDensity_det — in positive dimension, for a Haar measure μ and r > 0, the Monge–Ampère measure of the cone is not det (D²u) dμ.

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.1.
• A. Figalli, The Monge–Ampère Equation and Its Applications, Zurich Lectures in Advanced Mathematics, EMS, 2017, §2.1.

theorem TauCeti.mem_subdifferential_mul_norm_sub_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r : ℝ} {a x y : E} (hr : 0 ≤ r) : y ∈ subdifferential (innerₗ E) (fun (x : E) => ↑(r * ‖x - a‖)) x ↔ ‖y‖ ≤ r ∧ inner ℝ (x - a) y = r * ‖x - a‖

The subdifferential of a cone. For 0 ≤ r, y is a subgradient of x ↦ r * ‖x - a‖ at x exactly when ‖y‖ ≤ r and ⟪x - a, y⟫ = r * ‖x - a‖.

theorem TauCeti.subdifferential_mul_norm_sub_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) (a : E) : subdifferential (innerₗ E) (fun (x : E) => ↑(r * ‖x - a‖)) a = Metric.closedBall 0 r

At its vertex, the subdifferential of the cone x ↦ r * ‖x - a‖ is the closed ball of radius r.

theorem TauCeti.subdifferential_mul_norm_sub_of_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r : ℝ} {a x : E} (hr : 0 ≤ r) (hx : x ≠ a) : subdifferential (innerₗ E) (fun (x : E) => ↑(r * ‖x - a‖)) x = {(r / ‖x - a‖) • (x - a)}

Away from its vertex, the subdifferential of the cone x ↦ r * ‖x - a‖ is the single point (r / ‖x - a‖) • (x - a).

theorem TauCeti.norm_eq_of_mem_subdifferential_mul_norm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r : ℝ} {a x y : E} (hr : 0 ≤ r) (hx : x ≠ a) (hy : y ∈ subdifferential (innerₗ E) (fun (x : E) => ↑(r * ‖x - a‖)) x) : ‖y‖ = r

Every subgradient of the cone x ↦ r * ‖x - a‖ away from its vertex has norm r.

theorem TauCeti.hasGradientAt_mul_norm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a x : E} [CompleteSpace E] (r : ℝ) (hx : x ≠ a) : HasGradientAt (fun (x : E) => r * ‖x - a‖) ((r / ‖x - a‖) • (x - a)) x

Away from its vertex, the cone x ↦ r * ‖x - a‖ has gradient (r / ‖x - a‖) • (x - a).

@[simp]

theorem TauCeti.gradient_mul_norm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a x : E} [CompleteSpace E] (r : ℝ) (hx : x ≠ a) : gradient (fun (x : E) => r * ‖x - a‖) x = (r / ‖x - a‖) • (x - a)

Away from its vertex, the gradient of the cone x ↦ r * ‖x - a‖ is (r / ‖x - a‖) • (x - a).

theorem TauCeti.differentiableAt_gradient_mul_norm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a x : E} [CompleteSpace E] (r : ℝ) (hx : x ≠ a) : DifferentiableAt ℝ (gradient fun (x : E) => r * ‖x - a‖) x

Away from its vertex, the gradient of the cone x ↦ r * ‖x - a‖ is differentiable: the cone is twice differentiable there.

@[simp]

theorem TauCeti.fderiv_gradient_mul_norm_sub_apply_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a x : E} [CompleteSpace E] (r : ℝ) (hx : x ≠ a) : (fderiv ℝ (gradient fun (x : E) => r * ‖x - a‖) x) (x - a) = 0

The gradient of the cone x ↦ r * ‖x - a‖ is constant along each open ray from the vertex a, so away from a its derivative vanishes in the radial direction x - a.

@[simp]

theorem TauCeti.det_fderiv_gradient_mul_norm_sub_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a x : E} [CompleteSpace E] [FiniteDimensional ℝ E] (r : ℝ) (hx : x ≠ a) : (fderiv ℝ (gradient fun (x : E) => r * ‖x - a‖) x).det = 0

The Hessian of a cone is degenerate. Away from its vertex a, the Hessian of the cone x ↦ r * ‖x - a‖ has determinant 0, since it annihilates the radial direction x - a.

theorem TauCeti.mongeAmpereMeasure_mul_norm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r : ℝ} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ ν : MeasureTheory.Measure E} [ν.IsAddHaarMeasure] (hμ : μ.AbsolutelyContinuous ν) (hr : 0 ≤ r) (a : E) : (mongeAmpereMeasure μ fun (x : E) => ↑(r * ‖x - a‖)) = μ (Metric.closedBall 0 r) • MeasureTheory.Measure.dirac a

The Monge–Ampère measure of a cone. For 0 ≤ r and a measure μ absolutely continuous with respect to a Haar measure, the Aleksandrov Monge–Ampère measure of the cone x ↦ r * ‖x - a‖ is the point mass μ (closedBall 0 r) • δ_a at its vertex.

theorem TauCeti.mutuallySingular_mongeAmpereMeasure_mul_norm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r : ℝ} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ ν : MeasureTheory.Measure E} [ν.IsAddHaarMeasure] [Nontrivial E] (hμ : μ.AbsolutelyContinuous ν) (hr : 0 ≤ r) (a : E) : (mongeAmpereMeasure μ fun (x : E) => ↑(r * ‖x - a‖)).MutuallySingular μ

The Monge–Ampère measure of a cone is singular. In positive dimension, the Aleksandrov Monge–Ampère measure of the cone x ↦ r * ‖x - a‖, for 0 ≤ r, is mutually singular with every measure μ absolutely continuous with respect to a Haar measure.

theorem TauCeti.mongeAmpereMeasure_mul_norm_sub_ne_withDensity_det {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r : ℝ} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [Nontrivial E] (hr : 0 < r) (a : E) : (mongeAmpereMeasure μ fun (x : E) => ↑(r * ‖x - a‖)) ≠ μ.withDensity fun (x : E) => ENNReal.ofReal (fderiv ℝ (gradient fun (x : E) => r * ‖x - a‖) x).det

The Hessian determinant does not determine the Monge–Ampère measure. In positive dimension, for a Haar measure μ and 0 < r, the cone x ↦ r * ‖x - a‖ is twice differentiable off its vertex with Hessian determinant 0 there (TauCeti.det_fderiv_gradient_mul_norm_sub_eq_zero), yet its Aleksandrov Monge–Ampère measure is not det (D²u) dx.