The Hopf–Lax formula and its subsolution inequality

For a Lagrangian L : E → ℝ and an initial datum φ : E → ℝ on a real vector space, the Hopf–Lax formula

u (t, x) = inf_y (φ y + t L ((x - y) / t))

defines, for t > 0, the value function of the control problem with running cost L and initial cost φ. For convex L it is the candidate solution of the Hamilton–Jacobi equation ∂ₜ u + H (∇ₓ u) = 0 with H the convex conjugate of L. This file proves the inequality that makes u a subsolution of that equation without any differentiability:

u (t + h, x + h w) ≤ u (t, x) + h L w for t > 0, h ≥ 0 and every velocity w.

It is the statement that moving at velocity w for time h costs at most h L w. At a point where u is differentiable it gives ∂ₜ u + ⟨∇ₓ u, w⟩ ≤ L w for every w, that is ∂ₜ u + H (∇ₓ u) ≤ 0, and the inequality survives averaging u against a probability kernel in space-time. This is the form in which Hopf–Lax functions are tested against solutions of the continuity equation to bound transport costs by the kinetic action, as in the lower bound of the Benamou–Brenier formula for the cost L w = ‖w‖ ^ p.

The infimum is taken in ℝ, so the results assume φ and L bounded below, which makes it finite for t ≥ 0. At t = 0 the formula degenerates to the infimum of φ; the Hopf–Lax function recovers φ as a limit t → 0⁺ only under additional hypotheses. That limit, and times t ≤ 0, are not studied here.

Main definitions

• TauCeti.hopfLax L φ t x: the Hopf–Lax value inf_y (φ y + t L (t⁻¹ (x - y))).

Main results

• TauCeti.hopfLax_le and TauCeti.le_hopfLax_iff: the Hopf–Lax value is the greatest lower bound of the penalized values.
• TauCeti.hopfLax_mono: the Hopf–Lax value is monotone in the Lagrangian and initial datum.
• TauCeti.hopfLax_le_add_mul and TauCeti.add_mul_le_hopfLax: the bounds m + t l ≤ u (t, x) ≤ φ x + t L 0 for lower bounds m of φ and l of L.
• TauCeti.hopfLax_add_add_smul_le: the subsolution inequality u (t + h, x + h w) ≤ u (t, x) + h L w for convex L.
• TauCeti.antitoneOn_hopfLax: for convex L with L 0 ≤ 0, u (t, x) decreases in t > 0.
• TauCeti.upperSemicontinuousOn_hopfLax: for continuous L, u is jointly upper semicontinuous on the open half-space t > 0.
• TauCeti.hopfLax_norm_rpow and TauCeti.hopfLax_norm_rpow_add_add_smul_le: for the cost L w = ‖w‖ ^ p, the formula reads u (t, x) = inf_y (φ y + ‖x - y‖ ^ p / t ^ (p - 1)), and the subsolution inequality holds in real seminormed spaces for 1 ≤ p.
• TauCeti.le_hopfLax_norm_rpow_neg_div: for this cost, a feasible pair φ ⊕ ψ gives ψ / κ ≤ u for the Hopf–Lax value u of -φ / κ.
• TauCeti.hopfLax_norm_rpow_le_self: for this cost, u at a time t ≥ 0 lies below φ.
• TauCeti.abs_hopfLax_norm_rpow_le: for this cost, u stays within the bounds of φ.
• TauCeti.lowerSemicontinuousOn_hopfLax_norm_rpow and TauCeti.continuousOn_hopfLax_norm_rpow: in a proper space, for 1 ≤ p, u is lower semicontinuous on t > 0 when φ is lower semicontinuous and bounded below, and continuous there when φ is continuous and bounded below.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, American Mathematical Society 2010, §3.3.2, on the Hopf–Lax formula.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 7.

noncomputable def TauCeti.hopfLax {E : Type u_1} [AddCommGroup E] [Module ℝ E] (L φ : E → ℝ) (t : ℝ) (x : E) : ℝ

The Hopf–Lax value inf_y (φ y + t L (t⁻¹ (x - y))) of the initial datum φ for the Lagrangian L at time t and position x. The infimum is taken in ℝ; it is the honest infimum when φ and L are bounded below and t ≥ 0.

theorem TauCeti.hopfLax_def {E : Type u_1} [AddCommGroup E] [Module ℝ E] (L φ : E → ℝ) (t : ℝ) (x : E) : hopfLax L φ t x = ⨅ (y : E), φ y + t * L (t⁻¹ • (x - y))

