Documentation

Marginis.JonesSpeisegger2012

Generating the Pfaffian closure with total Pfaffian functions #

by 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
Instances For
    noncomputable def f :
    Equations
    Instances For
      theorem P_satisfies_diffEq (x : ) :
      deriv f x = P (x, f x)
      def Q :
      Equations
      Instances For
        theorem Q_satisfies_diffEq (x : ) :
        deriv f x = Q x (f x)