Computing derivatives

Stream: Is there code for X?

[Michail Karatarakis]

Here's an mwe. Is there API for computing derivatives like this? I also have this unfilter lemma below to rewrite with but didn't get far :

import Mathlib.Analysis.Analytic.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.Complex.Basic

lemma unfilter {A f} (p : A → Prop) :
  (∀ᶠ z in f, p z) ↔ ∃ U ∈ f, ∀ z ∈ U, p z := by
    constructor
    · intro h; use {x | p x}; exact ⟨h, by aesop⟩
    · intro h
      rcases h with ⟨U, ⟨hU, hUp⟩⟩
      exact Filter.mem_of_superset hU hUp

theorem extracted_1 (z₀ : ℂ) (f : ℂ → ℂ) (hf : AnalyticAt ℂ f z₀)
  (hfdev : AnalyticAt ℂ (deriv f) z₀) (n : ℕ) (hn : n > 0)
  (g : ℂ → ℂ) (hg : AnalyticAt ℂ g z₀) (hgneq0 : g z₀ ≠ 0)
  (hexp : ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z) :
  ∀ᶠ (z : ℂ) in nhds z₀, deriv f z = (z - z₀) ^ (n - 1) • (n • g z + (z - z₀) • deriv g z) := sorry

[Michael Rothgang]

The fun_trans tactic (in some mathlib PR; I'm not sure what this is waiting on - besides reviews, of course) by @Tomas Skrivan goes in that direction. It seems like you want that, but also additional lemmas about analytic functions. (I can imagine you'd need to rewrite by those first, but then the tactic could work.)

[Tomas Skrivan]

fun_trans is a tactic designed to compute derivatives that can do something like the theorem statement but I didn't test it(and likely does not work) with filters like that.

My plan for the summer is to port tactic data_synth to mathlib that computes derivatives using HasFDeriv R f f' rather than with equality theorems fderiv R f = f' as fun_trans does. data_synth should effectively subsume fun_trans.

[Tomas Skrivan]

However, I'm really not sure how the tactic would help with this question as it is not completely clear to me what is meant by "API like this"

fun_trans can work with statements like this

  deriv ((z - z₀) ^ n • g z) z = (z - z₀) ^ (n - 1) • (n • g z + (z - z₀) • deriv g z)

and data_synth can work with HasDeriv equivalent which is not exactly how the theorem is stated.

[Michael Rothgang]

Today I needed to compute some elementary derivatives in Lean. This was for some analysis proof in the Carleson project (estimating "this constant is less than that constant", which involved proving the monotonicity of some function, which involves differentiating).

This involved polynomials and exponentials - so is straight-forward "in principle", but surprisingly tedious in Lean. A data_synth tactic would have been really helpful here: let me add one more voice of "this work is really useful" --- also for formalising research level proofs (as opposed to e.g. exercise sheets).

[Tomas Skrivan]

I started porting it to mathlib but got stuck when I realised that there is lots of complexity coming from computing derivatives of programs efficiently i.e. handling lots of let bindings efficiently. I'm not really sure if all of that is worth porting as it will take lots of time to clean up and document properly and at the same time all this complexity will be of little use to mathlib users.

I need to figure out how to have a simplified(but cleaner and maintainable) version of data_synth for mathlib and the efficient but messy version for SciLean without too much code duplication.

[Tomas Skrivan]

@Michael Rothgang What was the exact derivative you had to compute? It is always useful to have a set of actual use cases. For fun_prop it was really useful to have concrete problems from the sphere eversion project

[Michael Rothgang]

Thanks for asking! Basically, a large part of the diff in https://github.com/fpvandoorn/carleson/pull/357/files would ideally be just calls to data_synth.

[Michael Rothgang]

More precisely, here is a somewhat minimal example of what I needed to prove:

import Mathlib

open Real Set

noncomputable section

theorem deriv_const_rpow {a f' x : ℝ} {f : ℝ → ℝ} (hf : HasDerivAt f f' x) (ha : 0 < a) :
    deriv (a ^ f ·) x = (Real.log a) * f' * (a ^ f x) := by
  apply HasDerivAt.deriv
  convert HasDerivAt.rpow (hasDerivAt_const x a) hf ha using 1
  ring

def f : ℝ → ℝ := fun x ↦ 2 ^ (12 * x) / (3 * x ^ 3)

def f₁ : ℝ → ℝ := fun x ↦ (2 : ℝ) ^ ((12 : ℝ) * x)

def f₂ : ℝ → ℝ := fun x ↦ 3 * x ^ 3

lemma differentiableOn_f₁ : Differentiable ℝ f₁ := by
  unfold f₁
  apply Differentiable.comp ?_ (by fun_prop)
  exact Differentiable.rpow (by fun_prop) (by fun_prop) (fun _ ↦ by norm_num)

lemma differentiableOn_f₂ : Differentiable ℝ f₂ := by
  unfold f₂
  fun_prop

lemma differentiableOn_f : DifferentiableOn ℝ f (Set.Ioi 0) := by
  intro x hx
  have : 0 < x := hx
  unfold f
  apply DifferentiableAt.differentiableWithinAt
  apply (differentiableOn_f₁ x).mul <| (differentiableOn_f₂ x).inv (by sorry)

-- Is the derivative of f.
def f' : ℝ → ℝ := fun x ↦ ((12 * Real.log 2) - 3 * x⁻¹) * f x

