2.1. Symbolic Differentiation

2.1.1. Notation

Writing fderiv ℝ (fun x => f x) is somewhat tedious so SciLean makes our life easier by introducing a nice notation ∂ x, f x for differentiating (f x) w.r.t. x.

Before we explore this notation further we have to mention that fderiv can also compute complex derivatives with @fderiv ℂ instead of @fderiv ℝ. However, most of the time we work exclusively with real derivative so we can inform Lean that the default choce of the scalar field are real numbers using the following command

Now Lean knows that we want real derivative when we write ∂ x, f x.

Using this notation we can compute again the above derivative

fun x => ↑n * x ^ (n - 1) : ℝ → ℝ

Because we did not specify the point where we want to compute the derivative we obtained a function in x. We can specify the point where we want to compute the derivative with ∂ (x:=x₀), ...

↑n * x₀ ^ (n - 1) : ℝ

Writing rewrite_by fun_trans every time we want to diferentiate an expression gets a bit tedious. We can add an exclamation mark after ∂ to indicate that we want to run fun_trans tactic to compute the derivative.

fun x => ↑n * x ^ (n - 1) : ℝ → ℝ

We can differentiate w.r.t to a vector valued variable (x : ℝ×ℝ)

fun x => fun dx =>L[ℝ] 2 * ⟪dx, x⟫ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ

For derivatives w.r.t. a vector valued variable we have to also specify the direction in which we differentiate. Therefore in the above we obtained derivative as a function of the position x and direction dx. Furthermore, the notation fun dx =>L[ℝ] ... indicates that the function is linear function in dx and similarly X →L[ℝ] Y stands for the space of ℝ-linear functions from X to Y.

If we want to specify the position and the direction in which we want to compute the derivatives we use the notation ∂ (x:=x₀;dx₀), f x

2 * ⟪du₀, u₀⟫ : ℝ

To summarize all the different variants. For function of a scalar valued argument

For function of a vector valued argument

There is nothing stopping us from applying derivative multiple times to compute higher order derivatives

fun x => 2 : ℝ → ℝ

2.1.2. Examples

Let's put computing derivatives to some practical use. We will demonstrate how to use SciLean symbolic differentiations to solve few common tasks in scientific computing and physics.

