Fokker–Planck equation

DefinitionFree energy of a Fokker–Planck density#✓fully proved

The free energy F(t) = ∫ₐᵇ (Ψ p + D p log p) dx of the density p(t, ·) on [a, b] (potential Ψ, diffusion coefficient D).

noncomputable def freeEnergy (Ψ : ℝ → ℝ) (D a b : ℝ) (p : ℝ → ℝ → ℝ) (t : ℝ) : ℝ :=
  ∫ x in a..b, (Ψ x * p t x + D * (p t x * Real.log (p t x)))

Used by 2

Used byFree-energy decay · Dissipation identity

DefinitionNegative probability flux of the Fokker–Planck equation#✓fully proved

The (negative) probability flux p Ψ' + D ∂ₓ p of the gradient-drift Fokker–Planck equation at (t, x); the flux itself is -(p Ψ' + D ∂ₓ p).

noncomputable def negFlux (Ψ : ℝ → ℝ) (D : ℝ) (p : ℝ → ℝ → ℝ) (t x : ℝ) : ℝ :=
  p t x * deriv Ψ x + D * deriv (fun y => p t y) x

Used by 3

Used byDissipation identity · Mass conservation · No-flux solution of the gradient-drift Fokker–Planck equation

StructureNo-flux solution of the gradient-drift Fokker–Planck equation#✓fully proved

p solves the gradient-drift Fokker–Planck equation ∂ₜ p = ∂ₓ (p Ψ' + D ∂ₓ p) on [a, b] with zero flux at both ends, for times t ∈ I.

structure IsNoFluxSolutionOn (Ψ : ℝ → ℝ) (D a b : ℝ) (I : Set ℝ) (p : ℝ → ℝ → ℝ) : Prop where
  /-- The Fokker–Planck equation on `[a, b]`. -/
  pde : ∀ t ∈ I, ∀ x ∈ Icc a b, deriv (fun s => p s x) t = deriv (negFlux Ψ D p t) x
  /-- Zero flux at the left end. -/
  flux_left : ∀ t ∈ I, negFlux Ψ D p t a = 0
  /-- Zero flux at the right end. -/
  flux_right : ∀ t ∈ I, negFlux Ψ D p t b = 0

Uses 1 · Used by 3

Statement usesNegative probability flux of the Fokker–Planck equation

Used byFree-energy decay · Dissipation identity · Mass conservation

TheoremDissipation identity#✓fully proved

Let p be C² in (t, x), positive for times in an open set I, and solve the no-flux gradient-drift Fokker–Planck equation on [a, b] for t ∈ I, with C² potential Ψ (any real D). Then for t ∈ I, F'(t) = -∫ₐᵇ p (Ψ' + D ∂ₓ log p)² dx. Only the values of p on [a, b] enter F; positivity is asked of the whole C² function p t so that log (p t) is C².

theorem hasDerivAt_freeEnergy {Ψ : ℝ → ℝ} {D a b : ℝ} {I : Set ℝ} {p : ℝ → ℝ → ℝ}
    (hab : a ≤ b) (hI : IsOpen I) (hΨ : ContDiff ℝ 2 Ψ) (hp : ContDiff ℝ 2 (Function.uncurry p))
    (hpos : ∀ t ∈ I, ∀ x, 0 < p t x) (hsol : IsNoFluxSolutionOn Ψ D a b I p) {t : ℝ}
    (ht : t ∈ I) :
    HasDerivAt (freeEnergy Ψ D a b p)
      (-∫ x in a..b, p t x * (deriv Ψ x + D * deriv (fun y => Real.log (p t y)) x) ^ 2) t

Uses 3 · Used by 1

Statement usesNo-flux solution of the gradient-drift Fokker–Planck equation · Free energy of a Fokker–Planck density

Proof usesNegative probability flux of the Fokker–Planck equation

Used byFree-energy decay

TheoremFree-energy decay#✓fully proved

Under the hypotheses of hasDerivAt_freeEnergy, on a convex open time set I the free energy is nonincreasing.

