Optical flow equation: $\nabla I\cdot\mathbf V+\partial_t I=0$

Proved

ContinuityEqWiki.optical_flow_equation

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

continuity-equationmathematical-physics

Let $I(t,x,y)$ be an image intensity, $C^1$ jointly in time $t$ and image coordinates $(x,y)\in\mathbb R^2$ , and let $\mathbf V(t,x,y)=(V_x,V_y)$ be an optical flow velocity field. Let $t\mapsto p(t)\in\mathbb R^2$ be the image position of a moving object point, moving with the flow: $p'(t)=\mathbf V(t,p(t))$ for all $t$ . Assume brightness constancy: $I(t,p(t))$ does not depend on $t$ . Then for every $t$ , at the point $(t,p(t))$ ,

\frac{\partial I}{\partial x}V_x+\frac{\partial I}{\partial y}V_y+\frac{\partial I}{\partial t}=\nabla I\cdot\mathbf V+\frac{\partial I}{\partial t}=0 .

Formalization Note The source's discrete assumption ("brightness of the moving object did not change between two image frames") is encoded in its continuous-time form: the intensity is constant along the trajectory of the moving point, and the equation is asserted along that trajectory.

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem optical_flow_equation (I : ℝ → (Fin 2 → ℝ) → ℝ) (V : ℝ → (Fin 2 → ℝ) → Fin 2 → ℝ)
    (p : ℝ → Fin 2 → ℝ) (hI : ContDiff ℝ 1 (Function.uncurry I))
    (hp : ∀ t, HasDerivAt p (V t (p t)) t)
    (brightness_constancy : ∀ s t, I s (p s) = I t (p t)) :
    ∀ t, partialDeriv 0 (I t) (p t) * V t (p t) 0 + partialDeriv 1 (I t) (p t) * V t (p t) 1
      + timeDeriv I t (p t) = 0 := by sorry

end ContinuityEqWiki

Source

Wikipedia, "Continuity equation", revision oldid=1378634825, https://en.wikipedia.org/w/index.php?title=Continuity_equation&oldid=1378634825, section "Computer vision" (optical flow equation)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, non-blind read-back

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, at the explicit request of the proposal owner. Its author knew the source text and the intended meaning while writing it, so it must not be mistaken for a blind, independent audit. Reviewers should compare the Lean code against the source themselves.

Let $I:\mathbb R\times\mathbb R^2\to\mathbb R$ , $\mathbf V:\mathbb R\times\mathbb R^2\to\mathbb R^2$ and $p:\mathbb R\to\mathbb R^2$ be arbitrary maps. Assume:

$(t,z)\mapsto I(t,z)$ is $C^1$ on $\mathbb R\times\mathbb R^2$ ;
for every $t$ , $p$ is differentiable at $t$ with derivative $p'(t)=\mathbf V(t,p(t))$ ;
for all $s,t$ : $I(s,p(s))=I(t,p(t))$ .

No regularity is assumed on $\mathbf V$ . Conclusion: for every $t$ ,

\partial_0 I(t,\cdot)(p(t))\,\mathbf V(t,p(t))_0+\partial_1 I(t,\cdot)(p(t))\,\mathbf V(t,p(t))_1+\partial_t I(t,p(t))=0,

where $\partial_0,\partial_1$ are the partial derivatives in the two image coordinates and $\partial_tI(t,z)$ is the derivative of $s\mapsto I(s,z)$ at $t$ . The identity is asserted only at points of the form $(t,p(t))$ .

View graph

Optical flow equation: ∇I⋅V+∂tI=0\nabla I\cdot\mathbf V+\partial_t I=0∇I⋅V+∂t​I=0

Optical flow equation: $\nabla I\cdot\mathbf V+\partial_t I=0$