Physlib.SpaceAndTime.Time.Derivatives — Physlib

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nikolai Kashcheev, Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic
public import Physlib.SpaceAndTime.Space.Module
public import Physlib.SpaceAndTime.Time.Basic
public import Mathlib.Analysis.Calculus.Deriv.Inv
public import Mathlib.Analysis.InnerProductSpace.Calculus

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.

manifoldDeriv : The derivative of a function from Time to a manifold.

iii. Table of contents

A. The definition of the derivative

A.1. Derivatives of functions into vector spaces

A.2. Derivatives of functions into manifolds

B. Linearlity properties of the derivative

C. Derivative of constant functions

D. Smoothness properties

E. Derivatives of components

iv. References

@[expose] public section

A. The definition of the derivative

A.1. Derivatives of functions into vector spaces

@[inherit_doc deriv]
scoped notation "∂ₜ" => deriv

lemma deriv_eq [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (f : Time → M) (t : Time) : Time.deriv f t = fderiv ℝ f t 1 := rfl

A.2. Derivatives of functions into manifolds

B. Linearlity properties of the derivative

              

lemma deriv_smul (f : Time → EuclideanSpace ℝ (Fin d)) (k : ℝ)
    (hf : Differentiable ℝ f) :
    ∂ₜ (fun t => k • f t) t = k • ∂ₜ (fun t => f t) t := byd:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ ∂ₜ (fun t => k • f t) t = k • ∂ₜ (fun t => f t) t
  rw [deriv,d:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ (fderiv ℝ (fun t => k • f t) t) 1 = k • ∂ₜ (fun t => f t) td:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ (k • fderiv ℝ f t) 1 = k • ∂ₜ (fun t => f t) thd:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ DifferentiableAt ℝ f t fderiv_fun_const_smuld:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ (k • fderiv ℝ f t) 1 = k • ∂ₜ (fun t => f t) thd:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ DifferentiableAt ℝ f td:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ (k • fderiv ℝ f t) 1 = k • ∂ₜ (fun t => f t) thd:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ DifferentiableAt ℝ f t]d:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ (k • fderiv ℝ f t) 1 = k • ∂ₜ (fun t => f t) thd:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ DifferentiableAt ℝ f t
  rflhd:ℕt:Timef:Time → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ DifferentiableAt ℝ f t
  fun_propAll goals completed! 🐙

lemma deriv_neg [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) :
    ∂ₜ (-f) t = -∂ₜ f t := byM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → M⊢ ∂ₜ (-f) t = -∂ₜ f t
  rw [deriv,M:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → M⊢ (fderiv ℝ (-f) t) 1 = -∂ₜ f tM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → M⊢ (-fderiv ℝ f t) 1 = -∂ₜ f t fderiv_negM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → M⊢ (-fderiv ℝ f t) 1 = -∂ₜ f tM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → M⊢ (-fderiv ℝ f t) 1 = -∂ₜ f t]M:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → M⊢ (-fderiv ℝ f t) 1 = -∂ₜ f t
  rflAll goals completed! 🐙

lemma deriv_add [NormedAddCommGroup M] [NormedSpace ℝ M] (f g : Time → M)
    (hf : DifferentiableAt ℝ f t) (hg : DifferentiableAt ℝ g t) :
    ∂ₜ (fun s => f s + g s) t = ∂ₜ f t + ∂ₜ g t := byM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mg:Time → Mhf:DifferentiableAt ℝ f thg:DifferentiableAt ℝ g t⊢ ∂ₜ (fun s => f s + g s) t = ∂ₜ f t + ∂ₜ g t
  simp only [Time.deriv_eq]M:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mg:Time → Mhf:DifferentiableAt ℝ f thg:DifferentiableAt ℝ g t⊢ (fderiv ℝ (fun s => f s + g s) t) 1 = (fderiv ℝ f t) 1 + (fderiv ℝ g t) 1
  rw [fderiv_fun_add hf hg,M:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mg:Time → Mhf:DifferentiableAt ℝ f thg:DifferentiableAt ℝ g t⊢ (fderiv ℝ f t + fderiv ℝ g t) 1 = (fderiv ℝ f t) 1 + (fderiv ℝ g t) 1All goals completed! 🐙 _root_.add_applyM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mg:Time → Mhf:DifferentiableAt ℝ f thg:DifferentiableAt ℝ g t⊢ (fderiv ℝ f t) 1 + (fderiv ℝ g t) 1 = (fderiv ℝ f t) 1 + (fderiv ℝ g t) 1All goals completed! 🐙]All goals completed! 🐙

lemma deriv_fun_sum {ι : Type*} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (s : Finset ι) (a : ι → Time → M) (ha : ∀ i ∈ s, DifferentiableAt ℝ (a i) t) :
    ∂ₜ (fun x => ∑ i ∈ s, a i x) t = ∑ i ∈ s, ∂ₜ (a i) t := byM:Typet:Timeι:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Ms:Finset ιa:ι → Time → Mha:∀ i ∈ s, DifferentiableAt ℝ (a i) t⊢ ∂ₜ (fun x => ∑ i ∈ s, a i x) t = ∑ i ∈ s, ∂ₜ (a i) t
  simp only [Time.deriv_eq]M:Typet:Timeι:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Ms:Finset ιa:ι → Time → Mha:∀ i ∈ s, DifferentiableAt ℝ (a i) t⊢ (fderiv ℝ (fun x => ∑ i ∈ s, a i x) t) 1 = ∑ x ∈ s, (fderiv ℝ (a x) t) 1
  rw [fderiv_fun_sum ha,M:Typet:Timeι:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Ms:Finset ιa:ι → Time → Mha:∀ i ∈ s, DifferentiableAt ℝ (a i) t⊢ (∑ i ∈ s, fderiv ℝ (a i) t) 1 = ∑ x ∈ s, (fderiv ℝ (a x) t) 1All goals completed! 🐙 _root_.sum_applyM:Typet:Timeι:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Ms:Finset ιa:ι → Time → Mha:∀ i ∈ s, DifferentiableAt ℝ (a i) t⊢ ∑ i ∈ s, (fderiv ℝ (a i) t) 1 = ∑ x ∈ s, (fderiv ℝ (a x) t) 1All goals completed! 🐙]All goals completed! 🐙

lemma deriv_mul_const (f : Time → ℝ) (c : ℝ) (hf : DifferentiableAt ℝ f t) :
    ∂ₜ (fun s => f s * c) t = ∂ₜ f t * c := byt:Timef:Time → ℝc:ℝhf:DifferentiableAt ℝ f t⊢ ∂ₜ (fun s => f s * c) t = ∂ₜ f t * c
  simp only [Time.deriv_eq]t:Timef:Time → ℝc:ℝhf:DifferentiableAt ℝ f t⊢ (fderiv ℝ (fun s => f s * c) t) 1 = (fderiv ℝ f t) 1 * c
  rw [fderiv_mul_const hf c,t:Timef:Time → ℝc:ℝhf:DifferentiableAt ℝ f t⊢ (c • fderiv ℝ f t) 1 = (fderiv ℝ f t) 1 * cAll goals completed! 🐙 _root_.smul_apply,t:Timef:Time → ℝc:ℝhf:DifferentiableAt ℝ f t⊢ c • (fderiv ℝ f t) 1 = (fderiv ℝ f t) 1 * cAll goals completed! 🐙 smul_eq_mul,t:Timef:Time → ℝc:ℝhf:DifferentiableAt ℝ f t⊢ c * (fderiv ℝ f t) 1 = (fderiv ℝ f t) 1 * cAll goals completed! 🐙 mul_commt:Timef:Time → ℝc:ℝhf:DifferentiableAt ℝ f t⊢ (fderiv ℝ f t) 1 * c = (fderiv ℝ f t) 1 * cAll goals completed! 🐙]All goals completed! 🐙

Quotient rule for Time.deriv on real-valued functions: if c and g are differentiable at t and g t ≠ 0, then ∂ₜ (c / g) t = (∂ₜ c t * g t - c t * ∂ₜ g t) / (g t)^2.


lemma deriv_div {c g : Time → ℝ}
    (hc : DifferentiableAt ℝ c t) (hg : DifferentiableAt ℝ g t) (hgz : g t ≠ 0) :
    ∂ₜ (fun s => c s / g s) t =
      (∂ₜ c t * g t - c t * ∂ₜ g t) / (g t) ^ 2 := byt:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ ∂ₜ (fun s => c s / g s) t = (∂ₜ c t * g t - c t * ∂ₜ g t) / g t ^ 2
  repeat rw [Time.deriv_eqt:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ (fderiv ℝ (fun s => c s / g s) t) 1 = (∂ₜ c t * g t - c t * ∂ₜ g t) / g t ^ 2t:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ (fderiv ℝ (fun s => c s / g s) t) 1 = ((fderiv ℝ c t) 1 * g t - c t * (fderiv ℝ g t) 1) / g t ^ 2]t:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ (fderiv ℝ (fun s => c s / g s) t) 1 = ((fderiv ℝ c t) 1 * g t - c t * ∂ₜ g t) / g t ^ 2t:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ (fderiv ℝ (fun s => c s / g s) t) 1 = ((fderiv ℝ c t) 1 * g t - c t * (fderiv ℝ g t) 1) / g t ^ 2t:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ (fderiv ℝ (fun s => c s / g s) t) 1 = ((fderiv ℝ c t) 1 * g t - c t * (fderiv ℝ g t) 1) / g t ^ 2
  ring_nft:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ (fderiv ℝ (fun s => c s * (g s)⁻¹) t) 1 = (fderiv ℝ c t) 1 * g t * (g t)⁻¹ ^ 2 - c t * (fderiv ℝ g t) 1 * (g t)⁻¹ ^ 2
  simp [fderiv_fun_mul hc (DifferentiableAt.fun_inv (by fun_prop) hgz),
    fderiv_fun_comp t (differentiableAt_inv hgz) hg]t:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ -(c t * ((fderiv ℝ g t) 1 * (g t ^ 2)⁻¹)) + (g t)⁻¹ * (fderiv ℝ c t) 1 =
  (fderiv ℝ c t) 1 * g t * (g t ^ 2)⁻¹ - c t * (fderiv ℝ g t) 1 * (g t ^ 2)⁻¹
  field_simpt:Timec:Time → ℝg:Time → ℝhc:DifferentiableAt ℝ c thg:DifferentiableAt ℝ g thgz:g t ≠ 0⊢ -(c t * (fderiv ℝ g t) 1) + g t * (fderiv ℝ c t) 1 = g t * (fderiv ℝ c t) 1 - c t * (fderiv ℝ g t) 1
  ringAll goals completed! 🐙

C. Derivative of constant functions



@[simp]
lemma deriv_const [NormedAddCommGroup M] [NormedSpace ℝ M] (m : M) :
    ∂ₜ (fun _ => m) t = 0 := byM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mm:M⊢ ∂ₜ (fun x => m) t = 0
  rw [derivM:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mm:M⊢ (fderiv ℝ (fun x => m) t) 1 = 0M:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mm:M⊢ (fderiv ℝ (fun x => m) t) 1 = 0]M:Typet:Timeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mm:M⊢ (fderiv ℝ (fun x => m) t) 1 = 0
  simpAll goals completed! 🐙

D. Smoothness properties

              @[fun_prop]
lemma val_contDiff {n : WithTop ℕ∞} : ContDiff ℝ n Time.val := byn:ℕ∞ω⊢ ContDiff ℝ n val
  change ContDiff ℝ n toRealCLMn:ℕ∞ω⊢ ContDiff ℝ n ⇑toRealCLM
  fun_propAll goals completed! 🐙

@[fun_prop]
lemma deriv_differentiable_of_contDiff {M : Type}
    [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) (hf : ContDiff ℝ ∞ f) :
    Differentiable ℝ (∂ₜ f) := byM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ Differentiable ℝ (∂ₜ f)
  unfold derivM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ Differentiable ℝ fun t => (fderiv ℝ f t) 1
  change Differentiable ℝ ((fun x => x 1) ∘ (fun t => fderiv ℝ f t))M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ Differentiable ℝ ((fun x => x 1) ∘ fun t => fderiv ℝ f t)
  apply Differentiable.comphgM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ Differentiable ℝ fun x => x 1hfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ Differentiable ℝ fun t => fderiv ℝ f t
  ·hgM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ Differentiable ℝ fun x => x 1 fun_propAll goals completed! 🐙
  ·hfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ Differentiable ℝ fun t => fderiv ℝ f t rw [contDiff_infty_iff_fderiv,hfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:Differentiable ℝ f ∧ ContDiff ℝ ∞ (fderiv ℝ f)⊢ Differentiable ℝ fun t => fderiv ℝ f thfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:Differentiable ℝ f ∧ Differentiable ℝ (fderiv ℝ f) ∧ ContDiff ℝ ∞ (fderiv ℝ (fderiv ℝ f))⊢ Differentiable ℝ fun t => fderiv ℝ f t contDiff_infty_iff_fderivhfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:Differentiable ℝ f ∧ Differentiable ℝ (fderiv ℝ f) ∧ ContDiff ℝ ∞ (fderiv ℝ (fderiv ℝ f))⊢ Differentiable ℝ fun t => fderiv ℝ f thfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:Differentiable ℝ f ∧ Differentiable ℝ (fderiv ℝ f) ∧ ContDiff ℝ ∞ (fderiv ℝ (fderiv ℝ f))⊢ Differentiable ℝ fun t => fderiv ℝ f t] at hfhfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:Differentiable ℝ f ∧ Differentiable ℝ (fderiv ℝ f) ∧ ContDiff ℝ ∞ (fderiv ℝ (fderiv ℝ f))⊢ Differentiable ℝ fun t => fderiv ℝ f t
    exact hf.2.1All goals completed! 🐙@[fun_prop]
lemma deriv_contDiff_of_contDiff {M : Type}
    [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) (hf : ContDiff ℝ ∞ f) :
    ContDiff ℝ ∞ (∂ₜ f) := byM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ (∂ₜ f)
  unfold derivM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ fun t => (fderiv ℝ f t) 1
  change ContDiff ℝ ∞ ((fun x => x 1) ∘ (fun t => fderiv ℝ f t))M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ ((fun x => x 1) ∘ fun t => fderiv ℝ f t)
  apply ContDiff.comphgM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ fun x => x 1hfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ fun t => fderiv ℝ f t <;>hgM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ fun x => x 1hfM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Mhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ fun t => fderiv ℝ f t fun_propAll goals completed! 🐙@[fun_prop]
lemma deriv_contDiff_of_space {n} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : Time → Space d → M) (hf : ContDiff ℝ (n + 1) ↿f) :
    ContDiff ℝ n fun (x : Space d) => (∂ₜ fun t => f t x) t := byd:ℕt:Timen:ℕ∞ωM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ (n + 1) ↿f⊢ ContDiff ℝ n fun x => ∂ₜ (fun t => f t x) t
  unfold derivd:ℕt:Timen:ℕ∞ωM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ (n + 1) ↿f⊢ ContDiff ℝ n fun x => (fderiv ℝ (fun t => f t x) t) 1
  fun_propAll goals completed! 🐙