1.414214

  ring_nf --  m * (sqrt (k / m) * (sqrt (k / m) ==> m * sqrt (k * m⁻¹) ^ 2
  have h : m * sqrt (k * m⁻¹) ^ 2 = k := sorry_proof
  simp[h]

2.1.3. Gradient

In many practical applications, we need to compute gradient instead of directional derivative. For a function \(f : \mathbb{R}^n \rightarrow \mathbb{R} \) the gradient of \(f\) is a vector of all its partial derivatives

$$\nabla f = \left(\frac{\partial f}{\partial x_1}, \dots, \frac{\partial f}{\partial x_n} \right) $$

A more general way of defining gradient is through linear map transposition/adjoint. The derivative of a function f at point x is a linear map from X to ℝ

∂ f x : X →L[ℝ] ℝ

To obtain gradient we take an adjoint and evaluate it at one. This is exactly how gradient is defined.

Few examples of computing gradients

(1, 0) : ℝ × ℝ

2 • x₀ : X

y : X

variable {X} [NormedAddCommGroup X] [AdjointSpace ℝ X] [CompleteSpace X]

2.1.4. Derivative Rules

A commong issue when fun_trans is not doing what we expect is that there is a missing differentiation theorem.

For example, if we define a function

then nothing happens when we try to differentiate it

fun x => (∂ (x:=x), foo x) 1 : ℝ → ℝ

Turning on the fun_trans trace reveals useful information

[Meta.Tactic.fun_trans] [❌] ∂ (x:=x), foo x
  [Meta.Tactic.fun_trans] candidate theorems for foo: []
  [Meta.Tactic.fun_trans] candidate local theorems for foo: []
  [Meta.Tactic.fun_trans] candidate fvar theorems: [isContinuousLinearMap_fderiv]
  [Meta.Tactic.fun_trans] [❌] applying: isContinuousLinearMap_fderiv
    [Meta.Tactic.fun_trans] isContinuousLinearMap_fderiv, failed to discharge hypotheses
          SciLean.IsContinuousLinearMap ℝ fun x => foo x

The ❌ on the first line signifies that fun_trans failed to make prograss on ∂ (x:=x), foo x. The next two lines

  [Meta.Tactic.fun_trans] candidate theorems for foo: []
  [Meta.Tactic.fun_trans] candidate local theorems for foo: []

states that there are no derivative theorems for foo. The next line

  [Meta.Tactic.fun_trans] candidate fvar theorems: [isContinuousLinearMap_fderiv]

states that there is a potentially applicable theorem isContinuousLinearMap_fderiv which can differentiate linear functions. However the next few lines report that applying this theorem failed as fun_trans can't prove that foo is (continuous) linear map.

To remedy this problem we can define derivative of foo

and add a theorem that the derivative of foo is equal to foo_deriv

Because foo_deriv_rule is marked with fun_trans attribute it will be used when we try to differentiate foo now

fun x => foo_deriv x : ℝ → ℝ

Unfortuantelly there is one more issue, fun_trans will do nothing when we try to compose foo together

fun x => (∂ (x:=x), foo (foo x)) 1 : ℝ → ℝ

...
  [Meta.Tactic.fun_trans] trying comp theorem SciLean.fderiv.comp_rule
  [Meta.Tactic.fun_trans] [❌] applying: SciLean.fderiv.comp_rule
    [Meta.Tactic.fun_trans] SciLean.fderiv.comp_rule, failed to discharge hypotheses
          Differentiable ℝ fun x0 => foo x0
...

The trace reveals that fun_trans tries to apply composition(chain) rule SciLean.fderiv.comp_rule but it fails as it can't prove Differentiable ℝ fun x0 => foo x0. We need another theorem stating that foo is differentiable function. Mathlib has a tactic fun_prop that can prove differentiability and many other function properties like linearity, continuity, measurability etc. and fun_trans uses this tactic to ensure it can apply chain rule.

We need to add fun_prop theorem for foo

Now fun_trans knows that foo is differentiable function and can safely apply chain rule

fun x => foo_deriv x * foo_deriv (foo x) : ℝ → ℝ

Writing these theorems by hand is quite tedious so there is a macro def_fun_prop and def_fun_trans to help you with writing these theorems

It generates these theorems and definition

The problem of writing appropriate theorems for fun_trans and fun_prop is quite involved problem and will be discussed in future chapter.

2.1.5. Differentiating Division, Log, Sqrt, ...

So far we have worked with functions that are smooth. However, functions like division, log, sqrt, ‖·‖₂ are not differentiable everywhere. We have to be a bit careful with those functions because SciLean tries to perform computations that are, at least in principle, fully formalizable. Let's try to differentiate division

fun x => (∂ (x:=x), x⁻¹) 1 : ℝ → ℝ

We did not get expected -x⁻². When differentiation, or any tactic, is not doing what we expect we can turn on tracing. Let's try again with tracing on

and the beggining of the trace is saying that fun_trans tried to apply theorem HDiv.hDiv.arg_a0a1.fderiv_rule_at however it failed to discharge x ≠ 0

[Meta.Tactic.fun_trans] [❌] ∂ (x:=x), 1 / x
  [Meta.Tactic.fun_trans] candidate theorems for HDiv.hDiv: [HDiv.hDiv.arg_a0a1.fderiv_rule_at]
  [Meta.Tactic.fun_trans] [❌] applying: HDiv.hDiv.arg_a0a1.fderiv_rule_at
    [Meta.Tactic.fun_trans] [❌] discharging: x ≠ 0
    [Meta.Tactic.fun_trans] HDiv.hDiv.arg_a0a1.fderiv_rule_at, failed to discharge hypotheses
          x ≠ 0

This makes sense as division 1/x is well defined and differentiable only away from zero. Therefore we have to differentiate it at a concrete point that is not equal to zero.

-1 / x₀ ^ 2 : ℝ

We introduced a point x₀ and assumption hx₀ that it is not equal to zero. By default fun_trans does not see this assumption and we have to provide discharger. A discharger is any tactic that tries to satisfy(discharge) any assumption of the theorems fun_trans is using. In this simple case assumption tactic is enough as it just looks through the local context and tries to directly apply any existing assumptions.

Using assumption is not enough for a more complicated expression

(∂ (x:=x₀), (x ^ 2)⁻¹) 1 : ℝ

tracing shows

[Meta.Tactic.fun_trans] HDiv.hDiv.arg_a0a1.fderiv_rule_at,
  failed to discharge hypotheses x₀ ^ 2 ≠ 0

We need a tactic that is capable of infering (x₀^2 ≠ 0) from (x₀ ≠ 0). A very general and powerful tactic is aesop

-(2 * x₀) / (x₀ ^ 2) ^ 2 : ℝ

In multiple dimensions we often want to differentiate the norm

The fact that norm is not differentiable can cause issues. The common practice when writing numerical algorithms is to regularize norm using a small positive ε.

fun w => fun x =>L[ℝ] 2 * ⟪x, w⟫ / (2 * sqrt (ε + ‖w‖₂²)) : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ

2.1.6. Abstract Vector Spaces

In calculus we usually consider only functions \((f : \mathbb{R}^n \rightarrow \mathbb{R}^m) \). The issue is that on computers the type \( \mathbb{R}^n \) can have multiple different realizations. For example \( \mathbb{R}^3 \) can be modeled by Float×Float×Float, Float^[3] or Float×Float^[2]. They are all equivalent but in code we have to explicitely convert between these types. For this reason it is better to work with abstract vector spaces instead of with \( \mathbb{R}^n \).

Fortunately mathlib's derivative fderiv is already defined for a function (f : X → Y) between two abstract vector spaces X and Y over a field 𝕜. Mathlib's way of introducing an abstract vector space is rather involved and we need to spend some time talking about it. This presentation will be rather simplified. For interested reader we provide references at the end of this section that go over mathlib's algebraic stracutes in more detail.

A vector space X is a set with operations +,-,•,0 such that

  ∀ (x y z : X), x + (y + z) = (x + y) + z
  ∀ (x y : X), x + y = y + x
  ∀ (x : X), x + 0 = 0
  ∀ (x : X), x + (-x) = 0

  ∀ (r s : 𝕜) (x : X), r • (s • x) = (r * s) • x(
  ∀ (x : X), 1 • x = x
  ∀ (r : 𝕜) (x y : X), r • (x + y) = r • x + r • y
  ∀ (r s : 𝕜) (x : X), (r + s) • x = r • x + s • x

in mathlib the axioms talking about addition and negation are captured by the type class AddCommGroup and the aximps talking about scalar multiplication are captured by the type class Module. Therefore if we want to introduce a new abstract vector space over a field R we have to introduce these variables

When we want to differentiate a function (f : X → Y) between two vector spaces we also need that X and Y are equiped with a norm. For this purpose there is NormedAddCommGroup which equips AddCommGroup with a norm and guarantees that it compatible with addition and negation, and NormedSpace which equips Module with a norm and guarentees that it is compatible with scalar multiplication. Furthermore, we have to restric to a filed 𝕜 that is either real numbers ℝ or complex numbers ℂ. The type class RCLike states exactly that. Therefore when we work with derivative in general setting the code usually looks like this

When working with gradients we also need inner product as adjoint is defined through inner product. Unfortunately, here we diverge from mathlib a little bit. Mathlib defines InnerProductSpace which equips NormedSpace with inner product. Understandably InnerProductSpace requires that the ⟪x,x⟫ = ‖x‖² however mathlib made the unfortunate decision by definin norm on produce spaces as ‖(x,y)‖ = max ‖x‖ ‖y‖ which is incompatible with the inner product structure. Therefore type like ℝ×ℝ can't be equiped with InnerProductSpace. Because of these issues, SciLean introduces AdjointSpace which is almost identical to InnerProductSpace but it only requires that the norm induced by inner product is equivalend to the existing norm i.e. ∃ (c d : ℝ⁺), ∀ x, c * ⟪x,x⟫ ≤ ‖x‖^2 ≤ d * ⟪x,x⟫. On AdjointSpace SciLean introduces L₂-norm ‖x‖₂ := sqrt ⟪x,x⟫ which you have seen already and it is the norm you most likely want to use instead of the default norm ‖x‖. Therfore when we work with gradient in general setting the code usually looks like this

For interested reader we recommend reading the chapter Hierachies from Mathematics in Lean which explains how mathlib approaches algebraic hierachies like monoids, groups or modules. After reading that we recommend reading Differential Calculus in Normed Spaces which how NormedSpace is structured.