Documentation

TauCeti.Analysis.GradientFlow.MoreauYosida.Derivative

The derivative of the Moreau–Yosida approximation in the time step #

For an energy φ : X → EReal and a point x, the Moreau–Yosida approximation φ_τ(x) = inf_y (φ y + d(x, y)² / (2τ)) is nonincreasing in the time step τ. This file computes its derivative: if y_τ ∈ J_τ x is a resolvent step for each τ in an interval, then

d/dτ φ_τ(x) = -d(x, y_τ)² / (2τ²)

at every time where τ ↦ d(x, y_τ) is continuous, hence at all but countably many times, and integrating gives the energy identity of De Giorgi's variational interpolation

φ_τ(x) + ∫₀^τ d(x, y_r)² / (2r²) dr = φ(x)

for a lower semicontinuous energy and φ(x) finite. Combined with the slope estimate |∂φ|(y_r) ≤ d(x, y_r) / r this gives the discrete energy–dissipation inequality φ_τ(x) + ∫₀^τ |∂φ|²(y_r) / 2 dr ≤ φ(x) that drives the convergence of the minimizing movement scheme.

The resolvent steps y_τ are an arbitrary selection, with no measurability assumed: the monotonicity of τ ↦ d(x, y_τ) is what makes the integrals meaningful. The time step is a real number r, entering the Moreau–Yosida approximation as r.toNNReal, so that the integrals are ordinary interval integrals.

Main results #

References #

source
theorem TauCeti.moreauYosida_add_le_of_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} {τ : NNReal} {z : X} (hz : z ∈ moreauYosidaResolvent φ τ x) (σ : NNReal) :
moreauYosida φ σ x + ↑(edist x z ^ 2 / (2 * ↑τ)) ≤ moreauYosida φ τ x + ↑(edist x z ^ 2 / (2 * ↑σ))

Comparison of Moreau–Yosida approximations at two time steps. If z ∈ J_τ x is a resolvent step, then z is a competitor for the Moreau–Yosida approximation at every other time step σ, which gives φ_σ(x) + d(x, z)² / (2τ) ≤ φ_τ(x) + d(x, z)² / (2σ).