E. Derivatives of components

              

lemma differentiable_euclid {f : Time → EuclideanSpace ℝ (Fin n)}
    (hf : ∀ i, Differentiable ℝ (fun t => f t i)) :
    Differentiable ℝ f := byn:ℕf:Time → EuclideanSpace ℝ (Fin n)hf:∀ (i : Fin n), Differentiable ℝ fun t => (f t).ofLp i⊢ Differentiable ℝ f
  rw [differentiable_euclideann:ℕf:Time → EuclideanSpace ℝ (Fin n)hf:∀ (i : Fin n), Differentiable ℝ fun t => (f t).ofLp i⊢ ∀ (i : Fin n), Differentiable ℝ fun x => (f x).ofLp in:ℕf:Time → EuclideanSpace ℝ (Fin n)hf:∀ (i : Fin n), Differentiable ℝ fun t => (f t).ofLp i⊢ ∀ (i : Fin n), Differentiable ℝ fun x => (f x).ofLp i]n:ℕf:Time → EuclideanSpace ℝ (Fin n)hf:∀ (i : Fin n), Differentiable ℝ fun t => (f t).ofLp i⊢ ∀ (i : Fin n), Differentiable ℝ fun x => (f x).ofLp i
  fun_propAll goals completed! 🐙

lemma deriv_euclid { μ} {f : Time→ EuclideanSpace ℝ (Fin n)}
    (hf : Differentiable ℝ f) (t : Time) :
    deriv (fun t => f t μ) t = deriv (fun t => f t) t μ := byn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ ∂ₜ (fun t => (f t).ofLp μ) t = (∂ₜ (fun t => f t) t).ofLp μ
  rw [deriv_eqn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (fun t => (f t).ofLp μ) t) 1 = (∂ₜ (fun t => f t) t).ofLp μn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (fun t => (f t).ofLp μ) t) 1 = (∂ₜ (fun t => f t) t).ofLp μ]n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (fun t => (f t).ofLp μ) t) 1 = (∂ₜ (fun t => f t) t).ofLp μ
  change fderiv ℝ (EuclideanSpace.proj μ ∘ fun x => f x) t 1 = _n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ) ∘ fun x => f x) t) 1 = (∂ₜ (fun t => f t) t).ofLp μ
  rw [fderiv_compn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = (∂ₜ (fun t => f t) t).ofLp μhgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t)hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (fun x => f x) tn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = (∂ₜ (fun t => f t) t).ofLp μhgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t)hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (fun x => f x) t]n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = (∂ₜ (fun t => f t) t).ofLp μhgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t)hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (fun x => f x) t
  ·n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = (∂ₜ (fun t => f t) t).ofLp μ simp only [ContinuousLinearMap.fderiv, ContinuousLinearMap.coe_comp, Function.comp_apply,
    PiLp.proj_apply]n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ ((fderiv ℝ (fun x => f x) t) 1).ofLp μ = (∂ₜ (fun x => f x) t).ofLp μ
    rw [← deriv_eqn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ (∂ₜ (fun x => f x) t).ofLp μ = (∂ₜ (fun x => f x) t).ofLp μAll goals completed! 🐙]All goals completed! 🐙
  ·hgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t) fun_propAll goals completed! 🐙
  ·hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Time⊢ DifferentiableAt ℝ (fun x => f x) t fun_propAll goals completed! 🐙

