Computing derivatives examples

Stream: PhysLean

[Tomas Skrivan]

I'm working on porting data_synth tactic to mathlib, it is a tactic that can be used for computing derivatives. In physics, one has to compute derivatives very often. I would like to use this thread to collect examples of derivatives that this tactic should be able to compute. Any examples are welcome! Collecting such example would help me a lot in developing the tactic.

[Tomas Skrivan]

Let's start with a very simple example:

example (v t : ℝ) : deriv (fun t : ℝ => 1/2 * v * t^2) t = v * t := sorry

[Joseph Tooby-Smith]

Arefderiv examples ok? if so this is one I calculated a couple of days ago related to the point particle in EM:

import Mathlib

open InnerProductSpace
example (n : ℕ) (x y : EuclideanSpace ℝ (Fin 3)) :
    fderiv ℝ (fun x => (‖x‖ ^ 2 + 1/(n + 1))^ (-1/2 : ℝ)) x y =
    - ((‖x‖ ^ 2 + (1 + (n : ℝ))⁻¹) ^ (- 1 /2 : ℝ)) ^ 3 * ⟪x, y⟫_ℝ  := by sorry

[Tomas Skrivan]

Yes fderiv is ok, gradient, adjFDeriv, varGradient are ok too.

[ZhiKai Pong]

an example from wave equation:

import Mathlib

lemma wave_dt {s : EuclideanSpace ℝ (Fin d)} {f₀' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)}
    (h' : ∀ x, HasFDerivAt f₀ (f₀' x) x) :
    fderiv ℝ (fun t => f₀ (inner ℝ x s - c * t)) 1 =
    fun t => -c • (f₀' (inner ℝ x s - c * t)) 1 := by sorry

[Tomas Skrivan]

Basic division examples:

example (x : ℝ) (hx : x ≠ 0) : deriv (fun x : ℝ => x⁻¹) x = - x^(-2:ℤ) := sorry
example (x : EuclideanSpace ℝ (Fin 3)) : gradient (fun x => 1/‖x‖) x = -‖x‖^(-3:ℤ)•x := sorry

[ZhiKai Pong]

actually dx might be more interesting since you have to deal with single:

import Mathlib

lemma wave_dx {u v : Fin d} {s : EuclideanSpace ℝ (Fin d)}
    {f₀' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)}
    (h' : ∀ x, HasFDerivAt f₀ (f₀' x) x) :
    (fun x' => fderiv ℝ (fun x => (inner ℝ (f₀ (inner ℝ x s - c * t))
    (EuclideanSpace.single u 1))) x' (EuclideanSpace.single v 1))
    =
    fun x' => (inner ℝ (f₀' (inner ℝ x' s - c * t) (s v))
    (EuclideanSpace.single u 1)) := by sorry

[Joseph Tooby-Smith]

Example of one from the velocity of the classical harmonic oscillator:

import Mathlib
open Real
example (t ω : ℝ) (x₀ v₀ : EuclideanSpace ℝ (Fin 1)) :
  (fderiv ℝ (fun t => cos (ω * t) • x₀ + (sin (ω * val) / ω) • v₀) t) 1 =
  -ω • sin (ω * t) • x₀ + cos (ω * t) • v₀:= by sorry

[ZhiKai Pong]

fwiw the second derivative if solvable by a single tactic will be nice:

import Mathlib

lemma wave_dx2 {u v : Fin d} {s : EuclideanSpace ℝ (Fin d)}
    {f₀' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)} {f₀'' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)}
    (h'' : ∀ x, HasFDerivAt (fun x' => f₀' x' 1) (f₀'' x) x) :
    (fderiv ℝ (fun x' => (inner ℝ ((f₀' (inner ℝ x' s - c * t)) (s u))
    (EuclideanSpace.single v 1))) x) (EuclideanSpace.single u 1)
    =
    inner ℝ ((s u) ^ 2 • f₀'' (inner ℝ x s - c * t) 1) (EuclideanSpace.single v 1) := by sorry

[Joseph Tooby-Smith]

For adjFDeriv and varGradient I don't think there are any others in PhysLean then the ones we wrote when proving the Euler-Lagrange equations

[Tomas Skrivan]

Yeah, I guess just having Euler-Lagrange equation in one shot would be nice

[Joseph Tooby-Smith]

Yeah - that and Hamilton's equations!

[Tomas Skrivan]

Ok I have all these tests working now. You can have a look here

[Tomas Skrivan]

I had to modify the statement of the wave_dx2 lemma to

lemma wave_dx2 {u v : Fin d} {s : EuclideanSpace ℝ (Fin d)}
    {f₀' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)}
    {f₀'' : ℝ → ℝ →L[ℝ] ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)}
    (h'' : ∀ x, HasFDerivAt (fun x' => f₀' x') (f₀'' x) x) :
    (fderiv ℝ (fun x' => (inner ℝ ((f₀' (inner ℝ x' s - c * t)) (s u))
    (EuclideanSpace.single v 1))) x) (EuclideanSpace.single u 1)
    =
    inner ℝ (f₀'' (⟪x, s⟫_ℝ - c * t) (s u) (s u)) (EuclideanSpace.single v 1) := by

  have h : ⟪EuclideanSpace.single u 1, s⟫_ℝ = s u := by sorry
  conv_lhs =>
    simp only [fderiv_simproc]
    check_no_fderiv
    simp [h]

Let me explain what is happening in the proof.

• conv_lhs focuses on the left hand side
• simp only [fderiv_simprocs] calls simp with new simproc that computes derivatives and internally calls data_synth tactic to compute HasFDerivAt R f _ x. Simp is called with only to prevent it from computing trivial derivatives and such that I can see the raw output of the simproc
• check_no_fderiv checks fderiv has been eliminated
• simp[h] just call simp to massage lhs to the form of rhs

[Tomas Skrivan]

Also I could have not been bothered to figure out where I can find the theorem stating ⟪EuclideanSpace.single u 1, s⟫_ℝ = s u. If someone know, please let me know

[ZhiKai Pong]

Tomas Skrivan said:

Also I could have not been bothered to figure out where I can find the theorem stating ⟪EuclideanSpace.single u 1, s⟫_ℝ = s u. If someone know, please let me know

simp [PiLp.inner_apply] works