Computing derivatives of elementary functions

Stream: new members

[Stefan Kebekus]

Dear all,

I am new to lean and mathlib. As a first sample project in lean4, I would like to formalize the proof of Jensen's formula [https://en.wikipedia.org/wiki/Jensen%27s_formula] of complex analysis. Right now, I am banging my head against the wall because I cannot make lean to compute derivatives of the most elementary functions. Can anyone here please help me with that? I attach a reduced sample file that highlights with 'sorry' the places where I have problems.

Sorry for asking so elementary questions here. Any help of any kind is greatly appreciated!

Best wishes,

Stefan.

---

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.LineDeriv.Basic

-- Harmonic functions on the plane


noncomputable

def laplace : (ℂ → ℝ) → (ℂ → ℝ) := by

  intro f
  let F : ℝ × ℝ → ℝ := fun x ↦ f (x.1 + x.2 * Complex.I)

  let e₁ : ℝ × ℝ := ⟨1, 0⟩
  let e₂ : ℝ × ℝ := ⟨0, 1⟩

  let F₁ := fun x ↦ lineDeriv ℝ F x e₁
  let F₁₁ := fun x ↦ lineDeriv ℝ F₁ x e₁
  let F₂ := fun x ↦ lineDeriv ℝ F x e₂
  let F₂₂ := fun x ↦ lineDeriv ℝ F₂ x e₂

  exact fun x ↦ F₁₁ ⟨x.1, x.2⟩ + F₂₂ ⟨x.1, x.2⟩


example : ∀ z₀ : ℂ, laplace (fun z ↦ (z*z).re) z₀ = 0 := by
  intro z₀

  unfold laplace
  dsimp [lineDeriv]
  simp

  sorry

example : ∀ z₀ : ℂ, laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by
  intro z₀

  unfold laplace
  dsimp [lineDeriv]
  simp

  sorry

example : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
  -- Does not work: simp [deriv.add]
  sorry

[Ruben Van de Velde]

I don't know anything about lineDeriv, but I can help with your last example

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.LineDeriv.Basic

example : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
  rw [deriv_eq] -- in my experience with the library, more results are stated about `HasDerivAt` than about equality of `deriv`
  intro x
  apply HasDerivAt.const_add -- I guessed the name `HasDerivAt.add`, which didn't work, but the autocomplete dropdown showed `add_const` and `const_add` too
  exact hasDerivAt_id' x -- I assumed this was in the library, and `apply?` found it

[Stefan Kebekus]

@Ruben Van de Velde Now this is extremely helpful, thank you so much. I have been banging my head against concrete all day long. I will try to apply this to the other sorries (which are statements about deriv and not lineDeriv, so things might work).

[Luigi Massacci]

Here is your first one:

example : ∀ z₀ : ℂ, laplace (fun z ↦ (z*z).re) z₀ = 0 := by
  intro z₀
  unfold laplace
  dsimp [lineDeriv]
  simp
  conv =>
    lhs
    lhs
    arg 1
    intro t
    rw [deriv_sub] <;> tactic => try fun_prop
    rw [deriv_mul] <;> tactic => try fun_prop
    rw [deriv_const_add]
    simp
    ring_nf
  conv =>
    lhs
    rhs
    arg 1
    intro t
    rw [deriv_sub] <;> tactic => try fun_prop
    rw [deriv_const]
    rw [deriv_mul] <;> tactic => try fun_prop
    rw [deriv_const_add]
    simp
    ring_nf
  rw [deriv_const_add, deriv_sub] <;> try fun_prop
  simp

[Luigi Massacci]

Modulo that this was my first time actually computing derivatives, and there's probably a more optimized proof

[Luigi Massacci]

My strategy was "that looks like something I can do with conv + guessing the names of some rw theorems + fun_prop is always awesome"

[Stefan Kebekus]

@Luigi Massacci Thank you so much! I have a bit of a hard time following, though. What does 'conv' do in this context?

[Luigi Massacci]

