Generating the Pfaffian closure with total Pfaffian functions

GARETH JONES and PATRICK SPEISSEGGER

The paper concerns Pfaffian functions for which df/dx = P(x,f(x)) for a definable function P. Here we demonstrate formally that if f is the exponential function, then we can take P to be the projection on the second coordinate, Prod.snd which should be definable in pretty much all settings and has a name in Lean which does not require any import.

Q is a curried version of P.

def P : ℝ × ℝ → ℝ

Equations

• P = Prod.snd

noncomputable def f : ℝ → ℝ

Equations

• f = Real.exp

theorem P_satisfies_diffEq (x : ℝ) : deriv f x = P (x, f x)

def Q : ℝ → ℝ → ℝ

Equations

• Q x y = y

theorem Q_satisfies_diffEq (x : ℝ) : deriv f x = Q x (f x)