Partial Derivatives

Stream: new members

[Ryland Gross]

Hi all,

It's very nice to introduce myself to the Zulip Chat. I'm Ryland, an undergraduate math student currently taking a class on Lean4. I'm experimenting on the side trying to do some work on Partial Derivatives since I saw they still had not been added to Mathlib.

I've been learning about Frechet Derivatives through Wikipedia and Mathlib and I think I have successfully implemented some of them in a more exact case dealing with R^n, but I also think I can implement them for the more general addcommgroup, k module, topological space version too.

Do you all have any advice on how I should best proceed to keep working on this, even if it is just for my own edification // personal project with lean? I'm under the impression that we are stylistically trying to make everything as general as possible, is the way I described enough?

Thanks!

[Ryland Gross]

Sorry forgot to mention (my goal is to eventually prove Clairaut's Theorem)

[Bryan Wang]

Hi Ryland :) I think (correct me if wrong) I have seen one version of Clairaut's theorem as docs#Convex.second_derivative_within_at_symmetric

[Tomas Skrivan]

The topic of partial derivatives came up multiple times and always fizzles out as people experienced with Lean don't really need them. Some time ago I wrote a guide to partial derivatives, it might clarify a thing or two.

[Jireh Loreaux]

@Anne Baanen the guide to partial derivatives that Tomas Skrivan wrote and linked above was supposed to eventually make it onto the community website, but that never happened. Can you add that as a TODO item for the website overhaul? To be clear, I'm not asking you to do the work to add it to the website, only to add it as a tracked item on that document.

[Anne Baanen]

Wow, this is great! I'll definitely ensure this gets a proper page.

[Tomas Skrivan]

Ok I made a PR, but I just quickly copy pasted the post https://github.com/leanprover-community/leanprover-community.github.io/pull/800 Maybe it should go to MIL, I don't really know where it would be easier to find.

[Tomas Skrivan]

Btw there is inactive PR for partial derivatives notation #25427 it might be worth resurrecting and mention it in the guide.

[Tomas Skrivan]

Here is my take on partial derivative notation:

-- Index in brackets → EuclideanSpace.single i 1 direction, field ℝ
#check ∂[i] (f · y) x                      -- (∂[i] (f · y)) x = fderiv ℝ (f · y) x (single i 1)
#check ∂[i] x'', (f x'' y)                 -- fun x'' => fderiv ℝ ... x'' (single i 1)
#check ∂[i] (x'' := x), (f x'' y)          -- fderiv ℝ ... x (single i 1)

-- Numeric literal as index (isFin short-circuits on nat literals)
variable [NeZero n]
#check ∂[0] (f · y) x                       -- fderiv ℝ (f · y) x (single (0 : Fin n) 1)

-- Field + index
#check ∂[ℂ, i] (g · y') x'                 -- fderiv ℂ (g · y') x' (single i 1)

-- Field only → curried CLM-map; normal application gives the CLM at a point
#check ∂[ℝ] (f · y)                         -- fderiv ℝ (f · y)  :  _ → _ →L[ℝ] _
#check ∂[ℝ] (f · y) x                       -- (∂[ℝ] (f · y)) x  :  _ →L[ℝ] _
#check ∂[ℝ] x'', (f x'' y)                 -- fun x'' => fderiv ℝ (fun x'' => f x'' y) x''
#check ∂[ℝ] (x'' := x), (f x'' y)          -- fderiv ℝ (fun x'' => f x'' y) x
#check ∂[ℝ] (x'' := x; dx), (f x'' y)      -- fderiv ℝ (fun x'' => f x'' y) x dx

-- No brackets → defaults to ℝ
#check ∂ (f · y)                             -- fderiv ℝ (f · y)
#check ∂ (f · y) x                           -- (∂ (f · y)) x

-- second derivative
#check ∂ ∂ (f · y)
#check ∂ (x':=x), ∂ (x'':=x'), (f x'' y)

code

import Mathlib

open Lean Lean.Elab Lean.Elab.Term Lean.Meta

declare_syntax_cat partialHead
declare_syntax_cat partialBody

-- Head forms
syntax term ", " term : partialHead    -- `𝕜, i`
syntax term           : partialHead    -- `𝕜`  or  `i`  (elaborator decides)