lemma fderiv_euclid { μ} {f : Time→ EuclideanSpace ℝ (Fin n)}
    (hf : Differentiable ℝ f) (t dt : Time) :
    fderiv ℝ (fun t => f t μ) t dt = fderiv ℝ (fun t => f t) t dt μ := byn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ (fderiv ℝ (fun t => (f t).ofLp μ) t) dt = ((fderiv ℝ (fun t => f t) t) dt).ofLp μ
  change fderiv ℝ (EuclideanSpace.proj μ ∘ fun x => f x) t dt = _n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ) ∘ fun x => f x) t) dt = ((fderiv ℝ (fun t => f t) t) dt).ofLp μ
  rw [fderiv_compn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) dt = ((fderiv ℝ (fun t => f t) t) dt).ofLp μhgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t)hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (fun x => f x) tn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) dt = ((fderiv ℝ (fun t => f t) t) dt).ofLp μhgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t)hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (fun x => f x) t]n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) dt = ((fderiv ℝ (fun t => f t) t) dt).ofLp μhgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t)hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (fun x => f x) t
  ·n:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ (fderiv ℝ (⇑(EuclideanSpace.proj μ)) (f t) ∘SL fderiv ℝ (fun x => f x) t) dt = ((fderiv ℝ (fun t => f t) t) dt).ofLp μ simp [-EuclideanSpace.coe_proj]All goals completed! 🐙
  ·hgn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj μ)) (f t) fun_propAll goals completed! 🐙
  ·hfn:ℕμ:Fin nf:Time → EuclideanSpace ℝ (Fin n)hf:Differentiable ℝ ft:Timedt:Time⊢ DifferentiableAt ℝ (fun x => f x) t fun_propAll goals completed! 🐙

