The discrete variational inequality for resolvents of convex energies

Let φ : X → EReal be an energy on a metric space, m : ℝ and τ > 0 a time step. The convexity hypothesis under which Ambrosio–Gigli–Savaré prove that minimizing movements converge to the EVI_m gradient flow (their Assumption 4.0.1) is that the penalized energies of the resolvent are uniformly convex along some curve: for every base point w and any two points v₀, v₁ of the effective domain {x | φ x ≠ ⊤} there is a curve γ from v₀ to v₁ along which

z ↦ φ z + d(w, z)² / (2τ) is (m + 1 / τ)-convex

(TauCeti.PenalizedConvex m τ φ). This holds when φ is m-geodesically convex on a CAT(0) space, where the squared distance from w is 2-convex along every geodesic (TauCeti.GeodesicallyConvex.penalizedConvex), and, on the quadratic Wasserstein space, when φ is m-convex along generalized geodesics based at every law and 1 + m τ ≥ 0 (TauCeti.penalizedConvex_of_generalizedGeodesicallyConvex). Ordinary geodesic convexity is not enough in general, because the squared distance from a point need not be convex along geodesics. Ambrosio–Gigli–Savaré take the base point w in the effective domain; it is arbitrary here, as in both examples.

Under this hypothesis a resolvent step y ∈ J_τ x satisfies the discrete variational inequality (TauCeti.PenalizedConvex.apply_add_le_of_mem_moreauYosidaResolvent): for every v with φ v ≠ ⊤,

φ y + d(x, y)² / (2τ) + d(y, v)² / (2τ) + (m / 2) d(y, v)² ≤ φ v + d(x, v)² / (2τ).

The penalized energy at x is smallest at y, so it grows at least quadratically along the curve from y to v (TauCeti.ConvexAlong.apply_add_le_of_forall_le). Read as (d(y, v)² - d(x, v)²) / (2τ) + (m / 2) d(y, v)² ≤ φ v - φ y - d(x, y)² / (2τ), this is the implicit Euler discretization of the evolution variational inequality (1/2) d/dt d(u t, v)² + (m / 2) d(u t, v)² ≤ φ v - φ (u t) (TauCeti.IsEVISolution). In particular, when 1 + m τ > 0 and φ never takes the value ⊥ and is finite somewhere, the resolvent has at most one point (TauCeti.PenalizedConvex.subsingleton_moreauYosidaResolvent).

Along a minimizing movement sequence U with U (n + 1) ∈ J_τ (U n), the discrete variational inequality reads r d(U (n + 1), v)² - d(U n, v)² ≤ 2τ (φ v - φ (U (n + 1))) with r = 1 + m τ. When r ≥ 0, multiplying by r ^ n and summing, with the energy nonincreasing, gives the discrete integrated inequality (TauCeti.PenalizedConvex.pow_mul_dist_sq_sub_le)

r ^ N d(U N, v)² / 2 - d(U 0, v)² / 2 ≤ τ (∑_{n < N} r ^ n) (φ v - φ (U N)).

This is the discrete form of the integrated evolution variational inequality TauCeti.IsEVISolution.exp_mul_dist_sq_sub_le: r ^ N replaces e^{m N τ} and τ ∑_{n < N} r ^ n replaces ∫₀^{Nτ} e^{m s} ds. Still for r ≥ 0, it gives the energy regularization estimate φ (U N) ≤ φ v + (d(U 0, v)² - r ^ N d(U N, v)²) / (2τ ∑_{n < N} r ^ n) for N ≥ 1 (TauCeti.PenalizedConvex.apply_le), which for m = 0 is the rate φ (U N) ≤ φ v + d(U 0, v)² / (2 N τ), and the weighted distance estimate r ^ N d(U N, v)² ≤ d(U 0, v)² towards a point v of smaller energy, such as a minimizer of φ (TauCeti.PenalizedConvex.pow_mul_dist_sq_le). For m > 0 and a fixed minimizer v of finite energy, this is geometric convergence of the scheme to v. These are the a priori estimates on which the convergence of minimizing movements to the EVI_m flow rests.

Main definitions

• TauCeti.PenalizedConvex m τ φ: the penalized energies φ + d(w, ·)² / (2τ) are (m + 1 / τ)-convex along some curve between any two points of finite energy.

Main results

