The Moreau–Yosida approximation and the resolvent of an energy

For an energy φ : X → EReal on an extended metric space and a time step τ ≥ 0, the Moreau–Yosida approximation of φ is

φ_τ(x) = inf_y (φ y + d(x, y)² / (2τ)),

and the resolvent J_τ x is the set of points y at which this infimum is attained. A point of J_τ x is one step of the implicit Euler scheme for the gradient flow of φ started at x, and iterating resolvent steps gives the minimizing movement scheme of De Giorgi. The estimates proved here are the discrete counterparts of the energy-dissipation inequality on which the convergence of that scheme rests.

The infimum and the minimization run only over the points at finite distance from x, so both depend only on the finite-distance component of x, and a resolvent step stays at finite distance from its starting point (TauCeti.edist_ne_top_of_mem_moreauYosidaResolvent). Ambrosio–Gigli–Savaré take energies with values in (-∞, ∞]; here φ may take the value ⊥, and the results assume φ ≠ ⊥ at the points where they need it.

Main definitions

• TauCeti.moreauYosida φ τ x: the Moreau–Yosida approximation φ_τ(x).
• TauCeti.moreauYosidaResolvent φ τ x: the resolvent J_τ x, the set of minimizers of y ↦ φ y + d(x, y)² / (2τ) over the points at finite distance from x.

Main results

• TauCeti.apply_add_le_of_mem_moreauYosidaResolvent: the one-step energy estimate φ y + d(x, y)² / (2τ) ≤ φ x for y ∈ J_τ x.
• TauCeti.edist_ne_top_of_mem_moreauYosidaResolvent: a resolvent step has finite length.
• TauCeti.edist_le_edist_of_mem_moreauYosidaResolvent and TauCeti.apply_le_apply_of_mem_moreauYosidaResolvent: for τ < σ, a resolvent step of time σ goes at least as far as one of time τ, and reaches energy at most as large.
• TauCeti.toENNReal_sub_le_of_mem_moreauYosidaResolvent: the local decrease estimate (φ y - φ z)⁺ ≤ (d(x, y) / τ + d(y, z) / (2τ)) d(y, z) for y ∈ J_τ x.
• TauCeti.descendingSlope_le_of_mem_moreauYosidaResolvent: the slope estimate |∂φ|(y) ≤ d(x, y) / τ for y ∈ J_τ x.
• TauCeti.apply_add_sum_le_of_forall_mem_moreauYosidaResolvent: the discrete energy estimate φ (u N) + ∑_{n < N} d(u n, u (n + 1))² / (2τ) ≤ φ (u 0) along a minimizing movement sequence.
• TauCeti.moreauYosida_eq_iInf and TauCeti.mem_moreauYosidaResolvent_iff_isMinOn: on a pseudometric space, φ_τ(x) is the infimum of the penalized energy over all points and J_τ x is its set of global minimizers; TauCeti.apply_add_le_apply_add_of_mem_moreauYosidaResolvent is the minimality of a resolvent step with the real penalty dist x z ^ 2 / (2τ).
• TauCeti.moreauYosida_half_norm_sq: on a seminormed real inner product space, the Moreau–Yosida approximation of ‖·‖² / 2 is ‖x‖² / (2 (1 + τ)).
• TauCeti.moreauYosidaResolvent_half_norm_sq: on a normed real inner product space, the resolvent of ‖·‖² / 2 is the single point x / (1 + τ).

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 and Chapter 3, Section 3.1.

noncomputable def TauCeti.moreauYosida {X : Type u_1} [PseudoEMetricSpace X] (φ : X → EReal) (τ : NNReal) (x : X) : EReal

The Moreau–Yosida approximation φ_τ(x) = inf_y (φ y + d(x, y)² / (2τ)) of an energy φ with time step τ. The infimum runs over the points y at finite distance from x, so points at infinite distance from x do not contribute, even where φ y = ⊥.

theorem TauCeti.moreauYosida_def {X : Type u_1} [PseudoEMetricSpace X] (φ : X → EReal) (τ : NNReal) (x : X) : moreauYosida φ τ x = ⨅ (y : X), ⨅ (_ : edist x y ≠ ⊤), φ y + ↑(edist x y ^ 2 / (2 * ↑τ))