theorem antitoneOn_freeEnergy {Ψ : ℝ → ℝ} {D a b : ℝ} {I : Set ℝ} {p : ℝ → ℝ → ℝ}
    (hab : a ≤ b) (hI : IsOpen I) (hIc : Convex ℝ I) (hΨ : ContDiff ℝ 2 Ψ)
    (hp : ContDiff ℝ 2 (Function.uncurry p)) (hpos : ∀ t ∈ I, ∀ x, 0 < p t x)
    (hsol : IsNoFluxSolutionOn Ψ D a b I p) : AntitoneOn (freeEnergy Ψ D a b p) I

Uses 3

Statement usesNo-flux solution of the gradient-drift Fokker–Planck equation · Free energy of a Fokker–Planck density

Proof usesDissipation identity

TheoremMass conservation#✓fully proved

If p is C² and solves the no-flux equation on [a, b] for times in I (positivity is not needed), the total mass ∫ₐᵇ p(t, x) dx has zero time derivative at every t ∈ I.

theorem hasDerivAt_mass {Ψ : ℝ → ℝ} {D a b : ℝ} {I : Set ℝ} {p : ℝ → ℝ → ℝ} (hab : a ≤ b)
    (hΨ : ContDiff ℝ 2 Ψ) (hp : ContDiff ℝ 2 (Function.uncurry p))
    (hsol : IsNoFluxSolutionOn Ψ D a b I p) {t : ℝ} (ht : t ∈ I) :
    HasDerivAt (fun s => ∫ x in a..b, p s x) 0 t

Uses 2

Statement usesNo-flux solution of the gradient-drift Fokker–Planck equation

Proof usesNegative probability flux of the Fokker–Planck equation

DefinitionPartial derivative on Euclidean coordinate space#✓fully proved

The partial derivative ∂ᵢ f (x) = Df(x) eᵢ on Fin n → ℝ.