try it out in the infoview and it should be clearer, but essentially it allows you to work under binders (in particular, to simplify expressions), see here for some documentation, it is one of the more useful tactics for this kind of stuff.

[Stefan Kebekus]

@Luigi Massacci Understood. Awesome, you saved my [and my wife's] weekend. Thanks again!

[Luigi Massacci]

Also, if you are doing Complex Analysis stuff, @Vincent Beffara can probably be helpful for the non-elementary stuff

[Patrick Massot]

@Stefan Kebekus we should start by saying that Mathlib is very bad at concrete computations. We know we have a lot of work to do about that. Some of it is already under way. For instance https://github.com/leanprover-community/mathlib4/pull/10594 is work in progress towards a tactic that helps computing concrete derivatives. Right know you would have a lot more fun formalizing abstract mathematics.

[Patrick Massot]

For instance your last example can be proven using:

example : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
  ext t
  rw [deriv_const_add]
  simp

but really it should be only one tactic.

[Patrick Massot]

However I also think you took a wrong start with your definition of the Laplacian. You used lineDeriv that is a very exotic definition, as explained in the overall documentation of the file containing it: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/LineDeriv/Basic.html.

[Patrick Massot]

So I am not surprised that lots of lemmas are missing here.

[Patrick Massot]

A more idiomatic definition would be using docs#iteratedFDeriv.

[Patrick Massot]

Something like

def laplace' (f : ℂ → ℝ) (z : ℂ) : ℝ :=
  iteratedFDeriv ℝ 2 f z ![1, 1] + iteratedFDeriv ℝ 2 f z ![Complex.I, Complex.I]

[Patrick Massot]

Which reads

$$\Delta f(z) = D^2f(z)(1, 1) + D^2f(z)(i, i)$$

where you can already see that Lean requires you to be more specific that you paper and pen since the above expression does not clearly say whether $D$ means real or complex differentiation.

[Patrick Massot]

However using this definition will not fix the issue I started with: doing concrete computations will probably be very painful.

[Patrick Massot]

Note for people who wonder what they could do to help the community today: in the Lean 3 version of the Mathematics in Lean textbook, the differential calculus chapter contained more concrete examples than in the Lean 4 version. Those examples were removed when we ported the book last summer because the Lean 4 simplifier had bugs at that time. In the mean time Leo worked a lot on the Lean 4 simplifier and I bet many of those examples could be restored (maybe after adding some simp attributes in mathlib). A pull request to the book doing that would be very welcome.

[Stefan Kebekus]

@Patrick Massot Thank you for your explanations and suggestions. I am experimenting with the approach you suggested and do seem to make some progress. I am looking forward to working with the community here. Thanks again.

[Stefan Kebekus]

@Luigi Massacci Thanks again for your help. I will be in touch with Beffara as soon as my project becomes more concrete.

[Stefan Kebekus]

@massot Dear Patrick, I am trying to follow the path that you suggested … but now I am struggling to compare various notions of derivatives. Any help would be greatly appreciated! -- Thanks again, and sorry for the hassle.

Concretely, for a function

$$f : \mathbb R \times \mathbb R \to R$$

I would like to compare

$$f''(z) (a, b), (\frac{\partial}{\partial a}\frac{\partial}{\partial b}f)(z), ( w \to f'(w)(a))'(b)$$

In Lean4:

lemma l₁ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
  ∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = iteratedFDeriv ℝ 2 f z ![a, b] := by
  sorry

lemma l₂ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
  ∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w ↦ (fderiv ℝ f w) a) z) b := by
  sorry

[Sébastien Gouëzel]

These questions are not straightforward, especially the first one, since the definition of the iterated derivative involves the process called currying (viewing a function on a product space as a function of functions), and one needs to see how this process commutes with taking derivatives -- while this is all completely transparent in informal mathematics. Here are proofs for your statements:

import Mathlib.Analysis.Calculus.ContDiff.Bounds
import Mathlib.Analysis.Calculus.FDeriv.Symmetric

variable {E : Type*} [NormedAddCommGroup E]  [NormedSpace ℝ E]