The defining formula of the Moreau–Yosida approximation, as an infimum.

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

The Moreau–Yosida approximation at x is at most the penalized energy at any point y at finite distance from x.

theorem TauCeti.le_moreauYosida_iff {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x : X} {c : EReal} : c ≤ moreauYosida φ τ x ↔ ∀ (y : X), edist x y ≠ ⊤ → c ≤ φ y + ↑(edist x y ^ 2 / (2 * ↑τ))

A lower bound for the Moreau–Yosida approximation is a lower bound for the penalized energy at every point at finite distance from x.

theorem TauCeti.moreauYosida_le_self {X : Type u_1} [PseudoEMetricSpace X] (φ : X → EReal) (τ : NNReal) (x : X) : moreauYosida φ τ x ≤ φ x

The Moreau–Yosida approximation lies below the energy.

theorem TauCeti.moreauYosida_mono {X : Type u_1} [PseudoEMetricSpace X] {φ ψ : X → EReal} (h : φ ≤ ψ) (τ : NNReal) (x : X) : moreauYosida φ τ x ≤ moreauYosida ψ τ x

The Moreau–Yosida approximation is monotone in the energy.

theorem TauCeti.antitone_moreauYosida {X : Type u_1} [PseudoEMetricSpace X] (φ : X → EReal) (x : X) : Antitone fun (x_1 : NNReal) => moreauYosida φ x_1 x

The Moreau–Yosida approximation decreases as the time step grows.

def TauCeti.moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] (φ : X → EReal) (τ : NNReal) (x : X) : Set X

The resolvent J_τ x of an energy φ: the set of points y at finite distance from x minimizing y ↦ φ y + d(x, y)² / (2τ) among the points at finite distance from x, that is, attaining the Moreau–Yosida approximation φ_τ(x) (TauCeti.mem_moreauYosidaResolvent_iff_eq_moreauYosida). It may be empty or contain several points.

theorem TauCeti.mem_moreauYosidaResolvent_iff {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} : y ∈ moreauYosidaResolvent φ τ x ↔ edist x y ≠ ⊤ ∧ ∀ (z : X), edist x z ≠ ⊤ → φ y + ↑(edist x y ^ 2 / (2 * ↑τ)) ≤ φ z + ↑(edist x z ^ 2 / (2 * ↑τ))

The defining property of the resolvent: y is at finite distance from x and minimizes the penalized energy among the points at finite distance from x.

theorem TauCeti.mem_moreauYosidaResolvent_iff_eq_moreauYosida {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} : y ∈ moreauYosidaResolvent φ τ x ↔ edist x y ≠ ⊤ ∧ φ y + ↑(edist x y ^ 2 / (2 * ↑τ)) = moreauYosida φ τ x

A point lies in the resolvent exactly when it is at finite distance from x and attains the Moreau–Yosida approximation.

theorem TauCeti.apply_add_le_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hy : y ∈ moreauYosidaResolvent φ τ x) : φ y + ↑(edist x y ^ 2 / (2 * ↑τ)) ≤ φ x

One-step energy estimate. A resolvent step y ∈ J_τ x lowers the energy by at least the penalty d(x, y)² / (2τ).

theorem TauCeti.apply_le_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hy : y ∈ moreauYosidaResolvent φ τ x) : φ y ≤ φ x

A resolvent step does not increase the energy.

theorem TauCeti.apply_ne_top_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hy : y ∈ moreauYosidaResolvent φ τ x) (hx : moreauYosida φ τ x ≠ ⊤) : φ y ≠ ⊤

A resolvent step from a point where the Moreau–Yosida approximation is finite has finite energy.

theorem TauCeti.edist_ne_top_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hy : y ∈ moreauYosidaResolvent φ τ x) : edist x y ≠ ⊤

Resolvent steps stay in the finite-distance component. A resolvent step y ∈ J_τ x has finite length.