source
theorem TauCeti.hasDerivAt_toReal_moreauYosida {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {r : ℝ} (hr : 0 < r) (hy : ∀ᶠ (s : ℝ) in nhds r, y s ∈ moreauYosidaResolvent φ s.toNNReal x) (hr₁ : moreauYosida φ r.toNNReal x ≠ ⊤) (hr₂ : moreauYosida φ r.toNNReal x ≠ ⊥) (hc : ContinuousAt (fun (s : ℝ) => (edist x (y s)).toReal) r) :
HasDerivAt (fun (s : ℝ) => (moreauYosida φ s.toNNReal x).toReal) (-(edist x (y r)).toReal ^ 2 / (2 * r ^ 2)) r

The derivative of the Moreau–Yosida approximation in the time step. Let y s ∈ J_s x be a resolvent step for all times s near r > 0, with φ_r(x) finite. If s ↦ d(x, y s) is continuous at r, then s ↦ φ_s(x) has derivative -d(x, y r)² / (2r²) at r.

source
theorem TauCeti.countable_not_hasDerivAt_toReal_moreauYosida {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {a b : ℝ} (ha : 0 ≤ a) (hy : ∀ r ∈ Set.Ioo a b, y r ∈ moreauYosidaResolvent φ r.toNNReal x) (ha' : moreauYosida φ a.toNNReal x ≠ ⊤) (hb' : moreauYosida φ b.toNNReal x ≠ ⊥) :
{r : ℝ | r ∈ Set.Ioo a b ∧ ¬HasDerivAt (fun (s : ℝ) => (moreauYosida φ s.toNNReal x).toReal) (-(edist x (y r)).toReal ^ 2 / (2 * r ^ 2)) r}.Countable

The derivative formula holds off a countable set. Let y r ∈ J_r x be a resolvent step for every time r in an interval (a, b) with a ≥ 0, and let φ_a(x) ≠ ⊤ and φ_b(x) ≠ ⊥. Then r ↦ φ_r(x) has derivative -d(x, y r)² / (2r²) at all but countably many r ∈ (a, b).

source
theorem TauCeti.moreauYosida_eq_add_integral {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {τ σ : ℝ} (hτ : 0 < τ) (hτσ : τ ≤ σ) (hy : ∀ r ∈ Set.Icc τ σ, y r ∈ moreauYosidaResolvent φ r.toNNReal x) (hτ' : moreauYosida φ τ.toNNReal x ≠ ⊤) (hσ' : moreauYosida φ σ.toNNReal x ≠ ⊥) :
moreauYosida φ τ.toNNReal x = moreauYosida φ σ.toNNReal x + ↑(∫ (r : ℝ) in τ..σ, (edist x (y r)).toReal ^ 2 / (2 * r ^ 2))

Integrated derivative formula. Let y r ∈ J_r x be a resolvent step for every time r ∈ [τ, σ], with 0 < τ, φ_τ(x) ≠ ⊤ and φ_σ(x) ≠ ⊥. Then φ_τ(x) = φ_σ(x) + ∫_τ^σ d(x, y r)² / (2r²) dr.

source
theorem TauCeti.tendsto_moreauYosida_nhdsGT_zero {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} (hφ : LowerSemicontinuousAt φ x) {σ : NNReal} (hσ : 0 < σ) (hσ' : moreauYosida φ σ x ≠ ⊥) :
Filter.Tendsto (fun (τ : NNReal) => moreauYosida φ τ x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))

Continuity of the Moreau–Yosida approximation at time zero. If φ is lower semicontinuous at x and φ_σ(x) ≠ ⊥ for some σ > 0, then φ_τ(x) → φ(x) as τ → 0⁺. This holds also when φ x = ⊤, and needs no resolvent steps.

source
theorem TauCeti.intervalIntegrable_edist_sq_div_of_forall_mem_moreauYosidaResolvent {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {σ : ℝ} (hσ : 0 < σ) (hy : ∀ r ∈ Set.Ioc 0 σ, y r ∈ moreauYosidaResolvent φ r.toNNReal x) (hx : φ x ≠ ⊤) (hσ' : moreauYosida φ σ.toNNReal x ≠ ⊥) :
IntervalIntegrable (fun (r : ℝ) => (edist x (y r)).toReal ^ 2 / (2 * r ^ 2)) MeasureTheory.volume 0 σ

The integrand d(x, y r)² / (2r²) of the De Giorgi energy identity is integrable on (0, σ], when y r ∈ J_r x for every r ∈ (0, σ], φ(x) ≠ ⊤ and φ_σ(x) ≠ ⊥.

source
theorem TauCeti.moreauYosida_add_integral_le {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {σ : ℝ} (hσ : 0 < σ) (hy : ∀ r ∈ Set.Ioc 0 σ, y r ∈ moreauYosidaResolvent φ r.toNNReal x) (hx : φ x ≠ ⊤) (hσ' : moreauYosida φ σ.toNNReal x ≠ ⊥) :
moreauYosida φ σ.toNNReal x + ↑(∫ (r : ℝ) in 0..σ, (edist x (y r)).toReal ^ 2 / (2 * r ^ 2)) ≤ φ x

De Giorgi energy inequality. Let y r ∈ J_r x be a resolvent step for every time r ∈ (0, σ], with φ(x) ≠ ⊤ and φ_σ(x) ≠ ⊥. Then φ_σ(x) + ∫₀^σ d(x, y r)² / (2r²) dr ≤ φ(x). Equality holds when φ is lower semicontinuous at x (TauCeti.moreauYosida_add_integral_eq).

source
theorem TauCeti.moreauYosida_add_integral_eq {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {σ : ℝ} (hφ : LowerSemicontinuousAt φ x) (hσ : 0 < σ) (hy : ∀ r ∈ Set.Ioc 0 σ, y r ∈ moreauYosidaResolvent φ r.toNNReal x) (hx : φ x ≠ ⊤) (hσ' : moreauYosida φ σ.toNNReal x ≠ ⊥) :
moreauYosida φ σ.toNNReal x + ↑(∫ (r : ℝ) in 0..σ, (edist x (y r)).toReal ^ 2 / (2 * r ^ 2)) = φ x

De Giorgi energy identity. Let φ be lower semicontinuous at x with φ(x) ≠ ⊤, and let y r ∈ J_r x be a resolvent step for every time r ∈ (0, σ], with φ_σ(x) ≠ ⊥. Then φ_σ(x) + ∫₀^σ d(x, y r)² / (2r²) dr = φ(x).

source
theorem TauCeti.moreauYosida_add_lintegral_descendingSlope_le {X : Type u_1} [EMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {σ : ℝ} (hσ : 0 < σ) (hy : ∀ r ∈ Set.Ioc 0 σ, y r ∈ moreauYosidaResolvent φ r.toNNReal x) (hx : φ x ≠ ⊤) (hσ' : moreauYosida φ σ.toNNReal x ≠ ⊥) :
moreauYosida φ σ.toNNReal x + ↑(∫⁻ (r : ℝ) in Set.Ioc 0 σ, descendingSlope φ (y r) ^ 2 / 2) ≤ φ x

Discrete energy–dissipation inequality. Let y r ∈ J_r x be a resolvent step for every time r ∈ (0, σ], with φ(x) ≠ ⊤ and φ_σ(x) ≠ ⊥. Then φ_σ(x) + ∫₀^σ |∂φ|²(y r) / 2 dr ≤ φ(x), where |∂φ| is the descending slope.

source
theorem TauCeti.apply_add_add_lintegral_descendingSlope_le {X : Type u_1} [EMetricSpace X] {φ : X → EReal} {x : X} {y : ℝ → X} {τ : NNReal} (hτ : 0 < τ) {z : X} (hz : z ∈ moreauYosidaResolvent φ τ x) (hy : ∀ r ∈ Set.Ioc 0 ↑τ, y r ∈ moreauYosidaResolvent φ r.toNNReal x) :
φ z + ↑(edist x z ^ 2 / (2 * ↑τ)) + ↑(∫⁻ (r : ℝ) in Set.Ioc 0 ↑τ, descendingSlope φ (y r) ^ 2 / 2) ≤ φ x

Discrete energy–dissipation inequality for one resolvent step. Let z ∈ J_τ x be a resolvent step with time step τ > 0, and let y r ∈ J_r x be a resolvent step for every time r ∈ (0, τ]. Then φ z + d(x, z)² / (2τ) + ∫₀^τ |∂φ|²(y r) / 2 dr ≤ φ(x), where |∂φ| is the descending slope. Unlike TauCeti.moreauYosida_add_lintegral_descendingSlope_le, no finiteness hypothesis is needed: the inequality is trivial when φ x = ⊤ or φ z = ⊥.