lemma deriv_lorentzVector {d : ℕ} {f : Time → Lorentz.Vector d}
    (hf : Differentiable ℝ f) (t : Time) (i : Fin 1 ⊕ Fin d) :
    deriv (fun t => f t i) t = deriv (fun t => f t) t i := byd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ ∂ₜ (fun t => f t i) t = ∂ₜ (fun t => f t) t i
  rw [deriv_eqd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (fun t => f t i) t) 1 = ∂ₜ (fun t => f t) t id:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (fun t => f t i) t) 1 = ∂ₜ (fun t => f t) t i]d:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (fun t => f t i) t) 1 = ∂ₜ (fun t => f t) t i
  change fderiv ℝ (Lorentz.Vector.coordCLM i ∘ fun x => f x) t 1 = _d:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM i) ∘ fun x => f x) t) 1 = ∂ₜ (fun t => f t) t i
  rw [fderiv_compd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = ∂ₜ (fun t => f t) t ihgd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t)hfd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (fun x => f x) td:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = ∂ₜ (fun t => f t) t ihgd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t)hfd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (fun x => f x) t]d:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = ∂ₜ (fun t => f t) t ihgd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t)hfd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (fun x => f x) t
  ·d:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t) ∘SL fderiv ℝ (fun x => f x) t) 1 = ∂ₜ (fun t => f t) t i simpd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (Lorentz.Vector.coordCLM i) ((fderiv ℝ (fun x => f x) t) 1) = ∂ₜ (fun x => f x) t i
    rw [← deriv_eqd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (Lorentz.Vector.coordCLM i) (∂ₜ (fun x => f x) t) = ∂ₜ (fun x => f x) t id:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (Lorentz.Vector.coordCLM i) (∂ₜ (fun x => f x) t) = ∂ₜ (fun x => f x) t i]d:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ (Lorentz.Vector.coordCLM i) (∂ₜ (fun x => f x) t) = ∂ₜ (fun x => f x) t i
    rflAll goals completed! 🐙
  ·hgd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (⇑(Lorentz.Vector.coordCLM i)) (f t) fun_propAll goals completed! 🐙
  ·hfd:ℕf:Time → Lorentz.Vector dhf:Differentiable ℝ ft:Timei:Fin 1 ⊕ Fin d⊢ DifferentiableAt ℝ (fun x => f x) t fun_propAll goals completed! 🐙lemma deriv_space {d : ℕ} {f : Time → Space d}
    (hf : Differentiable ℝ f) (t : Time) (i : Fin d) :
    deriv (fun s => f s i) t = deriv f t i :=
  (Space.fderiv_space_components i f hf t 1).symm