lemma l₁ (f : E → ℝ) (z a b : E) :
    fderiv ℝ (fderiv ℝ f) z a b = iteratedFDeriv ℝ 2 f z ![a, b] := by
  -- next line should not be needed, but is because of synthPending issue
  let A (n : ℕ) : NormedAddCommGroup (E →L[ℝ]
      ContinuousMultilinearMap ℝ (fun (_ : Fin n) ↦ E) ℝ) := by infer_instance
  simp only [iteratedFDeriv_succ_eq_comp_left, Nat.succ_eq_add_one, Nat.reduceAdd,
    Function.comp_apply,
    (continuousMultilinearCurryLeftEquiv ℝ (fun (_ : Fin 1) ↦ E) ℝ).comp_fderiv
      -- next line shouldn't be needed, but Lean is confused without it
      -- without any help (i.e., just using LinearIsometryEquiv.comp_fderiv), nothing is simplified.
      (f := fderiv ℝ (iteratedFDeriv ℝ 0 f)),
    continuousMultilinearCurryLeftEquiv_apply, Fin.isValue, Matrix.cons_val_zero, Fin.tail_def,
    ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe]
  simp [iteratedFDeriv_zero_eq_comp, fderiv_continuousLinearEquiv_comp,
    LinearIsometryEquiv.comp_fderiv']

lemma l₂' {f : E → ℝ} (hf : ContDiff ℝ 2 f) (z a b : E) :
    fderiv ℝ (fderiv ℝ f) z b a = fderiv ℝ (fun w ↦ fderiv ℝ f w a) z b := by
  rw [fderiv_clm_apply]
  · simp
  · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
  · simp

lemma l₂ {f : E → ℝ} (hf : ContDiff ℝ 2 f) (z a b : E) :
    fderiv ℝ (fderiv ℝ f) z a b = fderiv ℝ (fun w ↦ fderiv ℝ f w a) z b := by
  rw [← l₂' hf z a b]
  apply second_derivative_symmetric (f := f) (f' := fderiv ℝ f) (x := z)
  · intro y
    exact (hf.differentiable one_le_two y).hasFDerivAt
  · exact ((contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z).hasFDerivAt

Note that the first proof will not compile on master, as I had to add a few missing statements in our library here and there. But it works on my branch SG_fderiv_fderiv, as you can see at https://github.com/leanprover-community/mathlib4/actions/runs/8949607940/job/24584095263.

[Sébastien Gouëzel]

A few comments on the proofs.

First, instead of taking a function defined on ℝ × ℝ as in your example, I did it on a general normed space. The reason is that more generality often makes the proofs easier to read and to write, as you are not confused by irrelevant details.

Second, for the first lemma l₁, I didn't need the assumption of second differentiability, this identity is always true.

Third, for the second lemma l₂, your statement is true as given, but not so natural because you have exchanged the roles of a and b in the left and right hand sides. Of course, it doesn't make a difference since the second derivative is symmetric (and we know that in mathlib), but the natural proof gives the statement l₂' in my code snippet.

Don't hesitate to ask if you have more questions on what is going on there!

[Sébastien Gouëzel]

Also, as spaces of continuous linear maps into spaces of continuous multilinear maps are quite involved, Lean struggles a little bit here and you can see a few defects of our system in the proof of l₁, that I have pinpointed in the comments. Namely, typeclass inference is failing if I don't help it a little bit, and a simp lemma doesn't fire if I don't help it a little bit.

[Stefan Kebekus]

@Sébastien Gouëzel Thank you for your great answer. This will definitely help me move forward.

I understand your comments on the proofs/my statements. This is a little simplistic because I tried to write down the simplest statement I couldn't prove. As soon as things are working, I will upgrade the statements to the appropriate level of generality.

Are you planning to submit SG_fderiv_fderiv to the main branch of mathlib anytime soon?

Thanks again,

Stefan.

[Sébastien Gouëzel]

Yes, I have just PRed my branch to mathlib, in #12697 (with a simpler proof than the above, as I found a better lemma).

[Stefan Kebekus]

That's very good news, looking forward to it.