The defining formula of the Hopf–Lax value.

@[simp]

theorem TauCeti.hopfLax_one {E : Type u_1} [AddCommGroup E] [Module ℝ E] (L φ : E → ℝ) (x : E) : hopfLax L φ 1 x = ⨅ (y : E), φ y + L (x - y)

At time 1 the Hopf–Lax value is the infimal convolution inf_y (φ y + L (x - y)).

theorem TauCeti.hopfLax_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t : ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (ht : 0 ≤ t) (x y : E) : hopfLax L φ t x ≤ φ y + t * L (t⁻¹ • (x - y))

The Hopf–Lax value is at most the penalized value at any point y.

theorem TauCeti.le_hopfLax {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t c : ℝ} {x : E} (h : ∀ (y : E), c ≤ φ y + t * L (t⁻¹ • (x - y))) : c ≤ hopfLax L φ t x

A lower bound for every penalized value is a lower bound for the Hopf–Lax value.

theorem TauCeti.le_hopfLax_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t : ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (ht : 0 ≤ t) {c : ℝ} {x : E} : c ≤ hopfLax L φ t x ↔ ∀ (y : E), c ≤ φ y + t * L (t⁻¹ • (x - y))

The Hopf–Lax value is the greatest lower bound of the penalized values.

theorem TauCeti.hopfLax_le_add_mul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t : ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (ht : 0 ≤ t) (x : E) : hopfLax L φ t x ≤ φ x + t * L 0

The Hopf–Lax value lies below the initial datum plus the cost t L 0 of staying put.

theorem TauCeti.hopfLax_mono {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t : ℝ} {K ψ : E → ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (ht : 0 ≤ t) (hLK : L ≤ K) (hφψ : φ ≤ ψ) (x : E) : hopfLax L φ t x ≤ hopfLax K ψ t x

The Hopf–Lax value is monotone in the Lagrangian and initial datum at nonnegative times.

theorem TauCeti.add_mul_le_hopfLax {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t m l : ℝ} (hm : ∀ (y : E), m ≤ φ y) (hl : ∀ (w : E), l ≤ L w) (ht : 0 ≤ t) (x : E) : m + t * l ≤ hopfLax L φ t x

For lower bounds m of φ and l of L, the Hopf–Lax value at time t ≥ 0 is at least m + t l.

theorem TauCeti.hopfLax_add_add_smul_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t h : ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (hLc : ConvexOn ℝ Set.univ L) (ht : 0 < t) (hh : 0 ≤ h) (x w : E) : hopfLax L φ (t + h) (x + h • w) ≤ hopfLax L φ t x + h * L w

The Hopf–Lax subsolution inequality. For a convex Lagrangian L, moving from (t, x) at velocity w for time h ≥ 0 raises the Hopf–Lax value by at most h L w: u (t + h, x + h w) ≤ u (t, x) + h L w for t > 0.

theorem TauCeti.hopfLax_add_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} {t h : ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (hLc : ConvexOn ℝ Set.univ L) (ht : 0 < t) (hh : 0 ≤ h) (x : E) : hopfLax L φ (t + h) x ≤ hopfLax L φ t x + h * L 0

For a convex Lagrangian, the Hopf–Lax value grows by at most h L 0 from time t > 0 to time t + h.

theorem TauCeti.antitoneOn_hopfLax {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (hLc : ConvexOn ℝ Set.univ L) (hL0 : L 0 ≤ 0) (x : E) : AntitoneOn (fun (x_1 : ℝ) => hopfLax L φ x_1 x) (Set.Ioi 0)

For a convex Lagrangian with L 0 ≤ 0, the Hopf–Lax value at a fixed point decreases in time t > 0.

theorem TauCeti.upperSemicontinuousOn_hopfLax {E : Type u_1} [AddCommGroup E] [Module ℝ E] {L φ : E → ℝ} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L)) (hLc : Continuous L) : UpperSemicontinuousOn (fun (q : ℝ × E) => hopfLax L φ q.1 q.2) {q : ℝ × E | 0 < q.1}

For a continuous Lagrangian, the Hopf–Lax value is jointly upper semicontinuous in time and space on the open half-space t > 0, as an infimum of continuous functions. No regularity of φ is needed.

