Minimizing Movement (JKO-type scheme)

This file implements the minimizing movement scheme (JKO scheme) for gradient flows in general metric spaces, without dependency on measure theory.

Main definitions

• MmFunctional: The functional to minimize at each time step
• IsMinimizer: Predicate for being a minimizer
• MmStep: Single step of the minimizing movement scheme
• MmCurve: Discrete curve obtained from the scheme

Main results

• mm_step_exists: Existence of minimizers under appropriate assumptions
• Energy decrease and a priori estimates for the scheme

def Frourio.distSquared {X : Type u_1} [PseudoMetricSpace X] (x y : X) : ℝ

Squared distance function for convenience.

Equations

• Frourio.distSquared x y = dist x y ^ 2

noncomputable def Frourio.MmFunctional {X : Type u_1} [PseudoMetricSpace X] (τ : ℝ) (F : X → ℝ) (xPrev x : X) : ℝ

The functional to minimize in the minimizing movement scheme. MmFunctional τ F xPrev x = F(x) + (1/(2τ)) * d²(x, xPrev)

Equations

• Frourio.MmFunctional τ F xPrev x = F x + 1 / (2 * τ) * Frourio.distSquared x xPrev

def Frourio.IsMinimizer {Y : Type u_2} (f : Y → ℝ) (x : Y) : Prop

A point is a minimizer if it achieves the minimum value of the functional.

Equations

• Frourio.IsMinimizer f x = ∀ (y : Y), f x ≤ f y

def Frourio.MmStep {X : Type u_1} [PseudoMetricSpace X] (τ : ℝ) (F : X → ℝ) (xPrev x : X) : Prop

A single step of the minimizing movement scheme.

Equations

• Frourio.MmStep τ F xPrev x = Frourio.IsMinimizer (Frourio.MmFunctional τ F xPrev) x

def Frourio.MmProper {X : Type u_1} (F : X → ℝ) : Prop

The functional F is proper if it takes finite values somewhere.

Equations

• Frourio.MmProper F = ∃ (x : X), F x ≠ 0

def Frourio.MmCoercive {X : Type u_1} [PseudoMetricSpace X] [Nonempty X] (F : X → ℝ) : Prop

The functional F is coercive if it grows to infinity at infinity.

Equations

• Frourio.MmCoercive F = ∀ (c : ℝ), ∃ (r : ℝ), ∀ (x : X), dist x (Classical.arbitrary X) > r → F x > c

def Frourio.MmCompactSublevels {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) : Prop

The functional F has compact sublevels if its sublevel sets are relatively compact.

Equations

• Frourio.MmCompactSublevels F = ∀ (c : ℝ), IsCompact {x : X | F x ≤ c}

structure Frourio.MmCurve {X : Type u_1} [PseudoMetricSpace X] (τ : ℝ) (F : X → ℝ) (x0 : X) : Type u_1

Discrete curve obtained from the minimizing movement scheme.

• points : ℕ → X

  The discrete points at times nτ

• init : self.points 0 = x0

  Initial condition

• step (n : ℕ) : MmStep τ F (self.points n) (self.points (n + 1))

  Each point is obtained by minimizing movement

noncomputable def Frourio.MmCurve.interpolate {X : Type u_1} [PseudoMetricSpace X] {τ : ℝ} {F : X → ℝ} {x0 : X} (curve : MmCurve τ F x0) (t : ℝ) : X

Linear interpolation between discrete points for continuous extension.

Equations

• curve.interpolate t = if t ≤ 0 then x0 else let n := ⌊t / τ⌋.toNat; let s := (t - ↑n * τ) / τ; if s = 0 then curve.points n else curve.points n

theorem Frourio.mm_energy_decrease {X : Type u_1} [PseudoMetricSpace X] {τ : ℝ} (hτ : 0 < τ) {F : X → ℝ} {xPrev x : X} (h : MmStep τ F xPrev x) : F x ≤ F xPrev

Energy decrease along the minimizing movement scheme.

theorem Frourio.mm_distance_estimate {X : Type u_1} [PseudoMetricSpace X] {τ : ℝ} (hτ : 0 < τ) {F : X → ℝ} {xPrev x : X} (h : MmStep τ F xPrev x) : distSquared x xPrev ≤ 2 * τ * (F xPrev - F x)

A priori estimate on distance for the minimizing movement scheme.

theorem Frourio.sublevel_closed_of_lsc {X : Type u_1} [PseudoMetricSpace X] {F : X → ℝ} (hF : LowerSemicontinuous F) (c : ℝ) : IsClosed {x : X | F x ≤ c}

Helper: sublevel sets are closed for lower semicontinuous functions.

theorem Frourio.lsc_bddBelow_on_compact {X : Type u_1} [PseudoMetricSpace X] {f : X → ℝ} {K : Set X} (hK_compact : IsCompact K) (_hK_nonempty : K.Nonempty) (hf_lsc : LowerSemicontinuous f) : BddBelow (f '' K)

Helper: A lower semicontinuous function on a compact set is bounded below.

theorem Frourio.exists_approx_min_on_compact {X : Type u_1} [PseudoMetricSpace X] {f : X → ℝ} {K : Set X} (hK_compact : IsCompact K) (hK_nonempty : K.Nonempty) (hf_lsc : LowerSemicontinuous f) (ε : ℝ) : ε > 0 → ∃ x ∈ K, f x < sInf (f '' K) + ε

Helper: For the infimum m of f on K, we can find points arbitrarily close to m.

theorem Frourio.lsc_attains_min_on_compact {X : Type u_1} [PseudoMetricSpace X] {f : X → ℝ} {K : Set X} (hK_compact : IsCompact K) (hK_nonempty : K.Nonempty) (hf_lsc : LowerSemicontinuous f) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y

A lower semicontinuous real-valued function on a non-empty compact set attains its infimum. This is a special case of the Weierstrass extreme value theorem.

theorem Frourio.mm_step_exists {X : Type u_1} [PseudoMetricSpace X] {τ : ℝ} (hτ : 0 < τ) {F : X → ℝ} {xPrev : X} (hF_lsc : LowerSemicontinuous F) (hF_proper : MmProper F) (hF_compact : MmCompactSublevels F) : ∃ (x : X), MmStep τ F xPrev x

Existence of minimizers for the minimizing movement step.

theorem Frourio.mm_curve_energy_dissipation {X : Type u_1} [PseudoMetricSpace X] {τ : ℝ} (hτ : 0 < τ) {F : X → ℝ} {x0 : X} (curve : MmCurve τ F x0) (n : ℕ) : F (curve.points n) ≤ F x0

Energy dissipation inequality for a discrete curve.

theorem Frourio.mm_curve_distance_sum {X : Type u_1} [PseudoMetricSpace X] {τ : ℝ} (hτ : 0 < τ) {F : X → ℝ} {x0 : X} (curve : MmCurve τ F x0) (N : ℕ) : ∑ n ∈ Finset.range N, distSquared (curve.points (n + 1)) (curve.points n) ≤ 2 * τ * (F x0 - F (curve.points N))

Sum of squared distances is bounded by initial energy difference.