noncomputable def pderiv (i : Fin n) (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ :=
  fderiv ℝ f x (Pi.single i 1)

Used by 9

Used byDivergence of a vector field · Rotational drifts share the Gibbs stationary density · Identifiability of the potential · Probability flux of a diffusion · The Gibbs density has zero flux · Flux of the Gibbs density under a rotational gradient drift · The Gibbs density is stationary · Gradient of a function on Euclidean coordinate space · A zero-flux density determines the drift

DefinitionGradient of a function on Euclidean coordinate space#✓fully proved

The gradient ∇f(x) = (∂ᵢ f(x))ᵢ.

noncomputable def grad (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : Fin n → ℝ :=
  fun i => pderiv i f x

Uses 1 · Used by 7

Statement usesPartial derivative on Euclidean coordinate space

Used byRotational drifts share the Gibbs stationary density · Identifiability of the potential · An explicit rotational drift with nonzero flux · The Gibbs density has zero flux · Flux of the Gibbs density under a rotational gradient drift · The Gibbs density is stationary · A zero-flux density determines the drift

DefinitionDivergence of a vector field#✓fully proved

The divergence div F (x) = ∑ᵢ ∂ᵢ Fᵢ (x) of a vector field.

noncomputable def divergence (F : (Fin n → ℝ) → Fin n → ℝ) (x : Fin n → ℝ) : ℝ :=
  ∑ i, pderiv i (fun y => F y i) x

Uses 1 · Used by 4

Statement usesPartial derivative on Euclidean coordinate space

Used byRotational drifts share the Gibbs stationary density · An explicit rotational drift with nonzero flux · Fokker–Planck operator · The Gibbs density is stationary

DefinitionProbability flux of a diffusion#✓fully proved

The probability flux J = b p - D ∇p of the diffusion dX = b dt + √(2D) dW with density p.

noncomputable def flux (D : ℝ) (b : (Fin n → ℝ) → Fin n → ℝ) (p : (Fin n → ℝ) → ℝ)
    (x : Fin n → ℝ) : Fin n → ℝ :=
  fun i => b x i * p x - D * pderiv i p x

Uses 1 · Used by 8

Statement usesPartial derivative on Euclidean coordinate space

Used byRotational drifts share the Gibbs stationary density · Identifiability of the potential · An explicit rotational drift with nonzero flux · The Gibbs density has zero flux · Flux of the Gibbs density under a rotational gradient drift · Fokker–Planck operator · The Gibbs density is stationary · A zero-flux density determines the drift

DefinitionFokker–Planck operator#✓fully proved

The Fokker–Planck operator -div J: the density evolves by ∂ₜ p = fokkerPlanckOp D b p, and p is stationary iff this vanishes.

noncomputable def fokkerPlanckOp (D : ℝ) (b : (Fin n → ℝ) → Fin n → ℝ) (p : (Fin n → ℝ) → ℝ)
    (x : Fin n → ℝ) : ℝ :=
  -divergence (flux D b p) x

Uses 2 · Used by 1

Statement usesDivergence of a vector field · Probability flux of a diffusion

Used byThe Gibbs density is stationary

DefinitionGibbs density#✓fully proved

The (unnormalized) Gibbs density e^{-Ψ(x) / D}.

noncomputable def gibbs (Ψ : (Fin n → ℝ) → ℝ) (D : ℝ) (x : Fin n → ℝ) : ℝ :=
  Real.exp (-Ψ x / D)

Used by 5

Used byRotational drifts share the Gibbs stationary density · An explicit rotational drift with nonzero flux · The Gibbs density has zero flux · Flux of the Gibbs density under a rotational gradient drift · The Gibbs density is stationary

TheoremThe Gibbs density has zero flux#✓fully proved

The Gibbs density has zero flux under the gradient drift -∇Ψ: for differentiable Ψ, D ≠ 0 and any constant c, J = -∇Ψ · c e^{-Ψ/D} - D ∇(c e^{-Ψ/D}) = 0.

theorem flux_gibbs_eq_zero {Ψ : (Fin n → ℝ) → ℝ} (hΨ : Differentiable ℝ Ψ) {D : ℝ}
    (hD : D ≠ 0) (c : ℝ) : flux D (fun x => -grad Ψ x) (fun x => c * gibbs Ψ D x) = 0

Uses 4 · Used by 1

Statement usesProbability flux of a diffusion · Gibbs density · Gradient of a function on Euclidean coordinate space

Proof usesPartial derivative on Euclidean coordinate space

Used byThe Gibbs density is stationary

TheoremThe Gibbs density is stationary#✓fully proved

The Gibbs density is stationary for the gradient drift: -div J = 0.

theorem fokkerPlanckOp_gibbs_eq_zero {Ψ : (Fin n → ℝ) → ℝ} (hΨ : Differentiable ℝ Ψ) {D : ℝ}
    (hD : D ≠ 0) (c : ℝ) (x : Fin n → ℝ) :
    fokkerPlanckOp D (fun x => -grad Ψ x) (fun x => c * gibbs Ψ D x) x = 0

Uses 7

Statement usesFokker–Planck operator · Gibbs density · Gradient of a function on Euclidean coordinate space

Proof usesDivergence of a vector field · Probability flux of a diffusion · The Gibbs density has zero flux · Partial derivative on Euclidean coordinate space

TheoremA zero-flux density determines the drift#✓fully proved

If p > 0 is differentiable and the gradient drift -∇Ψ has zero flux for p, then ∂ᵢ Ψ = -D ∂ᵢ log p.

theorem pderiv_eq_of_flux_eq_zero {Ψ p : (Fin n → ℝ) → ℝ} {D : ℝ} (hp : Differentiable ℝ p)
    (hpos : ∀ x, 0 < p x) (h : flux D (fun x => -grad Ψ x) p = 0) (i : Fin n)
    (x : Fin n → ℝ) : pderiv i Ψ x = -D * pderiv i (fun y => Real.log (p y)) x

Uses 3 · Used by 1

Statement usesProbability flux of a diffusion · Gradient of a function on Euclidean coordinate space · Partial derivative on Euclidean coordinate space

Used byIdentifiability of the potential

TheoremIdentifiability of the potential#✓fully proved

Two differentiable potentials whose gradient drifts both have zero flux for the same positive differentiable density differ by a constant.

theorem exists_const_of_flux_eq_zero {Ψ₁ Ψ₂ p : (Fin n → ℝ) → ℝ} {D : ℝ}
    (hΨ₁ : Differentiable ℝ Ψ₁) (hΨ₂ : Differentiable ℝ Ψ₂) (hp : Differentiable ℝ p)
    (hpos : ∀ x, 0 < p x) (h₁ : flux D (fun x => -grad Ψ₁ x) p = 0)
    (h₂ : flux D (fun x => -grad Ψ₂ x) p = 0) : ∃ C, ∀ x, Ψ₁ x = Ψ₂ x + C

Uses 4

Statement usesProbability flux of a diffusion · Gradient of a function on Euclidean coordinate space

Proof usesPartial derivative on Euclidean coordinate space · A zero-flux density determines the drift

TheoremFlux of the Gibbs density under a rotational gradient drift#✓fully proved

The flux of the Gibbs density under the drift -(∇Ψ + A ∇Ψ) is the rotational part -(A ∇Ψ) e^{-Ψ / D} (for differentiable Ψ, D ≠ 0, any matrix A).

theorem flux_rotational_gibbs {Ψ : (Fin n → ℝ) → ℝ} (hΨ : Differentiable ℝ Ψ) {D : ℝ}
    (hD : D ≠ 0) (A : Matrix (Fin n) (Fin n) ℝ) (y : Fin n → ℝ) (i : Fin n) :
    flux D (fun y => -(grad Ψ y + A.mulVec (grad Ψ y))) (gibbs Ψ D) y i =
      -(A.mulVec (grad Ψ y) i * gibbs Ψ D y)

Uses 4 · Used by 1

Statement usesProbability flux of a diffusion · Gibbs density · Gradient of a function on Euclidean coordinate space

Proof usesPartial derivative on Euclidean coordinate space

Used byAn explicit rotational drift with nonzero flux

TheoremRotational drifts share the Gibbs stationary density#✓fully proved

Rotational drifts share the Gibbs stationary density (non-identifiability): for a C² potential Ψ, D ≠ 0 and an antisymmetric matrix A (Aᵀ = -A), the drift -(∇Ψ + A ∇Ψ) satisfies div J = 0 for p = e^{-Ψ / D}.

theorem divergence_flux_rotational_gibbs {Ψ : (Fin n → ℝ) → ℝ} (hΨ : ContDiff ℝ 2 Ψ) {D : ℝ}
    (hD : D ≠ 0) {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.transpose = -A) (x : Fin n → ℝ) :
    divergence (flux D (fun y => -(grad Ψ y + A.mulVec (grad Ψ y))) (gibbs Ψ D)) x = 0

Uses 5 · Used by 1

Statement usesDivergence of a vector field · Probability flux of a diffusion · Gibbs density · Gradient of a function on Euclidean coordinate space

Proof usesPartial derivative on Euclidean coordinate space

Used byAn explicit rotational drift with nonzero flux

TheoremAn explicit rotational drift with nonzero flux#✓fully proved

An explicit rotational drift with nonzero flux (our derivation): on ℝ² with Ψ(x) = (x₀² + x₁²) / 2, D = 1 and the rotation generator A = [[0, 1], [-1, 0]], the drift -(∇Ψ + A ∇Ψ) has the Gibbs (standard Gaussian, up to normalization) density as a stationary density, yet its flux at (1, 0) is nonzero, so it is not the gradient drift.

theorem exists_rotational_flux_ne_zero :
    let Ψ : (Fin 2 → ℝ) → ℝ := fun x => (x 0 ^ 2 + x 1 ^ 2) / 2
    let A : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; -1, 0]
    (∀ x, divergence (flux 1 (fun y => -(grad Ψ y + A.mulVec (grad Ψ y))) (gibbs Ψ 1)) x = 0) ∧
      flux 1 (fun y => -(grad Ψ y + A.mulVec (grad Ψ y))) (gibbs Ψ 1) ![1, 0] ≠ 0

Uses 6

Statement usesDivergence of a vector field · Probability flux of a diffusion · Gibbs density · Gradient of a function on Euclidean coordinate space

Proof usesRotational drifts share the Gibbs stationary density · Flux of the Gibbs density under a rotational gradient drift

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.