lemma hf'₁ (x : ℝ) : deriv f₁ x = (12 * Real.log 2) * f₁ x := by
  let f₃ : ℝ → ℝ := fun x ↦ 12 * x
  have hf₃ : HasDerivAt f₃ 12 x := by
    convert (hasDerivAt_id' x).const_mul (c := 12)
    rw [mul_one]
  let f₄ : ℝ → ℝ := fun x ↦ 2 ^ x
  have : f₁ = f₄ ∘ f₃ := by ext; simp [f₁, f₃, f₄]
  -- Proof in Carleson works somewhat like this.
  sorry /- rw [deriv_const_rpow (a := 2) hf₃ (by norm_num), this]
  ring_nf
  congr -/

lemma hf'₂ {x} (hx : x ≠ 0) : deriv f₂ x = 3 * x⁻¹ * f₂ x := by
  symm
  calc 3 * x⁻¹ * f₂ x
    _ = 9 * x ^ 2 := by
      unfold f₂
      calc 3 * x⁻¹ * (3 * x ^ 3)
        _ = 9 * x ^ 2 * x * x⁻¹ := by ring
        _ = 9 * x ^ 2 := by rw [mul_assoc, CommGroupWithZero.mul_inv_cancel x hx, mul_one]
    _ = 3 * (3 * x ^ 2) := by ring
    _ = _ := by
      unfold f₂; rw [HasDerivAt.deriv]
      exact (hasDerivAt_pow 3 x).const_mul 3

lemma deriv_f_eq {x : ℝ} (hx : 0 < x) : deriv f x = f' x := by
  calc deriv f x
    _ = deriv (fun x ↦ f₁ x / f₂ x) x := rfl
    _ = (deriv f₁ x * f₂ x - f₁ x * deriv f₂ x) / (f₂ x) ^ 2 := by
      apply deriv_div (differentiableOn_f₁ x) (differentiableOn_f₂ x)
      unfold f₂
      positivity
    _ = ((deriv f₁ x - f₁ x * 3 * x⁻¹) * f₂ x) / (f₂ x) ^ 2 := by rw [hf'₂ hx.ne']; ring
    _ = (deriv f₁ x - f₁ x * 3 * x⁻¹) / (f₂ x) := by
      have (a d : ℝ) (hd : d ≠ 0) : a * d / d ^ 2 = a / d := by
        rw [← IsUnit.mul_div_mul_right hd.isUnit a d]
        ring
      rw [this]
      unfold f₂
      positivity
    _ = _ := by simp only [f, f₁, f₂, f', hf'₁]; ring

example : MonotoneOn f (Set.Ici 4) := by
  apply monotoneOn_of_deriv_nonneg (convex_Ici 4)
    (differentiableOn_f.continuousOn.mono <| Ici_subset_Ioi.mpr (by norm_num)) ?_
  · intro x hx
    rw [interior_Ici, mem_Ioi] at hx
    rw [deriv_f_eq (by positivity)]
    unfold f'
    apply mul_nonneg
    · simp only [sub_nonneg]
      trans 3 * 4⁻¹
      · gcongr
      · linarith [Real.log_two_gt_d9]
    · unfold f
      positivity
  · rw [interior_Ici]
    exact differentiableOn_f.mono <| Ioi_subset_Ioi (by norm_num)

[Michael Rothgang]

Both the "my function is differentiable" and "its deriv is ..." would be nice to automate.

[Michael Rothgang]

I'm not quite sure why fun_prop cannot just do the first aspect, but the derivative is actually the more important one for me. (I could possibly golf this by taking the derivative, showing it's non-zero and deducing that my function must be differentiable. I haven't tried yet.)

[Eric Wieser]

As always, I'd suggest using HasDerivAt as much as possible, and avoiding Differentiable/deriv until the very last moment

[Rémy Degenne]

Tomas Skrivan said:

What was the exact derivative you had to compute? It is always useful to have a set of actual use cases.

The proofs of integral_id_gaussianReal and variance_fun_id_gaussian are basically derivative computations that are still much too long in Mathlib: https://github.com/leanprover-community/mathlib4/blob/fc190a53670152feca8698a35180a7d4bc08de07/Mathlib/Probability/Distributions/Gaussian/Real.lean#L500-L523

[Tomas Skrivan]

Eric Wieser said:

As always, I'd suggest using HasDerivAt as much as possible, and avoiding Differentiable/deriv until the very last moment

Yes yes that is what data_synth designed to do and I have simprocs that then simplify deriv ...

[Eric Wieser]

I tried to do this by hand, but got stuck in some algebra:

theorem hasDeriv_f {x : ℝ} (hx : 0 < x) : HasDerivAt f (f' x) x := by
  have : HasDerivAt f _ x
  · refine .div (𝕜' := ℝ) (x := x) (c' := ?_) (d' := ?_) ?h1 ?h2 (by positivity)
    case h1 =>
      refine .rpow (x := x) (g' := ?_) (f' := ?_) ?h11 ?h12 ?_
      case h11 =>
        exact hasDerivAt_const x (_ : ℝ)
      case h12 =>
        refine .mul (𝔸 := ℝ) (x := x) (c' := ?_) (d' := ?_) ?h121 ?h122
        case h121 =>
          exact hasDerivAt_const x (_ : ℝ)
        case h122 =>
          exact hasDerivAt_id x
      · positivity
    case h2 =>
      refine .mul (𝔸 := ℝ) (x := x) (c' := ?_) (d' := ?_) ?h21 ?h22
      case h21 =>
        exact hasDerivAt_const x (_ : ℝ)
      case h22 =>
        refine .pow (x := x)  (c' := ?_) _ ?h221
        case h221 =>
          exact hasDerivAt_id x
  convert this; clear this
  ext
  simp [f', f]
  ring_nf
  sorry

[Eric Wieser]

It seems like the elaborator fights you here much more than it used to