1.4 · Book p. 31 · PDF p. 43

The Langevin SDE as a Wasserstein Gradient Flow

Interprets the Fokker-Planck evolution of Langevin diffusion as gradient flow of relative entropy in Wasserstein space.

Open this section in the canonical August 9 source ↗

Displayed identity (1.4.7)

Geodesic alpha-convexity implies the first-order lower bound at the initial endpoint, with the derivative pairing and alpha times squared distance correction.

\[\mathcal F(\nu)\ge\mathcal F(\mu)+\left.\frac{d}{dt}\mathcal F(\mu_t)\right|_{t=0^+}+\frac{\alpha}{2}W_2^2(\mu,\nu)\]

Proof

\[\mathcal F(\mu_t)\le(1-t)\mathcal F(\mu)+t\mathcal F(\nu)-\frac{\alpha}{2}t(1-t)W_2^2(\mu,\nu)\]

Lean firstOrder_geodesicConvexity

\[\frac{\mathcal F(\mu_t)-\mathcal F(\mu)}{t}\le\mathcal F(\nu)-\mathcal F(\mu)-\frac{\alpha}{2}(1-t)W_2^2(\mu,\nu)\]

Lean firstOrder_geodesicConvexity

\[t\downarrow0\quad\Longrightarrow\quad\mathcal F(\nu)\ge\mathcal F(\mu)+\left.\frac{d}{dt}\mathcal F(\mu_t)\right|_{0^+}+\frac{\alpha}{2}W_2^2(\mu,\nu)\]

Lean firstOrder_geodesicConvexity

Apply the chord inequality at a positive interpolation time t, subtract the initial value, and divide by t. As t decreases to zero, the secant slope converges to the derivative along the geodesic and the correction converges to alpha times the squared endpoint distance divided by two.

Why is this valid?

A selected geodesic must satisfy the compiled chord formulation, and the path composition t maps to F(path t) must have derivative gradientPairing at zero. In a Wasserstein application, the separate geometric identification sets this scalar to the source inner product with the optimal displacement.

Source assumptions

an alpha-geodesically convex smooth functional
a constant-speed geodesic from mu to nu
the Riemannian derivative-gradient pairing

Formal assumptions

the compiled endpoint chord inequality on every selected geodesic
HasDerivAt of the functional along the selected path at zero

View Lean formalization

compiled · faithful paraphrase

ASTIS formalizes the positive-time secant limit with HasDerivAt.tendsto_slope and transports the eventual inequality through both limits using the closed order on the reals.

`AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Geometry/GeodesicConvexity.lean:40

theorem firstOrder_geodesicConvexity
    {M : Type*} [MetricSpace M]
    {isGeodesic : (ℝ → M) → Prop} {F : M → ℝ} {alpha : ℝ}
    (hconvex : IsAlphaGeodesicallyConvex isGeodesic F alpha)
    {path : ℝ → M} (hpath : isGeodesic path)
    {gradientPairing : ℝ}
    (hderiv : HasDerivAt (fun t => F (path t)) gradientPairing 0) :
    F (path 1) ≥
      F (path 0) + gradientPairing +
        alpha / 2 * dist (path 0) (path 1) ^ 2 := by
  let phi : ℝ → ℝ := fun t => F (path t)
  let upper : ℝ → ℝ := fun t =>
    F (path 1) - F (path 0) -
      alpha * (1 - t) / 2 * dist (path 0) (path 1) ^ 2
  have hslope :
      Tendsto (slope phi 0) (𝓝[>] 0) (𝓝 gradientPairing) := by
    apply hderiv.tendsto_slope.mono_left
    apply nhdsWithin_mono
    intro t ht
    simpa only [mem_compl_iff, mem_singleton_iff] using ne_of_gt ht
  have hupper :
      Tendsto upper (𝓝[>] 0) (𝓝 (upper 0)) := by
    have hcontinuous : ContinuousAt upper 0 := by
      dsimp only [upper]
      fun_prop
    have hfilter : 𝓝[>] (0 : ℝ) ≤ 𝓝 0 := inf_le_left
    exact hcontinuous.tendsto.mono_left hfilter
  have hslope_le : slope phi 0 ≤ᶠ[𝓝[>] 0] upper := by
    filter_upwards [self_mem_nhdsWithin,
      (eventually_lt_nhds zero_lt_one).filter_mono inf_le_left]
      with t ht htle
    have htpos : 0 < t := ht
    have hchord := hconvex path hpath t ⟨htpos.le, htle.le⟩
    have hquotient :
        (F (path t) - F (path 0)) / t ≤ upper t := by
      apply (div_le_iff₀ htpos).2
      dsimp only [upper]
      nlinarith
    rw [div_eq_inv_mul] at hquotient
    simpa [phi, slope, htpos.ne'] using hquotient
  have hfirst := le_of_tendsto_of_tendsto hslope hupper hslope_le
  dsimp only [upper, sub_zero, one_mul] at hfirst
  linarith

end GeodesicConvexity
end Geometry
end TechnicalLemmas
end AutoSamplingTheory

Imports

Mathlib.Analysis.Calculus.Deriv.Slope
Mathlib.Topology.MetricSpace.Basic

Local dependencies

IsAlphaGeodesicallyConvex

Downstream consumers

gradient-flow contraction
Polyak-Lojasiewicz and quadratic-growth consequences