Sections of convex functions

A section of a real function u on Ω, centered at x with slope ℓ and height h, is the set of y ∈ Ω with u y < u x + ℓ (y - x) + h. In an inner product space, taking ℓ y = ⟪p, y⟫ gives the usual section with subgradient p; at a differentiability point one takes ℓ = fderiv ℝ u x. Keeping the slope as a linear functional allows changes of coordinates without choosing an inner product.

These sets are the domains on which local Monge–Ampère estimates are normalized. We prove convexity, openness, height nesting, contraction about the center, and invariance under adding affine functions. A continuous potential takes the boundary value of the section on its frontier, and a chord leaving a point of a section through a second point gives an inclusion into a section at that second point, which is the step behind the engulfing property of sections. Positive rescaling and linear coordinate changes give the exact unit-height normalization identity. A supporting slope is required for the nonpositive-height emptiness statement, but not for convexity or the normalization identities.

The function is real-valued on its specified domain; no extension outside the domain is used. For an extended-real convex potential one can take its real representative on the interior of its effective domain.

References

• C. E. Gutiérrez, The Monge–Ampère Equation, 2nd ed., Birkhäuser, 2016, §1.8.
• A. Figalli, The Monge–Ampère Equation and Its Applications, EMS, 2017, Chapter 3.

def TauCeti.convexSection {E : Type u_1} [AddCommGroup E] [Module ℝ E] (Ω : Set E) (u : E → ℝ) (x : E) (ℓ : E →ₗ[ℝ] ℝ) (h : ℝ) : Set E

The section of u on Ω at x, with slope ℓ and strict height h.

@[simp]

theorem TauCeti.mem_convexSection_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x y : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} : y ∈ convexSection Ω u x ℓ h ↔ y ∈ Ω ∧ u y < u x + ℓ (y - x) + h

Membership in a section is membership in the domain and the strict supporting-plane bound.

theorem TauCeti.convexSection_subset {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} : convexSection Ω u x ℓ h ⊆ Ω

A section is contained in its domain.

theorem TauCeti.convexSection_eq_sep_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} : convexSection Ω u x ℓ h = {y : E | y ∈ Ω ∧ (u - ⇑ℓ) y < u x - ℓ x + h}

A section is the strict sublevel set of the potential minus the slope on its domain.

theorem TauCeti.convexSection_mono_height {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h k : ℝ} (hhk : h ≤ k) : convexSection Ω u x ℓ h ⊆ convexSection Ω u x ℓ k

Increasing the height enlarges a section.