theorem TauCeti.hopfLax_norm_rpow {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {t p : ℝ} (φ : E → ℝ) (ht : 0 < t) (x : E) : hopfLax (fun (x : E) => ‖x‖ ^ p) φ t x = ⨅ (y : E), φ y + ‖x - y‖ ^ p / t ^ (p - 1)

For the cost L w = ‖w‖ ^ p, the Hopf–Lax value at time t > 0 is inf_y (φ y + ‖x - y‖ ^ p / t ^ (p - 1)).

theorem TauCeti.le_hopfLax_norm_rpow_neg_div {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {φ : E → ℝ} {t p : ℝ} {ψ : E → ℝ} (ht : 0 < t) (hφψ : ∀ (x y : E), φ x + ψ y ≤ ‖x - y‖ ^ p) (y : E) : ψ y / t ^ (p - 1) ≤ hopfLax (fun (x : E) => ‖x‖ ^ p) (fun (x : E) => -φ x / t ^ (p - 1)) t y

For the cost L w = ‖w‖ ^ p, if φ x + ψ y ≤ ‖x - y‖ ^ p for all x y, then at a time t > 0 the Hopf–Lax value of -φ / κ, with κ = t ^ (p - 1), lies above ψ / κ.

theorem TauCeti.hopfLax_norm_rpow_add_add_smul_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {φ : E → ℝ} {t h p : ℝ} (hp : 1 ≤ p) (hφ : BddBelow (Set.range φ)) (ht : 0 < t) (hh : 0 ≤ h) (x w : E) : hopfLax (fun (x : E) => ‖x‖ ^ p) φ (t + h) (x + h • w) ≤ hopfLax (fun (x : E) => ‖x‖ ^ p) φ t x + h * ‖w‖ ^ p

The Hopf–Lax subsolution inequality for the p-th power cost. In a real seminormed space, for 1 ≤ p and φ bounded below, u (t + h, x + h w) ≤ u (t, x) + h ‖w‖ ^ p for t > 0 and h ≥ 0.

theorem TauCeti.hopfLax_norm_rpow_le_self {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {φ : E → ℝ} {t p : ℝ} (hp : p ≠ 0) (hφ : BddBelow (Set.range φ)) (ht : 0 ≤ t) (x : E) : hopfLax (fun (x : E) => ‖x‖ ^ p) φ t x ≤ φ x

For the cost L w = ‖w‖ ^ p with p ≠ 0, the Hopf–Lax value at a time t ≥ 0 lies below the initial datum φ.

theorem TauCeti.abs_hopfLax_norm_rpow_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {φ : E → ℝ} {t p : ℝ} (hp : p ≠ 0) {C : ℝ} (hφC : ∀ (y : E), |φ y| ≤ C) (ht : 0 ≤ t) (x : E) : |hopfLax (fun (x : E) => ‖x‖ ^ p) φ t x| ≤ C

For the cost L w = ‖w‖ ^ p with p ≠ 0, the Hopf–Lax value at a time t ≥ 0 stays within any bound C of the initial datum: |φ| ≤ C gives |u (t, x)| ≤ C.

theorem TauCeti.lowerSemicontinuousOn_hopfLax_norm_rpow {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {φ : E → ℝ} {p : ℝ} [ProperSpace E] (hp : 1 ≤ p) (hφ : LowerSemicontinuous φ) (hφb : BddBelow (Set.range φ)) : LowerSemicontinuousOn (fun (q : ℝ × E) => hopfLax (fun (x : E) => ‖x‖ ^ p) φ q.1 q.2) {q : ℝ × E | 0 < q.1}

Lower semicontinuity of the Hopf–Lax value for the p-th power cost. In a proper real seminormed space, for 1 ≤ p and a lower semicontinuous initial datum φ bounded below, the Hopf–Lax value u (t, x) = inf_y (φ y + ‖x - y‖ ^ p / t ^ (p - 1)) is jointly lower semicontinuous on the open half-space t > 0.

theorem TauCeti.continuousOn_hopfLax_norm_rpow {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {φ : E → ℝ} {p : ℝ} [ProperSpace E] (hp : 1 ≤ p) (hφ : Continuous φ) (hφb : BddBelow (Set.range φ)) : ContinuousOn (fun (q : ℝ × E) => hopfLax (fun (x : E) => ‖x‖ ^ p) φ q.1 q.2) {q : ℝ × E | 0 < q.1}

Continuity of the Hopf–Lax value for the p-th power cost. In a proper real seminormed space, for 1 ≤ p and a continuous initial datum φ bounded below, the Hopf–Lax value u (t, x) = inf_y (φ y + ‖x - y‖ ^ p / t ^ (p - 1)) is jointly continuous on the open half-space t > 0.