• TauCeti.PenalizedConvex.apply_add_le_of_mem_moreauYosidaResolvent: the discrete variational inequality.
• TauCeti.PenalizedConvex.eq_of_mem_moreauYosidaResolvent and TauCeti.PenalizedConvex.subsingleton_moreauYosidaResolvent: uniqueness of the resolvent step when 1 + m τ > 0, for a resolvent step of finite energy, respectively for an energy that never takes the value ⊥ and is finite somewhere.
• TauCeti.PenalizedConvex.pow_mul_dist_sq_sub_le: the discrete integrated evolution variational inequality along a minimizing movement sequence, when 1 + m τ ≥ 0.
• TauCeti.PenalizedConvex.apply_le: the discrete energy regularization estimate, when 1 + m τ ≥ 0.
• TauCeti.PenalizedConvex.pow_mul_dist_sq_le: the weighted distance estimate of a minimizing movement sequence towards points of smaller energy, when 1 + m τ ≥ 0.
• TauCeti.GeodesicallyConvex.penalizedConvex: on a CAT(0) space, an m-geodesically convex energy satisfies the hypothesis for every time step.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, Assumption 4.0.1, Theorem 4.1.2 and Section 4.1.

def TauCeti.PenalizedConvex {X : Type u_1} [PseudoMetricSpace X] (m : ℝ) (τ : NNReal) (φ : X → EReal) : Prop

The energy φ is penalized convex with parameter m and time step τ: for every base point w and any two points v₀, v₁ with φ v₀ ≠ ⊤ and φ v₁ ≠ ⊤ (energy ⊥ is allowed), some curve γ from v₀ to v₁ makes the penalized energy z ↦ φ z + d(w, z)² / (2τ) of the resolvent (m + 1 / τ)-convex along it. This is Assumption 4.0.1 of Ambrosio–Gigli–Savaré at the time step τ, there stated with the coefficient (1 + m τ) / τ = m + 1 / τ.

theorem TauCeti.penalizedConvex_def {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} : PenalizedConvex m τ φ ↔ ∀ ⦃w v₀ v₁ : X⦄, φ v₀ ≠ ⊤ → φ v₁ ≠ ⊤ → ∃ (γ : ℝ → X), γ 0 = v₀ ∧ γ 1 = v₁ ∧ ConvexAlong (m + (↑τ)⁻¹) (fun (z : X) => φ z + ↑(dist w z ^ 2 / (2 * ↑τ))) γ

The defining condition of penalized convexity.

theorem TauCeti.PenalizedConvex.mono {X : Type u_1} [PseudoMetricSpace X] {m m' : ℝ} {τ : NNReal} {φ : X → EReal} (h : PenalizedConvex m τ φ) (hm : m' ≤ m) : PenalizedConvex m' τ φ

Penalized convexity with a parameter m implies it for every smaller parameter.

theorem TauCeti.GeodesicallyConvex.penalizedConvex {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} [IsCATZeroSpace X] (h : GeodesicallyConvex m φ) : PenalizedConvex m τ φ

On a CAT(0) space, an m-geodesically convex energy is penalized convex with parameter m for every time step, along the geodesics that witness its convexity: the squared distance from a point is 2-convex along every geodesic.

theorem TauCeti.PenalizedConvex.apply_add_le_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} {x y v : X} (h : PenalizedConvex m τ φ) (hτ : 0 < τ) (hy : y ∈ moreauYosidaResolvent φ τ x) (hv : φ v ≠ ⊤) : φ y + ↑(dist x y ^ 2 / (2 * ↑τ) + dist y v ^ 2 / (2 * ↑τ) + m / 2 * dist y v ^ 2) ≤ φ v + ↑(dist x v ^ 2 / (2 * ↑τ))

The discrete variational inequality. If φ is penalized convex with parameter m and time step τ > 0, then a resolvent step y ∈ J_τ x satisfies, for every v with φ v ≠ ⊤,

φ y + d(x, y)² / (2τ) + d(y, v)² / (2τ) + (m / 2) d(y, v)² ≤ φ v + d(x, v)² / (2τ).

This is the implicit Euler form of the evolution variational inequality EVI_m.

