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 ↗

Formal topologyOpen this section in the underlying Lean graph↗

Displayed identity (1.4.7)

book 34 / PDF 46 · faithful paraphrase

Statement

\[\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)\]

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

Lean statement · firstOrder_geodesicConvexity

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

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

Exact module and namespace context

Proof / derivation

Source-faithful equation route; notation is normalized but the argument is not replaced by an ASTIS 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)\]

\[\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)\]

\[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)\]

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

The source argument is restated here as a strict ASTIS LaTeX packet before the Lean correspondence.

\[\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)\]

\[\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)\]

\[\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)\]

\[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 proof · firstOrder_geodesicConvexity

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.firstOrder_geodesicConvexity

Underlying proof leaves

firstOrder_geodesicConvexity

Chewi source ↗

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