-- Body forms: only the non-application cases.
-- `∂ f x` is handled by parsing `∂ f` as a term and letting Lean apply `x`.
syntax ident ", " term                                       : partialBody
syntax "(" ident " := " term ")" ", " term                 : partialBody
syntax "(" ident " := " term " ; " term ")" ", " term     : partialBody

-- partialBody forms (tried first due to definition order)
syntax (name := «∂Plain»)        "∂"                    partialBody : term
syntax (name := «∂Bracketed»)    "∂[" partialHead "]"   partialBody : term
-- function forms (fallback when partialBody doesn't match)
-- `syntax:max` makes the result atom-level, so `∂ f x` parses as `(∂ f) x`
syntax:max (name := «∂PlainFun»)     "∂"                    term:arg    : term
syntax:max (name := «∂BracketedFun») "∂[" partialHead "]"   term:arg    : term

-- ────────────────────────────────────────────────────────────
-- Helpers
-- ────────────────────────────────────────────────────────────

/-- `true` iff `t` should be treated as a `Fin n` index.
    Numeric literals (e.g. `0`, `1`) default-elaborate as `Nat` but are
    unambiguously intended as direction indices, so we short-circuit on them.
    For other expressions we check whether the inferred type is `Fin n`. -/
private def isFin (t : Syntax) : TermElabM Bool :=
  -- Numeric literal → always an index
  if t.isNatLit?.isSome then return true
  else
    withoutModifyingState do
      try
        let e  ← elabTerm t none
        let ty ← whnf (← inferType e)
        return ty.isAppOf ``Fin && ty.getAppNumArgs == 1
      catch _ => return false

/-- Parse the head bracket into `(field, optional index)` as term syntax. -/
private def parseHead (head : Syntax) : TermElabM (TSyntax `term × Option (TSyntax `term)) := do
  match head with
  | `(partialHead| $k:term , $i:term) => return (k, some i)
  | `(partialHead| $t:term) =>
      if ← isFin t
      then return (← `(ℝ), some t)   -- index only  →  default field ℝ
      else return (t, none)            -- type only   →  field 𝕜, CLM result
  | _ => throwError "∂[]: unexpected head syntax"

/-- Builds `EuclideanSpace.single i (1 : 𝕜)`. -/
private def mkDir (𝕜 i : TSyntax `term) : TermElabM (TSyntax `term) :=
  `(EuclideanSpace.single $i (1 : $𝕜))

/-- Assemble `∂[·] body` for the lambda / at-point / directional forms. -/
private def assemble
    (𝕜 : TSyntax `term) (idx : Option (TSyntax `term)) (body : Syntax) : TermElabM (TSyntax `term) := do
  let dir? ← idx.mapM (mkDir 𝕜)
  match body with

  -- x', e  →  fun x' => fderiv 𝕜 (fun x' => e) x' [dir]
  | `(partialBody| $x:ident , $e) =>
    match dir? with
    | none   => `(fun $x => fderiv $𝕜 (fun $x => $e) $x)
    | some d => `(fun $x => fderiv $𝕜 (fun $x => $e) $x $d)

  -- (x := v), e  →  fderiv 𝕜 (fun x => e) v [dir]
  | `(partialBody| ($x:ident := $v) , $e) =>
    match dir? with
    | none   => `(fderiv $𝕜 (fun $x => $e) $v)
    | some d => `(fderiv $𝕜 (fun $x => $e) $v $d)

  -- (x := v; dv), e  →  fderiv 𝕜 (fun x => e) v dv  [no index allowed]
  | `(partialBody| ($x:ident := $v ; $dv) , $e) =>
    if idx.isSome then
      throwError "∂: cannot combine a basis index [i] with an explicit direction (x := v; dv)"
    `(fderiv $𝕜 (fun $x => $e) $v $dv)

  | _ => throwError "∂: unrecognized body syntax"

/-- Assemble `∂[·] f` for the curried function form. -/
private def assembleFun
    (𝕜 : TSyntax `term) (idx : Option (TSyntax `term)) (f : TSyntax `term) : TermElabM (TSyntax `term) := do
  match idx with
  | none   => `(fderiv $𝕜 $f)
  | some i =>
    let d ← mkDir 𝕜 i
    withFreshMacroScope `(fun x => fderiv $𝕜 $f x $d)

-- ────────────────────────────────────────────────────────────
-- Elaborators
-- ────────────────────────────────────────────────────────────

@[term_elab «∂Plain»]
def elabPartialPlain : TermElab := fun stx exp? => do
  let `(∂ $body:partialBody) := stx | throwError "∂: unexpected syntax"
  elabTerm (← assemble (← `(ℝ)) none body) exp?

@[term_elab «∂Bracketed»]
def elabPartialBracketed : TermElab := fun stx exp? => do
  let `(∂[ $head:partialHead ] $body:partialBody) := stx | throwError "∂: unexpected syntax"
  let (𝕜, idx) ← parseHead head
  elabTerm (← assemble 𝕜 idx body) exp?

@[term_elab «∂PlainFun»]
def elabPartialPlainFun : TermElab := fun stx exp? => do
  let `(∂ $f:term) := stx | throwError "∂: unexpected syntax"
  elabTerm (← assembleFun (← `(ℝ)) none f) exp?

@[term_elab «∂BracketedFun»]
def elabPartialBracketedFun : TermElab := fun stx exp? => do
  let `(∂[ $head:partialHead ] $f:term) := stx | throwError "∂: unexpected syntax"
  let (𝕜, idx) ← parseHead head
  elabTerm (← assembleFun 𝕜 idx f) exp?


-- ────────────────────────────────────────────────────────────
-- Tests
-- ────────────────────────────────────────────────────────────

variable {m n k : ℕ}
  (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k))
  (g : EuclideanSpace ℂ (Fin n) → EuclideanSpace ℂ (Fin m) → EuclideanSpace ℂ (Fin k))
  (x : EuclideanSpace ℝ (Fin n)) (y : EuclideanSpace ℝ (Fin m))
  (x' : EuclideanSpace ℂ (Fin n)) (y' : EuclideanSpace ℂ (Fin m))
  (dx : EuclideanSpace ℝ (Fin n))
  (i : Fin n) (j : Fin m)

-- Index in brackets → EuclideanSpace.single i 1 direction, field ℝ
#check ∂[i] (f · y) x                      -- (∂[i] (f · y)) x = fderiv ℝ (f · y) x (single i 1)
#check ∂[i] x'', (f x'' y)                 -- fun x'' => fderiv ℝ ... x'' (single i 1)
#check ∂[i] (x'' := x), (f x'' y)          -- fderiv ℝ ... x (single i 1)

-- Numeric literal as index (isFin short-circuits on nat literals)
variable [NeZero n]
#check ∂[0] (f · y) x                       -- fderiv ℝ (f · y) x (single (0 : Fin n) 1)

-- Field + index
#check ∂[ℂ, i] (g · y') x'                 -- fderiv ℂ (g · y') x' (single i 1)

-- Field only → curried CLM-map; normal application gives the CLM at a point
#check ∂[ℝ] (f · y)                         -- fderiv ℝ (f · y)  :  _ → _ →L[ℝ] _
#check ∂[ℝ] (f · y) x                       -- (∂[ℝ] (f · y)) x  :  _ →L[ℝ] _
#check ∂[ℝ] x'', (f x'' y)                 -- fun x'' => fderiv ℝ (fun x'' => f x'' y) x''
#check ∂[ℝ] (x'' := x), (f x'' y)          -- fderiv ℝ (fun x'' => f x'' y) x
#check ∂[ℝ] (x'' := x; dx), (f x'' y)      -- fderiv ℝ (fun x'' => f x'' y) x dx

-- No brackets → defaults to ℝ
#check ∂ (f · y)                             -- fderiv ℝ (f · y)
#check ∂ (f · y) x                           -- (∂ (f · y)) x

-- second derivative
#check ∂ ∂ (f · y)
#check ∂ (x':=x), ∂ (x'':=x'), (f x'' y)

[Paul Lezeau]

Tomas Skrivan said:

Btw there is inactive PR for partial derivatives notation #25427 it might be worth resurrecting and mention it in the guide.

I got distracted by other stuff, but I'd be very happy to resurrect this if there is appetite for it!