Existence of resolvent steps and of minimizing movement sequences

For an energy φ : X → EReal on an extended metric space and a time step τ > 0, a point of the resolvent J_τ x minimizes y ↦ φ y + d(x, y)² / (2τ). This file proves, by the direct method of the calculus of variations, that such a minimizer exists under the hypotheses of Ambrosio–Gigli–Savaré, and hence that the minimizing movement scheme can be run from every point of the relevant finite-distance component.

The hypotheses use an auxiliary notion of convergence on X, which need not be that of the metric. In applications it is weaker: the weak topology of a Hilbert space, or the narrow topology on the Wasserstein space P₂(X), whose bounded sets are not relatively compact for the metric. Following Ambrosio–Gigli–Savaré, Assumption 2.1, with y_n ⇀ y denoting this convergence, the hypotheses are:

• the distance is sequentially lower semicontinuous: if y_n ⇀ y, then d(x, y) ≤ liminf d(x, y_n) (only the point x of the resolvent step is needed);
• the energy is sequentially lower semicontinuous on bounded sets: if y_n ⇀ y and (y_n) has finite diameter, then φ y ≤ liminf φ (y_n);
• bounded sublevels are relatively sequentially compact: a sequence of finite diameter along which φ is bounded above by a real number has a subsequence with y_{n_k} ⇀ y for some y;
• coercivity: φ_{τ₀}(x₀) > -∞ for some time step τ₀ and point x₀, where φ_τ is the Moreau–Yosida approximation.

Coercivity at (τ₀, x₀) propagates to every smaller time step and every point at finite distance from x₀ (TauCeti.moreauYosida_ne_bot_of_lt), through the quantitative bound φ_{τ₀}(x₀) ≤ φ_τ(x) + d(x, x₀)² / (2 (τ₀ - τ)) for τ < τ₀. Together with the other hypotheses it makes a minimizing sequence for φ_τ(x) bounded and contained in a sublevel of φ, so that a limit of a subsequence is a resolvent step.

Main results

• TauCeti.moreauYosida_le_moreauYosida_add: the bound φ_{τ₀}(x₀) ≤ φ_τ(x) + d(x, x₀)² / (2 (τ₀ - τ)) for τ < τ₀ and d(x, x₀) < ∞, and TauCeti.moreauYosida_ne_bot_of_lt: coercivity propagates.
• TauCeti.le_liminf_apply_add_edist_sq_div: the penalized energy φ + d(x, ·)² / (2τ) is lower semicontinuous along any convergence for which φ and d(x, ·) are.
• TauCeti.moreauYosidaResolvent_nonempty: under the hypotheses above, the resolvent J_τ x is nonempty for every τ < τ₀ and every x at finite distance from x₀.
• TauCeti.moreauYosidaResolvent_nonempty_of_lowerSemicontinuous: in a proper metric space, the resolvent of a lower semicontinuous coercive energy is nonempty, the auxiliary convergence being that of the metric.
• TauCeti.exists_forall_mem_moreauYosidaResolvent: under the same hypotheses, every point at finite distance from x₀ starts a minimizing movement sequence, in which each term is a resolvent step from the previous one.

Implementation notes

The auxiliary convergence is a map l : X → Filter X, with y_n ⇀ y meaning Tendsto (fun n ↦ y_n) atTop (l y). For a topology σ on X one takes l = @nhds X σ, and for a topology induced by a map f : X → Y, such as the narrow topology on P₂(X) pulled back from probability measures, l y = comap f (𝓝 (f y)). No property of l is used. Taking a map rather than a second TopologicalSpace X instance keeps it from competing with the topology of the metric.

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 2, Section 2.1 (Assumption 2.1) and Section 2.2 (Lemma 2.2.1 and Corollary 2.2.2).

