Time Derivatives

i. Overview

In this module we define and prove basic lemmas about derivatives of functions on Time.

ii. Key results

• deriv : The derivative of a function Time → M at a given time.

iii. Table of contents

• A. The definition of the derivative
• B. Linearlity properties of the derivative
• C. Derivative of constant functions
• D. Smoothness properties of the derivative
• E. Derivatives of components

iv. References

A. The definition of the derivative

noncomputable def Time.deriv {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (f : Time → M) : Time → M

Given a function f : Time → M the derivative of f.

Equations

• Time.deriv f t = (fderiv ℝ f t) 1

def Time.«term∂ₜ» : Lean.ParserDescr

Given a function f : Time → M the derivative of f.

Equations

• Time.«term∂ₜ» = Lean.ParserDescr.node `Time.«term∂ₜ» 1024 (Lean.ParserDescr.symbol "∂ₜ")

theorem Time.deriv_eq {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (f : Time → M) (t : Time) : deriv f t = (fderiv ℝ f t) 1

B. Linearlity properties of the derivative

theorem Time.deriv_smul {d : ℕ} {t : Time} (f : Time → EuclideanSpace ℝ (Fin d)) (k : ℝ) (hf : Differentiable ℝ f) : deriv (fun (t : Time) => k • f t) t = k • deriv (fun (t : Time) => f t) t

theorem Time.deriv_neg {M : Type} {t : Time} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) : deriv (-f) t = -deriv f t

C. Derivative of constant functions

@[simp]

theorem Time.deriv_const {M : Type} {t : Time} [NormedAddCommGroup M] [NormedSpace ℝ M] (m : M) : deriv (fun (x : Time) => m) t = 0

D. Smoothness properties of the derivative

theorem Time.deriv_differentiable_of_contDiff {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) (hf : ContDiff ℝ (↑⊤) f) : Differentiable ℝ (deriv f)

theorem Time.deriv_contDiff_of_contDiff {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (deriv f)

E. Derivatives of components

theorem Time.deriv_euclid {n : ℕ} {μ : Fin n} {f : Time → EuclideanSpace ℝ (Fin n)} (hf : Differentiable ℝ f) (t : Time) : deriv (fun (t : Time) => f t μ) t = deriv (fun (t : Time) => f t) t μ

theorem Time.deriv_lorentzVector {d : ℕ} {f : Time → Lorentz.Vector d} (hf : Differentiable ℝ f) (t : Time) (i : Fin 1 ⊕ Fin d) : deriv (fun (t : Time) => f t i) t = deriv (fun (t : Time) => f t) t i