The evolution variational inequality

Let φ : X → EReal be an energy on a metric space and λ : ℝ. A curve u : [0, ∞) → X is a solution of the evolution variational inequality EVI_λ if it is continuous, has finite energy at every positive time, and for every point y of the effective domain {y | φ y ≠ ⊤} and every time t > 0

(1/2) d⁺/dt d(u t, y)² + (λ/2) d(u t, y)² ≤ φ y - φ (u t),

where d⁺/dt is the upper right Dini derivative. This is one of the metric formulations of the gradient flow of φ, the one adapted to λ-convex energies: for a differentiable curve in a Hilbert space it reads ⟪u', u - y⟫ ≤ φ y - φ u - (λ/2) ‖u - y‖², the variational form of the subdifferential inclusion -u' ∈ ∂φ(u) for a λ-convex energy. For instance the flow t ↦ e⁻ᵗ x of ‖x‖² / 2 is an EVI_1 solution (TauCeti.isEVISolution_exp_neg_smul). Unlike curves of maximal slope, EVI_λ solutions are λ-contracting, which makes them unique.

For a lower semicontinuous energy, the results below are the basic structural properties of an EVI_λ solution u:

• the energy t ↦ φ (u t) is nonincreasing on (0, ∞);
• the differential inequality integrates, with E_λ(t) = ∫₀ᵗ e^{λr} dr, to (e^{λ(t-s)}/2) d(u t, y)² - (1/2) d(u s, y)² ≤ E_λ(t - s) (φ y - φ (u t)) for 0 ≤ s ≤ t;
• in particular the energy is regularized at positive times: φ (u t) ≤ φ y + (d(u 0, y)² - e^{λt} d(u t, y)²) / (2 E_λ(t));
• two solutions satisfy d(u t, v t) ≤ e^{-λt} d(u 0, v 0), so a solution is determined by its initial point.

Main definitions

• TauCeti.IsEVISolution λ φ u: u is an EVI_λ solution for φ.

Main results

• TauCeti.IsEVISolution.comp_add_const: a time translate t ↦ u (t + s), s ≥ 0, of a solution is a solution.
• TauCeti.IsEVISolution.antitoneOn: the energy is nonincreasing along a solution.
• TauCeti.IsEVISolution.exp_mul_dist_sq_sub_le: the integrated form of the evolution variational inequality.
• TauCeti.IsEVISolution.apply_le and TauCeti.IsEVISolution.apply_le_of_nonneg: the energy regularization estimate from time zero and from any nonnegative starting time.
• TauCeti.isEVISolution_iff_apply_le: the endpoint regularization estimates characterize continuous EVI solutions of finite energy at positive times.
• TauCeti.IsEVISolution.dist_le: the λ-contraction estimate, and TauCeti.IsEVISolution.eqOn: uniqueness of the solution with a given initial point.
• TauCeti.isEVISolution_exp_neg_smul: the flow t ↦ e⁻ᵗ x of ‖x‖² / 2 on a real inner product space is an EVI_1 solution.

Implementation notes

The time variable runs over ℝ, and only the values of u on [0, ∞) matter. The energy is required to be finite along the curve at positive times, as for curves of maximal slope, while the test points y range over the whole effective domain. The integrated inequality is stated with an arbitrary real upper bound c for φ y - φ (u t), which avoids multiplying extended reals.

The underlying space is a pseudometric space, as for curves of maximal slope and geodesic convexity in this directory.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, Chapter 4.
• M. Muratori, G. Savaré, Gradient flows and evolution variational inequalities in metric spaces. I: Structural properties, J. Funct. Anal. 278 (2020), Section 3.

structure TauCeti.IsEVISolution {X : Type u_1} [PseudoMetricSpace X] (lam : ℝ) (φ : X → EReal) (u : ℝ → X) : Prop

The curve u is a solution of the evolution variational inequality EVI_λ for the energy φ, where λ = lam: it is continuous on [0, ∞), its energy is finite at positive times, and for every y with φ y ≠ ⊤ and every t > 0

(1/2) d⁺/dt d(u t, y)² + (λ/2) d(u t, y)² ≤ φ y - φ (u t),

where d⁺/dt is the upper right Dini derivative, the limit superior of the difference quotients from the right.

• continuousOn : ContinuousOn u (Set.Ici 0)

  An EVI_λ solution is continuous on [0, ∞).