theorem TauCeti.convex_convexSection {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (hu : ConvexOn ℝ Ω u) : Convex ℝ (convexSection Ω u x ℓ h)

A section of a convex function is convex, even when the slope is not supporting.

theorem TauCeti.convexOn_convexSection_add_linearMap {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (hu : ConvexOn ℝ Ω u) (L : E →ₗ[ℝ] ℝ) (c : ℝ) : ConvexOn ℝ (convexSection Ω u x ℓ h) fun (y : E) => u y + L y + c

On a section of a convex function, adding a linear function and a constant to the potential keeps it convex. With L = -ℓ this subtracts the plane of the section from the potential.

theorem TauCeti.pos_of_mem_convexSection {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x y : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (hℓy : u x + (ℓ y - ℓ x) ≤ u y) (hy : y ∈ convexSection Ω u x ℓ h) : 0 < h

If u y lies above the plane through (x, u x) with slope ℓ (the supporting plane at x), then a section convexSection Ω u x ℓ h containing y has positive height h.

theorem TauCeti.convexSection_nonempty_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (hx : x ∈ Ω) (hℓ : ∀ y ∈ Ω, u x + (ℓ y - ℓ x) ≤ u y) : (convexSection Ω u x ℓ h).Nonempty ↔ 0 < h

A supporting slope gives a nonempty section exactly at positive heights.

theorem TauCeti.convexSection_eq_empty_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (hx : x ∈ Ω) (hℓ : ∀ y ∈ Ω, u x + (ℓ y - ℓ x) ≤ u y) : convexSection Ω u x ℓ h = ∅ ↔ h ≤ 0

At a supporting slope, precisely the nonpositive heights give an empty section.

theorem TauCeti.smul_sub_add_mem_convexSection {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x y : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (hu : ConvexOn ℝ Ω u) (hx : x ∈ Ω) (hy : y ∈ convexSection Ω u x ℓ h) {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) : t • (y - x) + x ∈ convexSection Ω u x ℓ (t * h)

Contracting a section by a positive factor at most one about its center contracts its height by the same factor. This uses convexity and does not require a supporting slope.

theorem TauCeti.mem_convexSection_of_add_smul_sub_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x y : E} {ℓ : E →ₗ[ℝ] ℝ} {h k : ℝ} {m : E →ₗ[ℝ] ℝ} {z : E} {t : ℝ} (hℓy : u x + (ℓ y - ℓ x) ≤ u y) (hm : ∀ p ∈ Ω, u y + (m p - m y) ≤ u p) (hz : z ∈ convexSection Ω u x ℓ h) (ht : 0 < t) (hw : y + t • (y - z) ∈ convexSection Ω u x ℓ k) : z ∈ convexSection Ω u y m (h + k / t)

Engulfing along a chord. Let m be a supporting slope at y, and let y lie above the plane through x with slope ℓ. If z ∈ S(x, h) and the chord from z through y, extended beyond y by t > 0 times its length, ends in S(x, k), then z lies in the section at y with slope m and height h + k / t. No convexity is needed: the supporting plane at y lies below the potential at the end of the chord.

@[simp]

theorem TauCeti.convexSection_add_affine {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (L : E →ₗ[ℝ] ℝ) (c : ℝ) : convexSection Ω (fun (y : E) => u y + L y + c) x (ℓ + L) h = convexSection Ω u x ℓ h

Adding an affine function to the potential and its linear part to the slope preserves every section.

theorem TauCeti.convexSection_mul_pos {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h a : ℝ} (ha : 0 < a) : convexSection Ω (fun (y : E) => a * u y) x (a • ℓ) (a * h) = convexSection Ω u x ℓ h

Positive rescaling of the potential, slope and height preserves a section.

theorem TauCeti.convexSection_comp_linearMap {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {Ω : Set E} {u : E → ℝ} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (A : F →ₗ[ℝ] E) (z : F) : convexSection (⇑A ⁻¹' Ω) (u ∘ ⇑A) z (ℓ ∘ₗ A) h = ⇑A ⁻¹' convexSection Ω u (A z) ℓ h

Pulling back the domain, potential and slope by a linear map pulls back the section. The map need not be injective or surjective.

theorem TauCeti.convexSection_comp_add {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (a : E) : convexSection ((fun (y : E) => y + a) ⁻¹' Ω) (fun (y : E) => u (y + a)) x ℓ h = (fun (y : E) => y + a) ⁻¹' convexSection Ω u (x + a) ℓ h

Translating coordinates translates the center and the domain of a section.

theorem TauCeti.convexSection_normalize {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} (A : F →ₗ[ℝ] E) (hh : 0 < h) : convexSection ((fun (z : F) => x + A z) ⁻¹' Ω) (fun (z : F) => (u (x + A z) - u x - ℓ (A z)) / h) 0 0 1 = (fun (z : F) => x + A z) ⁻¹' convexSection Ω u x ℓ h

Subtracting the supporting plane, dividing by the positive height, and using coordinates y = x + A z turns a section into a section centered at zero, with zero slope and height one. For a linear equivalence this is the section normalization used in local estimates.

theorem TauCeti.isOpen_convexSection {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} [TopologicalSpace E] (hΩ : IsOpen Ω) (hu : ContinuousOn u Ω) (hℓ : Continuous ⇑ℓ) : IsOpen (convexSection Ω u x ℓ h)

Sections of a continuous potential on an open domain are open when the slope is continuous. Convexity is not needed for this assertion.

theorem TauCeti.closure_convexSection_inter_subset {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h k : ℝ} [TopologicalSpace E] (hu : ContinuousOn u Ω) (hℓ : Continuous ⇑ℓ) (hhk : h < k) : closure (convexSection Ω u x ℓ h) ∩ Ω ⊆ convexSection Ω u x ℓ k

Within the domain, the closure of a section lies in every section of strictly larger height. Continuity is needed only on the domain, which need not be closed.

theorem TauCeti.continuousOn_closure_convexSection_add_linearMap {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} [TopologicalSpace E] (hu : ContinuousOn u Ω) {L : E →ₗ[ℝ] ℝ} (hL : Continuous ⇑L) (hS : closure (convexSection Ω u x ℓ h) ⊆ Ω) (c : ℝ) : ContinuousOn (fun (y : E) => u y + L y + c) (closure (convexSection Ω u x ℓ h))

If the closure of a section lies in the domain of a continuous potential, then adding a continuous linear function and a constant to the potential keeps it continuous on that closure.

theorem TauCeti.eq_of_mem_frontier_convexSection {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x y : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} [TopologicalSpace E] (hΩ : IsOpen Ω) (hu : ContinuousOn u Ω) (hℓ : Continuous ⇑ℓ) (hS : closure (convexSection Ω u x ℓ h) ⊆ Ω) (hy : y ∈ frontier (convexSection Ω u x ℓ h)) : u y = u x + ℓ (y - x) + h

If the closure of a section lies in the open domain of a continuous potential, then on the frontier of the section the potential equals the plane through (x, u x) with slope ℓ, raised by the height.

theorem TauCeti.isBounded_convexSection_and_closure_subset_of_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {Ω : Set E} {u : E → ℝ} {x : E} {ℓ : E →ₗ[ℝ] ℝ} {h : ℝ} [TopologicalSpace E] [Bornology E] {H : ℝ} (hhH : h ≤ H) (hH : Bornology.IsBounded (convexSection Ω u x ℓ H) ∧ closure (convexSection Ω u x ℓ H) ⊆ Ω) : Bornology.IsBounded (convexSection Ω u x ℓ h) ∧ closure (convexSection Ω u x ℓ h) ⊆ Ω

A section of height at most H lies in the section of height H, so it inherits its boundedness and the inclusion of its closure in the domain.