theorem TauCeti.apply_ne_bot_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hy : y ∈ moreauYosidaResolvent φ τ x) (hφy : φ y ≠ ⊥) {z : X} (hz : edist x z ≠ ⊤) : φ z ≠ ⊥

A resolvent step y ∈ J_τ x with φ y ≠ ⊥ forces φ ≠ ⊥ at every point at finite distance from x: otherwise that point would have penalized energy ⊥, below that of y.

theorem TauCeti.add_toReal_sq_div_le_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hτ : 0 < τ) (hy : y ∈ moreauYosidaResolvent φ τ x) {z : X} (hz : edist x z ≠ ⊤) {a b : ℝ} (ha : φ y = ↑a) (hb : φ z = ↑b) : a + (edist x y).toReal ^ 2 / (2 * ↑τ) ≤ b + (edist x z).toReal ^ 2 / (2 * ↑τ)

Minimality of a resolvent step, in real numbers. For a resolvent step y ∈ J_τ x with τ > 0, a point z at finite distance from x, and real energies φ y = a and φ z = b, the minimality of y against z is the real inequality a + d(x, y)² / (2τ) ≤ b + d(x, z)² / (2τ).

theorem TauCeti.edist_le_edist_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ σ : NNReal} {x y : X} (hτσ : τ < σ) (hy₀ : y ∈ moreauYosidaResolvent φ τ x) {y₁ : X} (hy₁ : y₁ ∈ moreauYosidaResolvent φ σ x) (hφy₀ : φ y ≠ ⊥) (hx : moreauYosida φ τ x ≠ ⊤) : edist x y ≤ edist x y₁

Monotonicity of resolvent steps in the time step. For time steps τ < σ, a resolvent step of time σ from x goes at least as far as a resolvent step y of time τ, provided the Moreau–Yosida approximation φ_τ(x) is finite and φ y ≠ ⊥.

theorem TauCeti.apply_le_apply_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ σ : NNReal} {x y : X} (hτ : 0 < τ) (hτσ : τ < σ) (hy₀ : y ∈ moreauYosidaResolvent φ τ x) {y₁ : X} (hy₁ : y₁ ∈ moreauYosidaResolvent φ σ x) : φ y₁ ≤ φ y

Monotonicity of resolvent steps in the time step. For time steps 0 < τ < σ, a resolvent step of time σ from x reaches energy at most that of a resolvent step of time τ.

theorem TauCeti.apply_add_sum_le_of_forall_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {u : ℕ → X} (hu : ∀ (n : ℕ), u (n + 1) ∈ moreauYosidaResolvent φ τ (u n)) (N : ℕ) : φ (u N) + ↑(∑ n ∈ Finset.range N, edist (u n) (u (n + 1)) ^ 2 / (2 * ↑τ)) ≤ φ (u 0)

Discrete energy estimate. Along a minimizing movement sequence, in which each u (n + 1) is a resolvent step from u n, the energy at time N plus the accumulated penalties ∑_{n < N} d(u n, u (n + 1))² / (2τ) is at most the initial energy.

theorem TauCeti.antitone_comp_of_forall_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {u : ℕ → X} (hu : ∀ (n : ℕ), u (n + 1) ∈ moreauYosidaResolvent φ τ (u n)) : Antitone (φ ∘ u)

Along a minimizing movement sequence the energy is nonincreasing.

theorem TauCeti.toENNReal_sub_le_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hτ : 0 < τ) (hy : y ∈ moreauYosidaResolvent φ τ x) {z : X} : (φ y - φ z).toENNReal ≤ (edist x y / ↑τ + edist y z / (2 * ↑τ)) * edist y z

Local decrease estimate for resolvent steps. If y ∈ J_τ x is a resolvent step with time step τ > 0, then for every z the decrease (φ y - φ z)⁺ is at most (d(x, y) / τ + d(y, z) / (2τ)) d(y, z). With d = d(x, y), e = d(x, z) and r = d(y, z), minimality of y gives 2τ (φ y - φ z) ≤ e² - d² ≤ (d + r)² - d² = 2dr + r².