• apply_ne_top {t : ℝ} (ht : 0 < t) : φ (u t) ≠ ⊤

  The energy of an EVI_λ solution at a positive time is not ⊤.

• apply_ne_bot {t : ℝ} (ht : 0 < t) : φ (u t) ≠ ⊥

  The energy of an EVI_λ solution at a positive time is not ⊥.

• limsup_slope_add_le {y : X} (hy : φ y ≠ ⊤) {t : ℝ} (ht : 0 < t) : Filter.limsup (fun (s : ℝ) => ↑(slope (fun (r : ℝ) => dist (u r) y ^ 2 / 2) t s)) (nhdsWithin t (Set.Ioi t)) + ↑(lam * (dist (u t) y ^ 2 / 2)) ≤ φ y - φ (u t)

  The evolution variational inequality.

theorem TauCeti.IsEVISolution.mono {X : Type u_1} [PseudoMetricSpace X] {lam lam' : ℝ} {φ : X → EReal} {u : ℝ → X} (h : IsEVISolution lam φ u) (hlam : lam' ≤ lam) : IsEVISolution lam' φ u

An EVI_λ solution is an EVI_λ' solution for every λ' ≤ λ.

theorem TauCeti.IsEVISolution.congr {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u v : ℝ → X} (h : IsEVISolution lam φ u) (huv : Set.EqOn u v (Set.Ici 0)) : IsEVISolution lam φ v

Being an EVI_λ solution depends only on the values of the curve at nonnegative times.

theorem TauCeti.IsEVISolution.comp_add_const {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} {s : ℝ} (h : IsEVISolution lam φ u) (hs : 0 ≤ s) : IsEVISolution lam φ fun (t : ℝ) => u (t + s)

Time translation. For s ≥ 0, the curve t ↦ u (t + s) started at time s along an EVI_λ solution u is again an EVI_λ solution.

theorem TauCeti.IsEVISolution.eventually_slope_lt {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} {y : X} {t : ℝ} (h : IsEVISolution lam φ u) (ht : 0 < t) {c : ℝ} (hc : φ y - φ (u t) ≤ ↑c) {r : ℝ} (hr : c - lam * (dist (u t) y ^ 2 / 2) < r) : ∀ᶠ (s : ℝ) in nhdsWithin t (Set.Ioi t), slope (fun (r : ℝ) => dist (u r) y ^ 2 / 2) t s < r

The evolution variational inequality bounds the difference quotients of d(u ·, y)² / 2 eventually from the right: for t > 0 and any real r > c - λ d(u t, y)² / 2, where c bounds φ y - φ (u t), the difference quotients at t are eventually less than r.

theorem TauCeti.IsEVISolution.antitoneOn {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} (h : IsEVISolution lam φ u) (hφ : LowerSemicontinuous φ) : AntitoneOn (fun (t : ℝ) => φ (u t)) (Set.Ioi 0)

The energy is nonincreasing along an EVI_λ solution of a lower semicontinuous energy.

theorem TauCeti.IsEVISolution.exp_mul_dist_sq_sub_le {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} {y : X} {s t : ℝ} (h : IsEVISolution lam φ u) (hφ : LowerSemicontinuous φ) (hs : 0 ≤ s) (hst : s ≤ t) {c : ℝ} (hc : φ y - φ (u t) ≤ ↑c) : Real.exp (lam * (t - s)) * (dist (u t) y ^ 2 / 2) - dist (u s) y ^ 2 / 2 ≤ (∫ (r : ℝ) in 0..t - s, Real.exp (lam * r)) * c

The integrated evolution variational inequality. For an EVI_λ solution u of a lower semicontinuous energy, a point y, times 0 ≤ s ≤ t and a real bound φ y - φ (u t) ≤ c,

(e^{λ(t-s)}/2) d(u t, y)² - (1/2) d(u s, y)² ≤ E_λ(t - s) c, where E_λ(T) = ∫₀ᵀ e^{λr} dr.

theorem TauCeti.IsEVISolution.apply_le {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} {y : X} {t : ℝ} (h : IsEVISolution lam φ u) (hφ : LowerSemicontinuous φ) (ht : 0 < t) : φ (u t) ≤ φ y + ↑((dist (u 0) y ^ 2 - Real.exp (lam * t) * dist (u t) y ^ 2) / (2 * ∫ (r : ℝ) in 0..t, Real.exp (lam * r)))