theorem TauCeti.PenalizedConvex.eq_of_mem_moreauYosidaResolvent {X : Type u_1} [MetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} {x y y' : X} (h : PenalizedConvex m τ φ) (hτ : 0 < τ) (hmτ : 0 < 1 + m * ↑τ) (hy : y ∈ moreauYosidaResolvent φ τ x) (hy' : y' ∈ moreauYosidaResolvent φ τ x) (htop : φ y ≠ ⊤) (hbot : φ y ≠ ⊥) : y = y'

Uniqueness of the resolvent step. If φ is penalized convex with parameter m and time step τ > 0 with 1 + m τ > 0, then two resolvent steps y, y' ∈ J_τ x, the first of finite energy, are equal.

theorem TauCeti.PenalizedConvex.subsingleton_moreauYosidaResolvent {X : Type u_1} [MetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} (h : PenalizedConvex m τ φ) (hτ : 0 < τ) (hmτ : 0 < 1 + m * ↑τ) (hbot : ∀ (z : X), φ z ≠ ⊥) (hdom : ∃ (z : X), φ z ≠ ⊤) (x : X) : (moreauYosidaResolvent φ τ x).Subsingleton

Uniqueness of the resolvent step. If φ never takes the value ⊥, is finite somewhere, and is penalized convex with parameter m and time step τ > 0 with 1 + m τ > 0, then every resolvent J_τ x has at most one point.

theorem TauCeti.PenalizedConvex.pow_mul_dist_sq_sub_le {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} {v : X} {U : ℕ → X} (h : PenalizedConvex m τ φ) (hτ : 0 < τ) (hmτ : 0 ≤ 1 + m * ↑τ) (hU : ∀ (n : ℕ), U (n + 1) ∈ moreauYosidaResolvent φ τ (U n)) (hv : φ v ≠ ⊤) {N : ℕ} (hN : φ (U N) ≠ ⊥) {c : ℝ} (hc : φ v - φ (U N) ≤ ↑c) : (1 + m * ↑τ) ^ N * (dist (U N) v ^ 2 / 2) - dist (U 0) v ^ 2 / 2 ≤ (↑τ * ∑ n ∈ Finset.range N, (1 + m * ↑τ) ^ n) * c

The discrete integrated evolution variational inequality. Let φ be penalized convex with parameter m and time step τ > 0 with 1 + m τ ≥ 0, and let U be a minimizing movement sequence, U (n + 1) ∈ J_τ (U n). For a point v with φ v ≠ ⊤, a step N with φ (U N) ≠ ⊥ and a real bound φ v - φ (U N) ≤ c, with r = 1 + m τ,

r ^ N d(U N, v)² / 2 - d(U 0, v)² / 2 ≤ τ (∑_{n < N} r ^ n) c.

This is the discrete form of TauCeti.IsEVISolution.exp_mul_dist_sq_sub_le.

theorem TauCeti.PenalizedConvex.apply_le {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} {v : X} {U : ℕ → X} (h : PenalizedConvex m τ φ) (hτ : 0 < τ) (hmτ : 0 ≤ 1 + m * ↑τ) (hU : ∀ (n : ℕ), U (n + 1) ∈ moreauYosidaResolvent φ τ (U n)) (hv : φ v ≠ ⊤) {N : ℕ} (hN : 0 < N) : φ (U N) ≤ φ v + ↑((dist (U 0) v ^ 2 - (1 + m * ↑τ) ^ N * dist (U N) v ^ 2) / (2 * ↑τ * ∑ n ∈ Finset.range N, (1 + m * ↑τ) ^ n))

The discrete energy regularization estimate. Let φ be penalized convex with parameter m and time step τ > 0 with 1 + m τ ≥ 0, and let U be a minimizing movement sequence, U (n + 1) ∈ J_τ (U n). For a point v with φ v ≠ ⊤ and a step N ≥ 1, with r = 1 + m τ,

φ (U N) ≤ φ v + (d(U 0, v)² - r ^ N d(U N, v)²) / (2τ ∑_{n < N} r ^ n).

For m = 0 this is φ (U N) ≤ φ v + (d(U 0, v)² - d(U N, v)²) / (2 N τ). This is the discrete form of TauCeti.IsEVISolution.apply_le.

theorem TauCeti.PenalizedConvex.pow_mul_dist_sq_le {X : Type u_1} [PseudoMetricSpace X] {m : ℝ} {τ : NNReal} {φ : X → EReal} {v : X} {U : ℕ → X} (h : PenalizedConvex m τ φ) (hτ : 0 < τ) (hmτ : 0 ≤ 1 + m * ↑τ) (hU : ∀ (n : ℕ), U (n + 1) ∈ moreauYosidaResolvent φ τ (U n)) (hv : φ v ≠ ⊤) (hv' : φ v ≠ ⊥) {N : ℕ} (hvN : φ v ≤ φ (U N)) : (1 + m * ↑τ) ^ N * dist (U N) v ^ 2 ≤ dist (U 0) v ^ 2

Weighted distance estimate towards points of smaller energy. Let φ be penalized convex with parameter m and time step τ > 0 with 1 + m τ ≥ 0, and let U be a minimizing movement sequence, U (n + 1) ∈ J_τ (U n). If v has finite energy φ v ≤ φ (U N), for instance if v minimizes φ, then

(1 + m τ) ^ N d(U N, v)² ≤ d(U 0, v)².

For m > 0 and a fixed minimizer v of finite energy, the scheme therefore converges geometrically to v; this is the discrete form of the contraction of the EVI_m flow.