theorem TauCeti.coe_edist_sq_div_eq_coe_dist_sq_div {X : Type u_1} [PseudoMetricSpace X] {τ : NNReal} (hτ : 0 < τ) (x y : X) : ↑(edist x y ^ 2 / (2 * ↑τ)) = ↑(dist x y ^ 2 / (2 * ↑τ))

On a pseudometric space with a time step τ > 0, the penalty d(x, y)² / (2τ) is the real number dist x y ^ 2 / (2τ).

theorem TauCeti.moreauYosida_eq_iInf {X : Type u_1} [PseudoMetricSpace X] (φ : X → EReal) (τ : NNReal) (x : X) : moreauYosida φ τ x = ⨅ (y : X), φ y + ↑(edist x y ^ 2 / (2 * ↑τ))

On a pseudometric space every point is at finite distance from x, so the Moreau–Yosida approximation is the infimum of the penalized energy over all points.

theorem TauCeti.mem_moreauYosidaResolvent_iff_isMinOn {X : Type u_1} [PseudoMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} : y ∈ moreauYosidaResolvent φ τ x ↔ IsMinOn (fun (z : X) => φ z + ↑(edist x z ^ 2 / (2 * ↑τ))) Set.univ y

On a pseudometric space, the resolvent J_τ x is the set of global minimizers of the penalized energy y ↦ φ y + d(x, y)² / (2τ).

theorem TauCeti.apply_add_le_apply_add_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hτ : 0 < τ) (hy : y ∈ moreauYosidaResolvent φ τ x) (z : X) : φ y + ↑(dist x y ^ 2 / (2 * ↑τ)) ≤ φ z + ↑(dist x z ^ 2 / (2 * ↑τ))

On a pseudometric space with a time step τ > 0, a resolvent step y ∈ J_τ x minimizes the penalized energy z ↦ φ z + d(x, z)² / (2τ), written with the real penalty.

theorem TauCeti.descendingSlope_le_of_mem_moreauYosidaResolvent {X : Type u_1} [EMetricSpace X] {φ : X → EReal} {τ : NNReal} {x y : X} (hτ : 0 < τ) (hy : y ∈ moreauYosidaResolvent φ τ x) : descendingSlope φ y ≤ edist x y / ↑τ

Slope estimate for resolvent steps. If y ∈ J_τ x is a resolvent step with time step τ > 0, then the descending slope of φ at y is at most d(x, y) / τ.

theorem TauCeti.half_norm_sq_add_edist_sq_div {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {τ : NNReal} (hτ : 0 < τ) (x y : E) : ↑(‖y‖ ^ 2 / 2) + ↑(edist x y ^ 2 / (2 * ↑τ)) = ↑(‖x‖ ^ 2 / (2 * (1 + ↑τ)) + (1 + ↑τ) / (2 * ↑τ) * ‖y - (1 + ↑τ)⁻¹ • x‖ ^ 2)

The objective φ y + d(x, y)² / (2τ) for φ = ‖·‖² / 2, as a real number, with the square completed: its minimum value ‖x‖² / (2 (1 + τ)) plus (1 + τ) / (2τ) times the squared distance from y to the minimizer x / (1 + τ). This is TauCeti.norm_sq_div_two_add_norm_sub_sq_div with the penalty read in EReal.

@[simp]

theorem TauCeti.moreauYosida_half_norm_sq {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (τ : NNReal) (x : E) : moreauYosida (fun (y : E) => ↑(‖y‖ ^ 2 / 2)) τ x = ↑(‖x‖ ^ 2 / (2 * (1 + ↑τ)))

On a seminormed real inner product space, the Moreau–Yosida approximation of the energy ‖·‖² / 2 with time step τ is ‖x‖² / (2 (1 + τ)).

@[simp]

theorem TauCeti.moreauYosidaResolvent_half_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (τ : NNReal) (x : E) : moreauYosidaResolvent (fun (y : E) => ↑(‖y‖ ^ 2 / 2)) τ x = {(1 + ↑τ)⁻¹ • x}

On a real inner product space, the resolvent of the energy ‖·‖² / 2 with time step τ is the single point x / (1 + τ).