The energy regularization estimate. For an EVI_λ solution u of a lower semicontinuous energy, a point y and a time t > 0 (trivially true when φ y = ⊤),

φ (u t) ≤ φ y + (d(u 0, y)² - e^{λt} d(u t, y)²) / (2 E_λ(t)), where E_λ(t) = ∫₀ᵗ e^{λr} dr.

theorem TauCeti.IsEVISolution.apply_le_of_nonneg {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} {y : X} {s t : ℝ} (h : IsEVISolution lam φ u) (hφ : LowerSemicontinuous φ) (hs : 0 ≤ s) (hst : s < t) : φ (u t) ≤ φ y + ↑((dist (u s) y ^ 2 - Real.exp (lam * (t - s)) * dist (u t) y ^ 2) / (2 * ∫ (r : ℝ) in 0..t - s, Real.exp (lam * r)))

The energy regularization estimate on an interval starting at any nonnegative time.

theorem TauCeti.isEVISolution_of_apply_le {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} (hφ : LowerSemicontinuous φ) (hu : ContinuousOn u (Set.Ici 0)) (htop : ∀ t > 0, φ (u t) ≠ ⊤) (hbot : ∀ t > 0, φ (u t) ≠ ⊥) (h : ∀ (y : X), φ y ≠ ⊤ → ∀ (s t : ℝ), 0 ≤ s → s < t → φ (u t) ≤ φ y + ↑((dist (u s) y ^ 2 - Real.exp (lam * (t - s)) * dist (u t) y ^ 2) / (2 * ∫ (r : ℝ) in 0..t - s, Real.exp (lam * r)))) : IsEVISolution lam φ u

The endpoint energy regularization estimate on every positive-length time interval implies the EVI, provided the energy is lower semicontinuous and finite along the curve at positive times.

theorem TauCeti.isEVISolution_iff_apply_le {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u : ℝ → X} (hφ : LowerSemicontinuous φ) : IsEVISolution lam φ u ↔ ContinuousOn u (Set.Ici 0) ∧ (∀ t > 0, φ (u t) ≠ ⊤) ∧ (∀ t > 0, φ (u t) ≠ ⊥) ∧ ∀ (y : X), φ y ≠ ⊤ → ∀ (s t : ℝ), 0 ≤ s → s < t → φ (u t) ≤ φ y + ↑((dist (u s) y ^ 2 - Real.exp (lam * (t - s)) * dist (u t) y ^ 2) / (2 * ∫ (r : ℝ) in 0..t - s, Real.exp (lam * r)))

For a lower semicontinuous energy, continuous curves of finite energy at positive times are EVI solutions exactly when they satisfy every endpoint energy regularization estimate.

theorem TauCeti.IsEVISolution.dist_le {X : Type u_1} [PseudoMetricSpace X] {lam : ℝ} {φ : X → EReal} {u v : ℝ → X} {t : ℝ} (hu : IsEVISolution lam φ u) (hv : IsEVISolution lam φ v) (hφ : LowerSemicontinuous φ) (ht : 0 ≤ t) : dist (u t) (v t) ≤ Real.exp (-(lam * t)) * dist (u 0) (v 0)

λ-contraction of EVI_λ solutions. Two EVI_λ solutions u and v of a lower semicontinuous energy satisfy d(u t, v t) ≤ e^{-λt} d(u 0, v 0) for every t ≥ 0.

theorem TauCeti.IsEVISolution.eqOn {X : Type u_1} [MetricSpace X] {lam : ℝ} {φ : X → EReal} {u v : ℝ → X} (hu : IsEVISolution lam φ u) (hv : IsEVISolution lam φ v) (hφ : LowerSemicontinuous φ) (h₀ : u 0 = v 0) : Set.EqOn u v (Set.Ici 0)

Uniqueness of EVI_λ solutions. In a metric space, two EVI_λ solutions of a lower semicontinuous energy with the same initial point agree on [0, ∞).

theorem TauCeti.isEVISolution_exp_neg_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : IsEVISolution 1 (fun (y : E) => ↑(‖y‖ ^ 2 / 2)) fun (t : ℝ) => Real.exp (-t) • x

The flow t ↦ e⁻ᵗ x of the energy ‖x‖² / 2 on a real inner product space is an EVI_1 solution: along it (1/2) d/dt ‖u t - y‖² + (1/2) ‖u t - y‖² = ‖y‖² / 2 - ‖u t‖² / 2.