theorem TauCeti.le_liminf_apply_add_edist_sq_div {X : Type u_1} [EDist X] {φ : X → EReal} {τ : NNReal} {x : X} {ι : Type u_2} {f : Filter ι} {w : ι → X} {y : X} (hd : edist x y ≤ Filter.liminf (fun (n : ι) => edist x (w n)) f) (hφ : φ y ≤ Filter.liminf (fun (n : ι) => φ (w n)) f) : φ y + ↑(edist x y ^ 2 / (2 * ↑τ)) ≤ Filter.liminf (fun (n : ι) => φ (w n) + ↑(edist x (w n) ^ 2 / (2 * ↑τ))) f

Lower semicontinuity of the penalized energy. If φ y ≤ liminf φ (w n) and d(x, y) ≤ liminf d(x, w n), then the penalized energy φ + d(x, ·)² / (2τ) satisfies the same inequality, including at τ = 0 with extended nonnegative division.

theorem TauCeti.edist_sq_div_le_add {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {τ τ₀ : NNReal} (hττ₀ : τ < τ₀) (x x₀ z : X) : edist x₀ z ^ 2 / (2 * ↑τ₀) ≤ edist x z ^ 2 / (2 * ↑τ) + edist x x₀ ^ 2 / (2 * (↑τ₀ - ↑τ))

For time steps τ < τ₀, the penalty d(x₀, z)² / (2τ₀) is at most d(x, z)² / (2τ) + d(x, x₀)² / (2 (τ₀ - τ)). With a = d(x, z), b = d(x, x₀) and s = τ₀ - τ, this is the triangle inequality followed by (a + b)² / (τ + s) ≤ a² / τ + b² / s.

theorem TauCeti.moreauYosida_le_moreauYosida_add {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ τ₀ : NNReal} {x x₀ : X} (hττ₀ : τ < τ₀) (hx : edist x x₀ ≠ ⊤) : moreauYosida φ τ₀ x₀ ≤ moreauYosida φ τ x + ↑(edist x x₀ ^ 2 / (2 * (↑τ₀ - ↑τ)))

Propagation of coercivity, quantitatively (Ambrosio–Gigli–Savaré, Lemma 2.2.1). For time steps τ < τ₀ and a point x at finite distance from x₀, φ_{τ₀}(x₀) ≤ φ_τ(x) + d(x, x₀)² / (2 (τ₀ - τ)).

theorem TauCeti.moreauYosida_ne_bot_of_lt {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ τ₀ : NNReal} {x x₀ : X} (hττ₀ : τ < τ₀) (hx : edist x x₀ ≠ ⊤) (h₀ : moreauYosida φ τ₀ x₀ ≠ ⊥) : moreauYosida φ τ x ≠ ⊥

Propagation of coercivity. If φ_{τ₀}(x₀) > -∞, then φ_τ(x) > -∞ for every time step τ < τ₀ and every point x at finite distance from x₀.

theorem TauCeti.coe_sub_div_le_moreauYosida {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ τ₀ : NNReal} {x x₀ : X} {m D : ℝ} (hττ₀ : τ < τ₀) (hm : moreauYosida φ τ₀ x₀ = ↑m) (hD : 0 ≤ D) (hxD : edist x x₀ ≤ ENNReal.ofReal D) : ↑(m - D ^ 2 / (2 * (↑τ₀ - ↑τ))) ≤ moreauYosida φ τ x

Propagation of coercivity, real form. If φ_{τ₀}(x₀) = m is a real number, τ < τ₀, and x lies within the real distance D of x₀, then m - D² / (2 (τ₀ - τ)) ≤ φ_τ(x).

theorem TauCeti.moreauYosidaResolvent_nonempty {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ τ₀ : NNReal} {x x₀ : X} {l : X → Filter X} (hd : ∀ ⦃v : ℕ → X⦄ ⦃y : X⦄, Filter.Tendsto v Filter.atTop (l y) → edist x y ≤ Filter.liminf (fun (n : ℕ) => edist x (v n)) Filter.atTop) (hφ : ∀ ⦃v : ℕ → X⦄ ⦃y : X⦄, Metric.ediam (Set.range v) ≠ ⊤ → Filter.Tendsto v Filter.atTop (l y) → φ y ≤ Filter.liminf (fun (n : ℕ) => φ (v n)) Filter.atTop) (hcpt : ∀ (c : ℝ) ⦃v : ℕ → X⦄, Metric.ediam (Set.range v) ≠ ⊤ → (∀ (n : ℕ), φ (v n) ≤ ↑c) → ∃ (y : X) (ψ : ℕ → ℕ), StrictMono ψ ∧ Filter.Tendsto (v ∘ ψ) Filter.atTop (l y)) (hττ₀ : τ < τ₀) (hx : edist x x₀ ≠ ⊤) (h₀ : moreauYosida φ τ₀ x₀ ≠ ⊥) : (moreauYosidaResolvent φ τ x).Nonempty

Existence of resolvent steps (Ambrosio–Gigli–Savaré, Corollary 2.2.2). Let l y be the filter of an auxiliary convergence y_n ⇀ y on X, possibly weaker than that of the metric (for instance l = @nhds X σ for a topology σ), such that

• y ↦ d(x, y) is sequentially lower semicontinuous for ⇀;
• φ is sequentially lower semicontinuous for ⇀ along sequences of finite diameter;
• every sequence of finite diameter along which φ is bounded above by a real number has a ⇀-convergent subsequence;

and let φ be coercive: φ_{τ₀}(x₀) > -∞. Then for every time step τ < τ₀ and every point x at finite distance from x₀, the resolvent J_τ x is nonempty.

theorem TauCeti.exists_forall_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ τ₀ : NNReal} {x x₀ : X} {l : X → Filter X} (hd : ∀ (z : X) ⦃v : ℕ → X⦄ ⦃y : X⦄, Filter.Tendsto v Filter.atTop (l y) → edist z y ≤ Filter.liminf (fun (n : ℕ) => edist z (v n)) Filter.atTop) (hφ : ∀ ⦃v : ℕ → X⦄ ⦃y : X⦄, Metric.ediam (Set.range v) ≠ ⊤ → Filter.Tendsto v Filter.atTop (l y) → φ y ≤ Filter.liminf (fun (n : ℕ) => φ (v n)) Filter.atTop) (hcpt : ∀ (c : ℝ) ⦃v : ℕ → X⦄, Metric.ediam (Set.range v) ≠ ⊤ → (∀ (n : ℕ), φ (v n) ≤ ↑c) → ∃ (y : X) (ψ : ℕ → ℕ), StrictMono ψ ∧ Filter.Tendsto (v ∘ ψ) Filter.atTop (l y)) (hττ₀ : τ < τ₀) (hx : edist x x₀ ≠ ⊤) (h₀ : moreauYosida φ τ₀ x₀ ≠ ⊥) : ∃ (u : ℕ → X), u 0 = x ∧ ∀ (n : ℕ), u (n + 1) ∈ moreauYosidaResolvent φ τ (u n)

Existence of minimizing movement sequences (Ambrosio–Gigli–Savaré, Corollary 2.2.2). Under the hypotheses of TauCeti.moreauYosidaResolvent_nonempty, with the lower semicontinuity of the distance now required from every base point, every point x at finite distance from x₀ starts a sequence u with u 0 = x in which each u (n + 1) is a resolvent step from u n.

theorem TauCeti.moreauYosidaResolvent_nonempty_of_lowerSemicontinuous {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {φ : X → EReal} {τ τ₀ : NNReal} {x x₀ : X} (hφ : LowerSemicontinuous φ) (hττ₀ : τ < τ₀) (h₀ : moreauYosida φ τ₀ x₀ ≠ ⊥) : (moreauYosidaResolvent φ τ x).Nonempty

Existence of resolvent steps in a proper space. In a proper metric space, the resolvent J_τ x of a lower semicontinuous energy φ with φ_{τ₀}(x₀) > -∞ is nonempty for every time step τ < τ₀. This is TauCeti.moreauYosidaResolvent_nonempty with l = 𝓝, the convergence of the metric, for which bounded sequences have convergent subsequences.