Physlib.SpaceAndTime.TimeAndSpace.Basic

Imports

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

public import Physlib.SpaceAndTime.Space.Derivatives.Curl

Functions and distributions on Time and Space d

i. Overview

In this module we define TimeAndSpace d as the product of Time and Space d, and prove basic lemmas about derivatives of functions and distributions on both coordinates.

The derivative and distribution results are in the namespace Space by convention.

ii. Key results

TimeAndSpace d : Euclidean spacetime as the product of time and space.

TimeAndSpace.time : The projection from TimeAndSpace d to Time.

TimeAndSpace.space : The projection from TimeAndSpace d to Space d.

distTimeDeriv : The derivative of a distribution on Time × Space d along the temporal coordinate.

distSpaceDeriv : The derivative of a distribution on Time × Space d along the spatial i coordinate.

distSpaceGrad : The spatial gradient of a distribution on Time × Space d.

distSpaceDiv : The spatial divergence of a distribution on Time × Space d.

distSpaceCurl : The spatial curl of a distribution on Time × Space 3.

iii. Table of contents

A. The coordinate product and derivatives involving time and space

A.1. The TimeAndSpace coordinate product

A.2. Space and time derivatives in terms of curried functions

A.3. Commuting time and space derivatives

A.4. Differentiablity conditions

A.5. Time derivative commute with curl

A.6. Constant of time deriative and space derivatives zero

A.7. Equal up to a constant of time and space derivatives equal

B. Derivatives of distributions on Time × Space d

B.1. Time derivatives

B.1.1. Composition with a CLM

B.2. Space derivatives

B.2.1. Space derivatives commute

B.2.2. Composition with a CLM

B.3. Time and space derivatives commute

B.4. The spatial gradient

B.5. The spatial divergence

B.6. The spatial curl

iv. References

@[expose] public section

A. The coordinate product and derivatives involving time and space

A.1. The `TimeAndSpace` coordinate product

Euclidean spacetime as the product of time and d-dimensional space.

abbrev TimeAndSpace (d : ℕ := 3) := Time × Space d

@[simp]
lemma time_apply (tx : TimeAndSpace d) :
    time tx = tx.1 := rfl

@[simp]
lemma space_apply (tx : TimeAndSpace d) :
    space tx = tx.2 := rfl

The time projection is nonexpanding for the product metric.


lemma dist_time_le (tx ty : TimeAndSpace d) :
    dist (time tx) (time ty) ≤ dist tx ty := byd:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (time tx) (time ty) ≤ dist tx ty
  rw [Prod.dist_eqd:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (time tx) (time ty) ≤ max (dist tx.1 ty.1) (dist tx.2 ty.2)d:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (time tx) (time ty) ≤ max (dist tx.1 ty.1) (dist tx.2 ty.2)]d:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (time tx) (time ty) ≤ max (dist tx.1 ty.1) (dist tx.2 ty.2)
  exact le_max_left _ _All goals completed! 🐙

The spatial projection is nonexpanding for the product metric.


lemma dist_space_le (tx ty : TimeAndSpace d) :
    dist (space tx) (space ty) ≤ dist tx ty := byd:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (space tx) (space ty) ≤ dist tx ty
  rw [Prod.dist_eqd:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (space tx) (space ty) ≤ max (dist tx.1 ty.1) (dist tx.2 ty.2)d:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (space tx) (space ty) ≤ max (dist tx.1 ty.1) (dist tx.2 ty.2)]d:ℕtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (space tx) (space ty) ≤ max (dist tx.1 ty.1) (dist tx.2 ty.2)
  exact le_max_right _ _All goals completed! 🐙

A.2. Space and time derivatives in terms of curried functions



lemma fderiv_space_eq_fderiv_curry {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : Time → Space d → M) (t : Time) (x dx : Space d)
    (hf : Differentiable ℝ ↿f) :
    fderiv ℝ (fun x' => f t x') x dx = fderiv ℝ ↿f (t, x) (0, dx) := byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ (fun x' => f t x') x) dx = (fderiv ℝ ↿f (t, x)) (0, dx)
  change fderiv ℝ (↿f ∘ fun x' => (t, x')) x dx = _d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ (↿f ∘ fun x' => (t, x')) x) dx = (fderiv ℝ ↿f (t, x)) (0, dx)
  rw [fderiv_comp,d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun x' => (t, x')) x) dx = (fderiv ℝ ↿f (t, x)) (0, dx)hgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => (t, x')) xd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun x' => t) x).prod (fderiv ℝ (fun x' => x') x)) dx = (fderiv ℝ ↿f (t, x)) (0, dx)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => t) xhf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => x') xhgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => (t, x')) x DifferentiableAt.fderiv_prodMkd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun x' => t) x).prod (fderiv ℝ (fun x' => x') x)) dx = (fderiv ℝ ↿f (t, x)) (0, dx)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => t) xhf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => x') xhgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => (t, x')) xd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun x' => t) x).prod (fderiv ℝ (fun x' => x') x)) dx = (fderiv ℝ ↿f (t, x)) (0, dx)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => t) xhf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => x') xhgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => (t, x')) x]d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun x' => t) x).prod (fderiv ℝ (fun x' => x') x)) dx = (fderiv ℝ ↿f (t, x)) (0, dx)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => t) xhf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => x') xhgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => (t, x')) x
  simp only [ContinuousLinearMap.coe_comp, Function.comp_apply, fderiv_fun_const, Pi.zero_apply,
    fderiv_fun_id, ContinuousLinearMap.prod_apply, _root_.zero_apply,
    ContinuousLinearMap.coe_id', id_eq]hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => t) xhf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => x') xhgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timex:Space ddx:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun x' => (t, x')) x
  repeat' fun_propAll goals completed! 🐙



lemma fderiv_time_eq_fderiv_curry {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : Time → Space d → M) (t dt : Time) (x : Space d)
    (hf : Differentiable ℝ ↿f) :
    fderiv ℝ (fun t' => f t' x) t dt = fderiv ℝ ↿f (t, x) (dt, 0) := byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ (fun t' => f t' x) t) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)
  change fderiv ℝ (↿f ∘ fun t' => (t', x)) t dt = _d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ (↿f ∘ fun t' => (t', x)) t) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)
  rw [fderiv_comp,d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun t' => (t', x)) t) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)hgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => (t', x)) td:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun t' => t') t).prod (fderiv ℝ (fun t' => x) t)) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => t') thf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => x) thgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => (t', x)) t DifferentiableAt.fderiv_prodMkd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun t' => t') t).prod (fderiv ℝ (fun t' => x) t)) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => t') thf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => x) thgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => (t', x)) td:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun t' => t') t).prod (fderiv ℝ (fun t' => x) t)) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => t') thf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => x) thgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => (t', x)) t]d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL (fderiv ℝ (fun t' => t') t).prod (fderiv ℝ (fun t' => x) t)) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => t') thf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => x) thgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => (t', x)) t
  simp only [ContinuousLinearMap.coe_comp, Function.comp_apply, fderiv_fun_id, fderiv_fun_const,
    Pi.zero_apply, ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq,
    _root_.zero_apply]hf₁d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => t') thf₂d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => x) thgd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ ↿f (t, x)hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space dhf:Differentiable ℝ ↿f⊢ DifferentiableAt ℝ (fun t' => (t', x)) t
  repeat' fun_propAll goals completed! 🐙

A.3. Commuting time and space derivatives

Derivatives along space coordinates and time commute.


lemma fderiv_time_commute_fderiv_space {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : Time → Space d → M) (t dt : Time) (x dx : Space d)
    (hf : ContDiff ℝ 2 ↿f) :
    fderiv ℝ (fun t' => fderiv ℝ (fun x' => f t' x') x dx) t dt
    = fderiv ℝ (fun x' => fderiv ℝ (fun t' => f t' x') t dt) x dx := byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun t' => (fderiv ℝ (fun x' => f t' x') x) dx) t) dt =
  (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt) x) dx
  trans fderiv ℝ (fun t' => (fderiv ℝ (↿f) (t', x) (0, dx))) t dtd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun t' => (fderiv ℝ (fun x' => f t' x') x) dx) t) dt =
  (fderiv ℝ (fun t' => (fderiv ℝ ↿f (t', x)) (0, dx)) t) dtd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun t' => (fderiv ℝ ↿f (t', x)) (0, dx)) t) dt =
  (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt) x) dx
  ·d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun t' => (fderiv ℝ (fun x' => f t' x') x) dx) t) dt =
  (fderiv ℝ (fun t' => (fderiv ℝ ↿f (t', x)) (0, dx)) t) dt congre_fd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fun t' => (fderiv ℝ (fun x' => f t' x') x) dx) = fun t' => (fderiv ℝ ↿f (t', x)) (0, dx)
    funext t'e_fd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿ft':Time⊢ (fderiv ℝ (fun x' => f t' x') x) dx = (fderiv ℝ ↿f (t', x)) (0, dx)
    exact fderiv_space_eq_fderiv_curry f t' x dx (hf.differentiable (byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿ft':Time⊢ 2 ≠ 0 simpAll goals completed! 🐙))
  trans fderiv ℝ (fun x => (fderiv ℝ (↿f) x (0, dx))) (t, x) (dt, 0)d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun t' => (fderiv ℝ ↿f (t', x)) (0, dx)) t) dt =
  (fderiv ℝ (fun x => (fderiv ℝ (↿f) x) (0, dx)) (t, x)) (dt, 0)d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun x => (fderiv ℝ (↿f) x) (0, dx)) (t, x)) (dt, 0) =
  (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt) x) dx
  ·d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun t' => (fderiv ℝ ↿f (t', x)) (0, dx)) t) dt =
  (fderiv ℝ (fun x => (fderiv ℝ (↿f) x) (0, dx)) (t, x)) (dt, 0) exact fderiv_time_eq_fderiv_curry (fun t x => fderiv ℝ ↿f (t, x) (0, dx)) t dt x (byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ Differentiable ℝ ↿fun t x => (fderiv ℝ ↿f (t, x)) (0, dx) fun_propAll goals completed! 🐙)
  symmd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt) x) dx =
  (fderiv ℝ (fun x => (fderiv ℝ (↿f) x) (0, dx)) (t, x)) (dt, 0)
  trans fderiv ℝ (fun x' => (fderiv ℝ (↿f) (t, x') (dt, 0))) x dxd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt) x) dx =
  (fderiv ℝ (fun x' => (fderiv ℝ ↿f (t, x')) (dt, 0)) x) dxd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun x' => (fderiv ℝ ↿f (t, x')) (dt, 0)) x) dx =
  (fderiv ℝ (fun x => (fderiv ℝ (↿f) x) (0, dx)) (t, x)) (dt, 0)
  ·d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt) x) dx =
  (fderiv ℝ (fun x' => (fderiv ℝ ↿f (t, x')) (dt, 0)) x) dx congre_fd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt) = fun x' => (fderiv ℝ ↿f (t, x')) (dt, 0)
    funext x'e_fd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿fx':Space d⊢ (fderiv ℝ (fun t' => f t' x') t) dt = (fderiv ℝ ↿f (t, x')) (dt, 0)
    exact fderiv_time_eq_fderiv_curry f t dt x' (hf.differentiable (byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿fx':Space d⊢ 2 ≠ 0 simpAll goals completed! 🐙))
  trans fderiv ℝ (fun t => (fderiv ℝ (↿f) t (dt, 0))) (t, x) (0, dx)d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun x' => (fderiv ℝ ↿f (t, x')) (dt, 0)) x) dx =
  (fderiv ℝ (fun t => (fderiv ℝ (↿f) t) (dt, 0)) (t, x)) (0, dx)d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun t => (fderiv ℝ (↿f) t) (dt, 0)) (t, x)) (0, dx) =
  (fderiv ℝ (fun x => (fderiv ℝ (↿f) x) (0, dx)) (t, x)) (dt, 0)
  ·d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ (fun x' => (fderiv ℝ ↿f (t, x')) (dt, 0)) x) dx =
  (fderiv ℝ (fun t => (fderiv ℝ (↿f) t) (dt, 0)) (t, x)) (0, dx) exact fderiv_space_eq_fderiv_curry (fun t x => fderiv ℝ ↿f (t, x) (dt, 0)) t x dx (byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ Differentiable ℝ ↿fun t x => (fderiv ℝ ↿f (t, x)) (dt, 0) fun_propAll goals completed! 🐙)
  rw [fderiv_clm_apply,d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun t => (dt, 0)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (dt, 0)) (0, dx) =
  (fderiv ℝ (fun x => (fderiv ℝ (↿f) x) (0, dx)) (t, x)) (dt, 0)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun t => (dt, 0)) (t, x)d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun t => (dt, 0)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (dt, 0)) (0, dx) =
  (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun x => (0, dx)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (0, dx)) (dt, 0)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun x => (0, dx)) (t, x)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun t => (dt, 0)) (t, x) fderiv_clm_applyd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun t => (dt, 0)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (dt, 0)) (0, dx) =
  (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun x => (0, dx)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (0, dx)) (dt, 0)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun x => (0, dx)) (t, x)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun t => (dt, 0)) (t, x)d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun t => (dt, 0)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (dt, 0)) (0, dx) =
  (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun x => (0, dx)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (0, dx)) (dt, 0)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun x => (0, dx)) (t, x)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun t => (dt, 0)) (t, x)]d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun t => (dt, 0)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (dt, 0)) (0, dx) =
  (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun x => (0, dx)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (0, dx)) (dt, 0)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun x => (0, dx)) (t, x)hcd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fderiv ℝ ↿f) (t, x)hud:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ DifferentiableAt ℝ (fun t => (dt, 0)) (t, x)
  ·d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun t => (dt, 0)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (dt, 0)) (0, dx) =
  (fderiv ℝ ↿f (t, x) ∘SL fderiv ℝ (fun x => (0, dx)) (t, x) + (fderiv ℝ (fderiv ℝ ↿f) (t, x)).flip (0, dx)) (dt, 0) simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,
      ContinuousLinearMap.flip_apply]d:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ ((fderiv ℝ (fderiv ℝ ↿f) (t, x)) (0, dx)) (dt, 0) = ((fderiv ℝ (fderiv ℝ ↿f) (t, x)) (dt, 0)) (0, dx)
    exact (hf.contDiffAt.isSymmSndFDerivAt (byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mt:Timedt:Timex:Space ddx:Space dhf:ContDiff ℝ 2 ↿f⊢ minSmoothness ℝ 2 ≤ 2 simpAll goals completed! 🐙)).eq (0, dx) (dt, 0)
  all_goals fun_propAll goals completed! 🐙

lemma time_deriv_comm_space_deriv {d i} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {f : Time → Space d → M} (hf : ContDiff ℝ 2 ↿f) (t : Time) (x : Space d) :
    Time.deriv (fun t' => Space.deriv i (f t') x) t
    = Space.deriv i (fun x' => Time.deriv (fun t' => f t' x') t) x := byd:ℕi:Fin dM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timex:Space d⊢ Time.deriv (fun t' => deriv i (f t') x) t = deriv i (fun x' => Time.deriv (fun t' => f t' x') t) x
  simp only [Time.deriv_eq, Space.deriv_eq_fderiv_basis]d:ℕi:Fin dM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timex:Space d⊢ (fderiv ℝ (fun t' => (fderiv ℝ (f t') x) (basis i)) t) 1 =
  (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) 1) x) (basis i)
  exact fderiv_time_commute_fderiv_space f t 1 x (Space.basis i) hfAll goals completed! 🐙

A.4. Differentiablity conditions

              

@[fun_prop]
lemma space_deriv_differentiable_time {d i} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {f : Time → Space d → M} (hf : ContDiff ℝ 2 ↿f) (x : Space d) :
    Differentiable ℝ (fun t => Space.deriv i (f t) x) := byd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d⊢ Differentiable ℝ fun t => deriv i (f t) x
  conv =>d:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d| Differentiable ℝ fun t => deriv i (f t) x
    enter [2, t]d:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dt:Time| deriv i (f t) x;
    rw [Space.deriv_eq_fderiv_basis]d:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dt:Time| (fderiv ℝ (f t) x) (basis i)
  apply Differentiable.clm_applyhcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d⊢ Differentiable ℝ fun y => fderiv ℝ (f y) xhud:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d⊢ Differentiable ℝ fun y => basis i
  ·hcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x have hdd : Differentiable ℝ ↿f := hf.differentiable (byd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d⊢ 2 ≠ 0hcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿f⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x simpAll goals completed! 🐙hcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿f⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x)hcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿f⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x
    have h1 (t : Time) : fderiv ℝ (fun x => f t x) x
      = fderiv ℝ (↿f) (t, x) ∘L (ContinuousLinearMap.inr ℝ Time (Space d)) := byd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d⊢ Differentiable ℝ fun t => deriv i (f t) xhcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x
      ext wd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿ft:Timew:Space d⊢ (fderiv ℝ (fun x => f t x) x) w = (fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)) whcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x
      simp only [ContinuousLinearMap.coe_comp, Function.comp_apply, ContinuousLinearMap.inr_apply]d:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿ft:Timew:Space d⊢ (fderiv ℝ (fun x => f t x) x) w = (fderiv ℝ ↿f (t, x)) (0, w)hcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x
      rw [← fderiv_space_eq_fderiv_curry f t x w hddd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿ft:Timew:Space d⊢ (fderiv ℝ (fun x => f t x) x) w = (fderiv ℝ (fun x' => f t x') x) whcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x]hcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (f y) xhcd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (f y) x
    conv =>d:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)| Differentiable ℝ fun y => fderiv ℝ (f y) x
      enter [2, y]d:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)y:Time| fderiv ℝ (f y) x
      change fderiv ℝ (fun x => f y x) xd:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)y:Time| fderiv ℝ (fun x => f y x) x
      rw [h1]d:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space dhdd:Differentiable ℝ ↿fh1:∀ (t : Time), fderiv ℝ (fun x => f t x) x = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)y:Time| fderiv ℝ ↿f (y, x) ∘SL ContinuousLinearMap.inr ℝ Time (Space d)
    fun_propAll goals completed! 🐙
  ·hud:ℕi:Fin dM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿fx:Space d⊢ Differentiable ℝ fun y => basis i fun_propAll goals completed! 🐙

@[fun_prop]
lemma time_deriv_differentiable_space {d } {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {f : Time → Space d → M} (hf : ContDiff ℝ 2 ↿f) (t : Time) :
    Differentiable ℝ (fun x => Time.deriv (f · x) t) := byd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time⊢ Differentiable ℝ fun x => Time.deriv (fun x_1 => f x_1 x) t
  conv =>d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time| Differentiable ℝ fun x => Time.deriv (fun x_1 => f x_1 x) t
    enter [2, x]d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timex:Space d| Time.deriv (fun x_1 => f x_1 x) t;
    rw [Time.deriv_eq]d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timex:Space d| (fderiv ℝ (fun x_1 => f x_1 x) t) 1
  apply Differentiable.clm_applyhcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) thud:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time⊢ Differentiable ℝ fun y => 1
  ·hcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t have hdd : Differentiable ℝ ↿f := hf.differentiable (byd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time⊢ 2 ≠ 0hcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿f⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t simpAll goals completed! 🐙hcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿f⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t)hcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿f⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t
    have h1 (x : Space d) : fderiv ℝ (fun t => f t x) t
      = fderiv ℝ (↿f) (t, x) ∘L (ContinuousLinearMap.inl ℝ Time (Space d)) := byd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time⊢ Differentiable ℝ fun x => Time.deriv (fun x_1 => f x_1 x) thcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t
      ext wd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fx:Space dw:Time⊢ (fderiv ℝ (fun t => f t x) t) w = (fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)) whcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t
      simp only [ContinuousLinearMap.coe_comp, Function.comp_apply, ContinuousLinearMap.inl_apply]d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fx:Space dw:Time⊢ (fderiv ℝ (fun t => f t x) t) w = (fderiv ℝ ↿f (t, x)) (w, 0)hcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t
      rw [← fderiv_time_eq_fderiv_curry f t w x hddd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fx:Space dw:Time⊢ (fderiv ℝ (fun t => f t x) t) w = (fderiv ℝ (fun t' => f t' x) t) whcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t]hcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) thcd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)⊢ Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t
    conv =>d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)| Differentiable ℝ fun y => fderiv ℝ (fun x => f x y) t
      enter [2, t']d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)t':Space d| fderiv ℝ (fun x => f x t') t
      change fderiv ℝ (fun x => f x t') td:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)t':Space d| fderiv ℝ (fun x => f x t') t
      rw [h1]d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Timehdd:Differentiable ℝ ↿fh1:∀ (x : Space d), fderiv ℝ (fun t => f t x) t = fderiv ℝ ↿f (t, x) ∘SL ContinuousLinearMap.inl ℝ Time (Space d)t':Space d| fderiv ℝ ↿f (t, t') ∘SL ContinuousLinearMap.inl ℝ Time (Space d)
    fun_propAll goals completed! 🐙
  ·hud:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:ContDiff ℝ 2 ↿ft:Time⊢ Differentiable ℝ fun y => 1 fun_propAll goals completed! 🐙

@[fun_prop]
lemma curl_differentiable_time
    (fₜ : Time → Space → EuclideanSpace ℝ (Fin 3))
    (hf : ContDiff ℝ 2 ↿fₜ) (x : Space) :
    Differentiable ℝ (fun t => (∇ ⨯ fₜ t) x) := byfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun t => curl (fₜ t) x
  rw [differentiable_euclideanfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ ∀ (i : Fin 3), Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp ifₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ ∀ (i : Fin 3), Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp i]fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ ∀ (i : Fin 3), Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp i
  intro ifₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Spacei:Fin 3⊢ Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp i
  fin_cases i«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp ((fun i => i) ⟨0, ⋯⟩)«1»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp ((fun i => i) ⟨1, ⋯⟩)«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp ((fun i => i) ⟨2, ⋯⟩) <;>«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp ((fun i => i) ⟨0, ⋯⟩)«1»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp ((fun i => i) ⟨1, ⋯⟩)«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 => (curl (fₜ x_1) x).ofLp ((fun i => i) ⟨2, ⋯⟩) simp only [Fin.zero_eta, Fin.isValue, curl]«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 =>
  deriv (⟨2, ⋯⟩ + 1) (fun x => (fₜ x_1 x).ofLp (⟨2, ⋯⟩ + 2)) x -
    deriv (⟨2, ⋯⟩ + 2) (fun x => (fₜ x_1 x).ofLp (⟨2, ⋯⟩ + 1)) x <;>«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 =>
  deriv (0 + 1) (fun x => (fₜ x_1 x).ofLp (0 + 2)) x - deriv (0 + 2) (fun x => (fₜ x_1 x).ofLp (0 + 1)) x«1»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 =>
  deriv (⟨1, ⋯⟩ + 1) (fun x => (fₜ x_1 x).ofLp (⟨1, ⋯⟩ + 2)) x -
    deriv (⟨1, ⋯⟩ + 2) (fun x => (fₜ x_1 x).ofLp (⟨1, ⋯⟩ + 1)) x«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 ↿fₜx:Space⊢ Differentiable ℝ fun x_1 =>
  deriv (⟨2, ⋯⟩ + 1) (fun x => (fₜ x_1 x).ofLp (⟨2, ⋯⟩ + 2)) x -
    deriv (⟨2, ⋯⟩ + 2) (fun x => (fₜ x_1 x).ofLp (⟨2, ⋯⟩ + 1)) x fun_propAll goals completed! 🐙

A.5. Time derivative commute with curl

Curl and time derivative commute.


lemma time_deriv_curl_commute (fₜ : Time → Space → EuclideanSpace ℝ (Fin 3))
    (t : Time) (x : Space) (hf : ContDiff ℝ 2 ↿fₜ) :
    ∂ₜ (fun t => (∇ ⨯ fₜ t) x) t = (∇ ⨯ fun x => (∂ₜ (fun t => fₜ t x) t)) x:= byfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ∂ₜ (fun t => curl (fₜ t) x) t = curl (fun x => ∂ₜ (fun t => fₜ t x) t) x
  ext ifₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ (∂ₜ (fun t => curl (fₜ t) x) t).ofLp i = (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp i
  rw [← Time.deriv_euclidfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ ∂ₜ (fun t => (curl (fₜ t) x).ofLp i) t = (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp ihffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ Differentiable ℝ fun t => curl (fₜ t) xfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ ∂ₜ (fun t => (curl (fₜ t) x).ofLp i) t = (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp ihffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ Differentiable ℝ fun t => curl (fₜ t) x]fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ ∂ₜ (fun t => (curl (fₜ t) x).ofLp i) t = (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp ihffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ Differentiable ℝ fun t => curl (fₜ t) x
  ·fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ ∂ₜ (fun t => (curl (fₜ t) x).ofLp i) t = (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp i fin_cases i«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ∂ₜ (fun t => (curl (fₜ t) x).ofLp ((fun i => i) ⟨0, ⋯⟩)) t =
  (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp ((fun i => i) ⟨0, ⋯⟩)«1»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ∂ₜ (fun t => (curl (fₜ t) x).ofLp ((fun i => i) ⟨1, ⋯⟩)) t =
  (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp ((fun i => i) ⟨1, ⋯⟩)«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ∂ₜ (fun t => (curl (fₜ t) x).ofLp ((fun i => i) ⟨2, ⋯⟩)) t =
  (curl (fun x => ∂ₜ (fun t => fₜ t x) t) x).ofLp ((fun i => i) ⟨2, ⋯⟩)
    all_goals
    simp [curl]«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ∂ₜ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x - deriv 1 (fun x => (fₜ t x).ofLp 0) x) t =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x
    rw [Time.deriv_eq,«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fderiv ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 2) x - deriv 2 (fun x => (fₜ t x).ofLp 1) x) t) 1 =
  deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 2) x - deriv 2 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fderiv ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t -
      fderiv ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t)
    1 =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t fderiv_fun_sub«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fderiv ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 2) x) t -
      fderiv ℝ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 1) x) t)
    1 =
  deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 2) x - deriv 2 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x«0».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 2) x) t«0».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 1) x) t«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fderiv ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t -
      fderiv ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t)
    1 =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t]«1»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fderiv ℝ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 0) x) t -
      fderiv ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 2) x) t)
    1 =
  deriv 2 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x - deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 2) x«1».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 0) x) t«1».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 2) x) t«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fderiv ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t -
      fderiv ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t)
    1 =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fderiv ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t -
      fderiv ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t)
    1 =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t
    simp [← Time.deriv_eq]«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ∂ₜ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t - ∂ₜ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t
    rw [time_deriv_comm_space_deriv,«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ deriv 1 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 2) t) x - ∂ₜ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 1) x) t =
  deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 2) x - deriv 2 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x«0».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 2«0».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 2) x) t«0».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 1) x) t«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ deriv 0 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 1) t) x - deriv 1 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t) x =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 0«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 1«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t time_deriv_comm_space_deriv«0»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ deriv 1 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 2) t) x - deriv 2 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 1) t) x =
  deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 2) x - deriv 2 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x«0».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 1«0».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 2«0».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 2) x) t«0».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 1) x) t«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ deriv 0 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 1) t) x - deriv 1 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t) x =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 0«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 1«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t]«1»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ deriv 2 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t) x - deriv 0 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 2) t) x =
  deriv 2 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x - deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 2) x«1».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 2«1».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 0«1».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 2 (fun x => (fₜ t x).ofLp 0) x) t«1».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 2) x) t«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ deriv 0 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 1) t) x - deriv 1 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t) x =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 0«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 1«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t«2»fₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ deriv 0 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 1) t) x - deriv 1 (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t) x =
  deriv 0 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1) x - deriv 1 (fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0) x«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 0«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ ContDiff ℝ 2 ↿fun t x => (fₜ t x).ofLp 1«2».hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 0 (fun x => (fₜ t x).ofLp 1) x) t«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t
    congr«2».e_a.e_ffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 1) t) = fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1«2».e_a.e_ffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t) = fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0 <;>«2».e_a.e_ffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 1) t) = fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 1«2».e_a.e_ffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ (fun x' => ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t) = fun x => (∂ₜ (fun t => fₜ t x) t).ofLp 0
      (funext x'«2».e_a.e_ffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ ∂ₜ (fun t' => (fₜ t' x').ofLp 0) t = (∂ₜ (fun t => fₜ t x') t).ofLp 0
       rw [Time.deriv_euclid«0».e_a.e_ffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ (∂ₜ (fun t => fₜ t x') t).ofLp 2 = (∂ₜ (fun t => fₜ t x') t).ofLp 2«0».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ Differentiable ℝ fun t' => fₜ t' x'«2».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ Differentiable ℝ fun t' => fₜ t' x']«1».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ Differentiable ℝ fun t' => fₜ t' x'«2».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ Differentiable ℝ fun t' => fₜ t' x'«2».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ Differentiable ℝ fun t' => fₜ t' x'
       have h1 := hf.differentiable (byfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Space⊢ 2 ≠ 0«2».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Spaceh1:Differentiable ℝ ↿fₜ⊢ Differentiable ℝ fun t' => fₜ t' x' simpAll goals completed! 🐙«2».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Spaceh1:Differentiable ℝ ↿fₜ⊢ Differentiable ℝ fun t' => fₜ t' x')«2».e_a.e_f.hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜx':Spaceh1:Differentiable ℝ ↿fₜ⊢ Differentiable ℝ fun t' => fₜ t' x'
       fun_propAll goals completed! 🐙)
    repeat' fun_prop«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ DifferentiableAt ℝ (fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x) t
    all_goals
      apply Differentiable.differentiableAt«2».hgfₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜ⊢ Differentiable ℝ fun t => deriv 1 (fun x => (fₜ t x).ofLp 0) x
      fun_propAll goals completed! 🐙
  ·hffₜ:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacehf:ContDiff ℝ 2 ↿fₜi:Fin 3⊢ Differentiable ℝ fun t => curl (fₜ t) x fun_propAll goals completed! 🐙

A.6. Constant of time deriative and space derivatives zero

              

lemma space_fun_of_time_deriv_eq_zero {d} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {f : Time → Space d → M} (hf : Differentiable ℝ ↿f)
    (h : ∀ t x, ∂ₜ (f · x) t = 0) :
    ∃ (g : Space d → M), ∀ t x, f t x = g x := byd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0⊢ ∃ g, ∀ (t : Time) (x : Space d), f t x = g x
  use fun x => f 0 xhd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0⊢ ∀ (t : Time) (x : Space d), f t x = (fun x => f 0 x) x
  intro t xhd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t:Timex:Space d⊢ f t x = (fun x => f 0 x) x
  apply is_const_of_fderiv_eq_zero (f := fun t' => f t' x) (𝕜 := ℝ)h.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t:Timex:Space d⊢ Differentiable ℝ fun t' => f t' xh.hf'd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t:Timex:Space d⊢ ∀ (x_1 : Time), fderiv ℝ (fun t' => f t' x) x_1 = 0
  ·h.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t:Timex:Space d⊢ Differentiable ℝ fun t' => f t' x fun_propAll goals completed! 🐙
  intro th.hf'd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Time⊢ fderiv ℝ (fun t' => f t' x) t = 0
  ext rh.hf'd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ (fderiv ℝ (fun t' => f t' x) t) r = 0 r
  simp only [_root_.zero_apply]h.hf'd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ (fderiv ℝ (fun t' => f t' x) t) r = 0
  trans r.val • (fderiv ℝ (fun t' => f t' x) t) 1d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ (fderiv ℝ (fun t' => f t' x) t) r = r.val • (fderiv ℝ (fun t' => f t' x) t) 1d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ r.val • (fderiv ℝ (fun t' => f t' x) t) 1 = 0
  ·d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ (fderiv ℝ (fun t' => f t' x) t) r = r.val • (fderiv ℝ (fun t' => f t' x) t) 1 rw [← map_smuld:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ (fderiv ℝ (fun t' => f t' x) t) r = (fderiv ℝ (fun t' => f t' x) t) (r.val • 1)d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ (fderiv ℝ (fun t' => f t' x) t) r = (fderiv ℝ (fun t' => f t' x) t) (r.val • 1)]d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ (fderiv ℝ (fun t' => f t' x) t) r = (fderiv ℝ (fun t' => f t' x) t) (r.val • 1)
    congre_6d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ r = r.val • 1
    exte_6d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ r.val = (r.val • 1).val
    simpAll goals completed! 🐙
  rw [← Time.deriv_eq,d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ r.val • ∂ₜ (fun t' => f t' x) t = 0All goals completed! 🐙 h t x,d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ r.val • 0 = 0All goals completed! 🐙 smul_zerod:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0t✝:Timex:Space dt:Timer:Time⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

lemma time_fun_of_space_deriv_eq_zero {d} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {f : Time → Space d → M} (hf : Differentiable ℝ ↿f)
    (h : ∀ t x i, Space.deriv i (f t) x = 0) :
    ∃ (g : Time → M), ∀ t x, f t x = g t := byd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0⊢ ∃ g, ∀ (t : Time) (x : Space d), f t x = g t
  use fun t => f t 0hd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0⊢ ∀ (t : Time) (x : Space d), f t x = (fun t => f t 0) t
  intro t xhd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex:Space d⊢ f t x = (fun t => f t 0) t
  apply is_const_of_fderiv_eq_zero (f := fun x' => f t x') (𝕜 := ℝ)h.hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex:Space d⊢ Differentiable ℝ fun x' => f t x'h.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex:Space d⊢ ∀ (x : Space d), fderiv ℝ (fun x' => f t x') x = 0
  ·h.hfd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex:Space d⊢ Differentiable ℝ fun x' => f t x' fun_propAll goals completed! 🐙
  intro xh.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex✝:Space dx:Space d⊢ fderiv ℝ (fun x' => f t x') x = 0
  apply ContinuousLinearMap.coe_injectiveh.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex✝:Space dx:Space d⊢ ↑(fderiv ℝ (fun x' => f t x') x) = ↑0
  apply (Space.basis (d := d)).toBasis.exth.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex✝:Space dx:Space d⊢ ∀ (i : Fin d), ↑(fderiv ℝ (fun x' => f t x') x) (basis.toBasis i) = ↑0 (basis.toBasis i)
  intro ih.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex✝:Space dx:Space di:Fin d⊢ ↑(fderiv ℝ (fun x' => f t x') x) (basis.toBasis i) = ↑0 (basis.toBasis i)
  simp only [ContinuousLinearMap.toLinearMap_zero, OrthonormalBasis.coe_toBasis,
    ContinuousLinearMap.coe_coe, LinearMap.zero_apply]h.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex✝:Space dx:Space di:Fin d⊢ (fderiv ℝ (fun x' => f t x') x) (basis i) = 0
  rw [← h t x i,h.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex✝:Space dx:Space di:Fin d⊢ (fderiv ℝ (fun x' => f t x') x) (basis i) = deriv i (f t) xAll goals completed! 🐙 Space.deriv_eq_fderiv_basish.hf'd:ℕM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0t:Timex✝:Space dx:Space di:Fin d⊢ (fderiv ℝ (fun x' => f t x') x) (basis i) = (fderiv ℝ (f t) x) (basis i)All goals completed! 🐙]All goals completed! 🐙

lemma const_of_time_deriv_space_deriv_eq_zero {d} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {f : Time → Space d → M} (hf : Differentiable ℝ ↿f)
    (h₁ : ∀ t x, ∂ₜ (f · x) t = 0)
    (h₂ : ∀ t x i, Space.deriv i (f t) x = 0) :
    ∃ (c : M), ∀ t x, f t x = c := byd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0⊢ ∃ c, ∀ (t : Time) (x : Space d), f t x = c
  obtain ⟨g, hg⟩ := space_fun_of_time_deriv_eq_zero hf h₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0g:Space d → Mhg:∀ (t : Time) (x : Space d), f t x = g x⊢ ∃ c, ∀ (t : Time) (x : Space d), f t x = c
  obtain ⟨k, hk⟩ := time_fun_of_space_deriv_eq_zero hf h₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0g:Space d → Mhg:∀ (t : Time) (x : Space d), f t x = g xk:Time → Mhk:∀ (t : Time) (x : Space d), f t x = k t⊢ ∃ c, ∀ (t : Time) (x : Space d), f t x = c
  use g 0hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0g:Space d → Mhg:∀ (t : Time) (x : Space d), f t x = g xk:Time → Mhk:∀ (t : Time) (x : Space d), f t x = k t⊢ ∀ (t : Time) (x : Space d), f t x = g 0
  intro t xhd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0g:Space d → Mhg:∀ (t : Time) (x : Space d), f t x = g xk:Time → Mhk:∀ (t : Time) (x : Space d), f t x = k tt:Timex:Space d⊢ f t x = g 0
  rw [hk t x,hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0g:Space d → Mhg:∀ (t : Time) (x : Space d), f t x = g xk:Time → Mhk:∀ (t : Time) (x : Space d), f t x = k tt:Timex:Space d⊢ k t = g 0All goals completed! 🐙 ← hk t 0,hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0g:Space d → Mhg:∀ (t : Time) (x : Space d), f t x = g xk:Time → Mhk:∀ (t : Time) (x : Space d), f t x = k tt:Timex:Space d⊢ f t 0 = g 0All goals completed! 🐙 hg t 0hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mhf:Differentiable ℝ ↿fh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = 0h₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0g:Space d → Mhg:∀ (t : Time) (x : Space d), f t x = g xk:Time → Mhk:∀ (t : Time) (x : Space d), f t x = k tt:Timex:Space d⊢ g 0 = g 0All goals completed! 🐙]All goals completed! 🐙

A.7. Equal up to a constant of time and space derivatives equal



lemma equal_up_to_const_of_deriv_eq {d} {M} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {f g : Time → Space d → M} (hf : Differentiable ℝ ↿f) (hg : Differentiable ℝ ↿g)
    (h₁ : ∀ t x, ∂ₜ (f · x) t = ∂ₜ (g · x) t)
    (h₂ : ∀ t x i, Space.deriv i (f t) x = Space.deriv i (g t) x) :
    ∃ (c : M), ∀ t x, f t x = g t x + c := byd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c, ∀ (t : Time) (x : Space d), f t x = g t x + c
  suffices h : ∃ c', ∀ t x, f t x - g t x = c' byd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xh:∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'⊢ ∃ c, ∀ (t : Time) (x : Space d), f t x = g t x + cd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'
    obtain ⟨c', hc'⟩ := hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xc':Mhc':∀ (t : Time) (x : Space d), f t x - g t x = c'⊢ ∃ c, ∀ (t : Time) (x : Space d), f t x = g t x + cd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'
    use c'hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xc':Mhc':∀ (t : Time) (x : Space d), f t x - g t x = c'⊢ ∀ (t : Time) (x : Space d), f t x = g t x + c'd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'
    intro t xhd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xc':Mhc':∀ (t : Time) (x : Space d), f t x - g t x = c't:Timex:Space d⊢ f t x = g t x + c'd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'
    rw [← hc' t xhd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xc':Mhc':∀ (t : Time) (x : Space d), f t x - g t x = c't:Timex:Space d⊢ f t x = g t x + (f t x - g t x)hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xc':Mhc':∀ (t : Time) (x : Space d), f t x - g t x = c't:Timex:Space d⊢ f t x = g t x + (f t x - g t x)d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c']hd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xc':Mhc':∀ (t : Time) (x : Space d), f t x - g t x = c't:Timex:Space d⊢ f t x = g t x + (f t x - g t x)d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'
    simpd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∃ c', ∀ (t : Time) (x : Space d), f t x - g t x = c'
  apply const_of_time_deriv_space_deriv_eq_zerohfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ Differentiable ℝ ↿fun t x => f t x - g t xh₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x - g x_1 x) t = 0h₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∀ (t : Time) (x : Space d) (i : Fin d), deriv i (fun x => f t x - g t x) x = 0
  ·hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ Differentiable ℝ ↿fun t x => f t x - g t x exact Differentiable.fun_sub hf hgAll goals completed! 🐙
  ·h₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x - g x_1 x) t = 0 intro t xh₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ ∂ₜ (fun x_1 => f x_1 x - g x_1 x) t = 0
    rw [Time.deriv_eq,h₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ (fderiv ℝ (fun x_1 => f x_1 x - g x_1 x) t) 1 = 0h₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ (fderiv ℝ (fun x_1 => f x_1 x) t - fderiv ℝ (fun x_1 => g x_1 x) t) 1 = 0h₁.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => f x_1 x) th₁.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => g x_1 x) t fderiv_fun_subh₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ (fderiv ℝ (fun x_1 => f x_1 x) t - fderiv ℝ (fun x_1 => g x_1 x) t) 1 = 0h₁.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => f x_1 x) th₁.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => g x_1 x) th₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ (fderiv ℝ (fun x_1 => f x_1 x) t - fderiv ℝ (fun x_1 => g x_1 x) t) 1 = 0h₁.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => f x_1 x) th₁.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => g x_1 x) t]h₁d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ (fderiv ℝ (fun x_1 => f x_1 x) t - fderiv ℝ (fun x_1 => g x_1 x) t) 1 = 0h₁.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => f x_1 x) th₁.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => g x_1 x) t
    simp [← Time.deriv_eq, h₁]h₁.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => f x_1 x) th₁.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space d⊢ DifferentiableAt ℝ (fun x_1 => g x_1 x) t
    all_goals fun_propAll goals completed! 🐙
  ·h₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x⊢ ∀ (t : Time) (x : Space d) (i : Fin d), deriv i (fun x => f t x - g t x) x = 0 intro t x ih₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ deriv i (fun x => f t x - g t x) x = 0
    rw [Space.deriv_eq_fderiv_basis,h₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ (fderiv ℝ (fun x => f t x - g t x) x) (basis i) = 0h₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ (fderiv ℝ (f t) x - fderiv ℝ (g t) x) (basis i) = 0h₂.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (f t) xh₂.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (g t) x fderiv_fun_subh₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ (fderiv ℝ (f t) x - fderiv ℝ (g t) x) (basis i) = 0h₂.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (f t) xh₂.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (g t) xh₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ (fderiv ℝ (f t) x - fderiv ℝ (g t) x) (basis i) = 0h₂.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (f t) xh₂.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (g t) x]h₂d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ (fderiv ℝ (f t) x - fderiv ℝ (g t) x) (basis i) = 0h₂.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (f t) xh₂.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (g t) x
    simp [← Space.deriv_eq_fderiv_basis, h₂]h₂.hfd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (f t) xh₂.hgd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:Time → Space d → Mg:Time → Space d → Mhf:Differentiable ℝ ↿fhg:Differentiable ℝ ↿gh₁:∀ (t : Time) (x : Space d), ∂ₜ (fun x_1 => f x_1 x) t = ∂ₜ (fun x_1 => g x_1 x) th₂:∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) xt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (g t) x
    all_goals fun_propAll goals completed! 🐙

B. Derivatives of distributions on Time × Space d

B.1. Time derivatives

              lemma distTimeDeriv_apply {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : (Time × Space d) →d[ℝ] M) (ε : 𝓢(Time × Space d, ℝ)) :
    (distTimeDeriv f) ε = fderivD ℝ f ε (1, 0) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ (distTimeDeriv f) ε = (((fderivD ℝ) f) ε) (1, 0)
  simp [distTimeDeriv]All goals completed! 🐙

lemma distTimeDeriv_apply' {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : (Time × Space d) →d[ℝ] M) (ε : 𝓢(Time × Space d, ℝ)) :
    (distTimeDeriv f) ε =
    -f (SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)
    ((fderivCLM ℝ (Time × Space d) ℝ) ε)) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ (distTimeDeriv f) ε = -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) ε))
  rw [distTimeDeriv_apply,M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ (((fderivD ℝ) f) ε) (1, 0) = -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) ε))All goals completed! 🐙 fderivD_applyM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) ε)) =
  -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) ε))All goals completed! 🐙]All goals completed! 🐙lemma apply_fderiv_eq_distTimeDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f : (Time × Space d) →d[ℝ] M) (ε : 𝓢(Time × Space d, ℝ)) :
    f (SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0) ((fderivCLM ℝ (Time × Space d) ℝ) ε)) =
    - (distTimeDeriv f) ε := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mf:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) ε)) = -(distTimeDeriv f) ε
  simp [distTimeDeriv_apply']All goals completed! 🐙

B.1.1. Composition with a CLM

lemma distTimeDeriv_apply_CLM {M M2 d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    [NormedAddCommGroup M2] [NormedSpace ℝ M2] (f : (Time × Space d) →d[ℝ] M)
    (c : M →L[ℝ] M2) : distTimeDeriv (c ∘L f) = c ∘L (distTimeDeriv f) := byM:TypeM2:Typed:ℕinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:NormedAddCommGroup M2inst✝:NormedSpace ℝ M2f:(Time × Space d)→d[ℝ] Mc:M →L[ℝ] M2⊢ distTimeDeriv (c ∘SL f) = c ∘SL distTimeDeriv f
  ext εM:TypeM2:Typed:ℕinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:NormedAddCommGroup M2inst✝:NormedSpace ℝ M2f:(Time × Space d)→d[ℝ] Mc:M →L[ℝ] M2ε:𝓢(Time × Space d, ℝ)⊢ (distTimeDeriv (c ∘SL f)) ε = (c ∘SL distTimeDeriv f) ε
  simp [distTimeDeriv_apply, fderivD_apply]All goals completed! 🐙

B.2. Space derivatives

              lemma distSpaceDeriv_apply {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (i : Fin d) (f : (Time × Space d) →d[ℝ] M) (ε : 𝓢(Time × Space d, ℝ)) :
    (distSpaceDeriv i f) ε = fderivD ℝ f ε (0, basis i) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ ((distSpaceDeriv i) f) ε = (((fderivD ℝ) f) ε) (0, basis i)
  simp [distSpaceDeriv]All goals completed! 🐙

lemma distSpaceDeriv_apply' {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (i : Fin d) (f : (Time × Space d) →d[ℝ] M) (ε : 𝓢(Time × Space d, ℝ)) :
    (distSpaceDeriv i f) ε =
    - f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
    ((fderivCLM ℝ (Time × Space d) ℝ) ε)) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ ((distSpaceDeriv i) f) ε =
  -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) ε))
  rw [distSpaceDeriv_apply,M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ (((fderivD ℝ) f) ε) (0, basis i) =
  -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) ε))All goals completed! 🐙 fderivD_applyM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) ε)) =
  -f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) ε))All goals completed! 🐙]All goals completed! 🐙lemma apply_fderiv_eq_distSpaceDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (i : Fin d) (f : (Time × Space d) →d[ℝ] M) (ε : 𝓢(Time × Space d, ℝ)) :
    f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
    ((fderivCLM ℝ (Time × Space d) ℝ) ε)) =
    - (distSpaceDeriv i f) ε := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mε:𝓢(Time × Space d, ℝ)⊢ f ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) ε)) =
  -((distSpaceDeriv i) f) ε
  simp [distSpaceDeriv_apply']All goals completed! 🐙

B.2.1. Space derivatives commute



lemma distSpaceDeriv_commute {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (i j : Fin d) (f : (Time × Space d) →d[ℝ] M) :
    distSpaceDeriv i (distSpaceDeriv j f) = distSpaceDeriv j (distSpaceDeriv i f) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] M⊢ (distSpaceDeriv i) ((distSpaceDeriv j) f) = (distSpaceDeriv j) ((distSpaceDeriv i) f)
  ext κM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)⊢ ((distSpaceDeriv i) ((distSpaceDeriv j) f)) κ = ((distSpaceDeriv j) ((distSpaceDeriv i) f)) κ
  simp only [distSpaceDeriv_apply, fderivD_apply, neg_neg]M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)⊢ f
    ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis j))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) κ)))) =
  f
    ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis j)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))))
  congr 1e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)⊢ (SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis j))
    ((fderivCLM ℝ (Time × Space d) ℝ)
      ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))) =
  (SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
    ((fderivCLM ℝ (Time × Space d) ℝ)
      ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis j)) ((fderivCLM ℝ (Time × Space d) ℝ) κ)))
  ext xe_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space d⊢ ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis j))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))))
    x =
  ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis j)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))))
    x
  change fderiv ℝ (fun x => fderiv ℝ κ x (0, basis i)) x (0, basis j) =
    fderiv ℝ (fun x => fderiv ℝ κ x (0, basis j)) x (0, basis i)e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space d⊢ (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis i)) x) (0, basis j) =
  (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis j)) x) (0, basis i)
  have h1 := smooth κ 2e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis i)) x) (0, basis j) =
  (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis j)) x) (0, basis i)
  rw [fderiv_clm_apply,e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (0, basis j) =
  (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis j)) x) (0, basis i)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) xe_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (0, basis j) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis j)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis j)) (0, basis i)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis j)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) x fderiv_clm_applye_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (0, basis j) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis j)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis j)) (0, basis i)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis j)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) xe_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (0, basis j) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis j)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis j)) (0, basis i)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis j)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) x]e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (0, basis j) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis j)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis j)) (0, basis i)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis j)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) x
  ·e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (0, basis j) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis j)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis j)) (0, basis i) simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,
      ContinuousLinearMap.flip_apply]e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ ((fderiv ℝ (fderiv ℝ ⇑κ) x) (0, basis j)) (0, basis i) = ((fderiv ℝ (fderiv ℝ ⇑κ) x) (0, basis i)) (0, basis j)
    exact (h1.contDiffAt.isSymmSndFDerivAt (byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin dj:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ minSmoothness ℝ 2 ≤ ↑2 simpAll goals completed! 🐙)).eq (0, basis j) (0, basis i)
  all_goals fun_propAll goals completed! 🐙

B.2.2. Composition with a CLM

lemma distSpaceDeriv_apply_CLM {M M2 d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    [NormedAddCommGroup M2] [NormedSpace ℝ M2]
    (i : Fin d) (f : (Time × Space d) →d[ℝ] M)
    (c : M →L[ℝ] M2) : distSpaceDeriv i (c ∘L f) = c ∘L (distSpaceDeriv i f) := byM:TypeM2:Typed:ℕinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:NormedAddCommGroup M2inst✝:NormedSpace ℝ M2i:Fin df:(Time × Space d)→d[ℝ] Mc:M →L[ℝ] M2⊢ (distSpaceDeriv i) (c ∘SL f) = c ∘SL (distSpaceDeriv i) f
  ext εM:TypeM2:Typed:ℕinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:NormedAddCommGroup M2inst✝:NormedSpace ℝ M2i:Fin df:(Time × Space d)→d[ℝ] Mc:M →L[ℝ] M2ε:𝓢(Time × Space d, ℝ)⊢ ((distSpaceDeriv i) (c ∘SL f)) ε = (c ∘SL (distSpaceDeriv i) f) ε
  simp [distSpaceDeriv_apply, fderivD_apply]All goals completed! 🐙

B.3. Time and space derivatives commute



lemma distTimeDeriv_commute_distSpaceDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (i : Fin d) (f : (Time × Space d) →d[ℝ] M) :
    distTimeDeriv (distSpaceDeriv i f) = distSpaceDeriv i (distTimeDeriv f) := byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] M⊢ distTimeDeriv ((distSpaceDeriv i) f) = (distSpaceDeriv i) (distTimeDeriv f)
  ext κM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)⊢ (distTimeDeriv ((distSpaceDeriv i) f)) κ = ((distSpaceDeriv i) (distTimeDeriv f)) κ
  simp only [distTimeDeriv_apply, distSpaceDeriv_apply, fderivD_apply, neg_neg]M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)⊢ f
    ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) κ)))) =
  f
    ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))))
  congr 1e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)⊢ (SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
    ((fderivCLM ℝ (Time × Space d) ℝ)
      ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))) =
  (SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0))
    ((fderivCLM ℝ (Time × Space d) ℝ)
      ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) κ)))
  ext xe_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space d⊢ ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))))
    x =
  ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (1, 0))
      ((fderivCLM ℝ (Time × Space d) ℝ)
        ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, basis i)) ((fderivCLM ℝ (Time × Space d) ℝ) κ))))
    x
  change fderiv ℝ (fun x => fderiv ℝ κ x (1, 0)) x (0, basis i) =
    fderiv ℝ (fun x => fderiv ℝ κ x (0, basis i)) x (1, 0)e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space d⊢ (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (1, 0)) x) (0, basis i) =
  (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis i)) x) (1, 0)
  have h1 := smooth κ 2e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (1, 0)) x) (0, basis i) =
  (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis i)) x) (1, 0)
  rw [fderiv_clm_apply,e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (1, 0)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (1, 0)) (0, basis i) =
  (fderiv ℝ (fun x => (fderiv ℝ (⇑κ) x) (0, basis i)) x) (1, 0)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (1, 0)) xe_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (1, 0)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (1, 0)) (0, basis i) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (1, 0)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (1, 0)) x fderiv_clm_applye_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (1, 0)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (1, 0)) (0, basis i) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (1, 0)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (1, 0)) xe_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (1, 0)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (1, 0)) (0, basis i) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (1, 0)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (1, 0)) x]e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (1, 0)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (1, 0)) (0, basis i) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (1, 0)e_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (0, basis i)) xe_6.hcM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fderiv ℝ ⇑κ) xe_6.huM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ DifferentiableAt ℝ (fun x => (1, 0)) x
  ·e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (1, 0)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (1, 0)) (0, basis i) =
  (fderiv ℝ (⇑κ) x ∘SL fderiv ℝ (fun x => (0, basis i)) x + (fderiv ℝ (fderiv ℝ ⇑κ) x).flip (0, basis i)) (1, 0) simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,
      ContinuousLinearMap.flip_apply]e_6M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ ((fderiv ℝ (fderiv ℝ ⇑κ) x) (0, basis i)) (1, 0) = ((fderiv ℝ (fderiv ℝ ⇑κ) x) (1, 0)) (0, basis i)
    exact (h1.contDiffAt.isSymmSndFDerivAt (byM:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mi:Fin df:(Time × Space d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:Time × Space dh1:ContDiff ℝ ↑2 ⇑κ⊢ minSmoothness ℝ 2 ≤ ↑2 simpAll goals completed! 🐙)).eq (0, basis i) (1, 0)
  all_goals fun_propAll goals completed! 🐙

B.4. The spatial gradient

lemma distSpaceGrad_apply {d} (f : (Time × Space d) →d[ℝ] ℝ) (ε : 𝓢(Time × Space d, ℝ)) :
    distSpaceGrad f ε = fun i => distSpaceDeriv i f ε := byd:ℕf:(Time × Space d)→d[ℝ] ℝε:𝓢(Time × Space d, ℝ)⊢ ((distSpaceGrad f) ε).ofLp = fun i => ((distSpaceDeriv i) f) ε
  rflAll goals completed! 🐙

B.5. The spatial divergence

lemma distSpaceDiv_apply_eq_sum_distSpaceDeriv {d}
    (f : (Time × Space d) →d[ℝ] EuclideanSpace ℝ (Fin d)) (η : 𝓢(Time ×Space d, ℝ)) :
    distSpaceDiv f η = ∑ i, distSpaceDeriv i f η i := byd:ℕf:(Time × Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Time × Space d, ℝ)⊢ (distSpaceDiv f) η = ∑ i, (((distSpaceDeriv i) f) η).ofLp i rflAll goals completed! 🐙

Functions and distributions on Time and Space d

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The coordinate product and derivatives involving time and space

A.1. The TimeAndSpace coordinate product

A.2. Space and time derivatives in terms of curried functions

A.3. Commuting time and space derivatives

A.4. Differentiablity conditions

A.5. Time derivative commute with curl

A.6. Constant of time deriative and space derivatives zero

A.7. Equal up to a constant of time and space derivatives equal

B. Derivatives of distributions on Time × Space d

B.1. Time derivatives

B.1.1. Composition with a CLM

B.2. Space derivatives

B.2.1. Space derivatives commute

B.2.2. Composition with a CLM

B.3. Time and space derivatives commute

B.4. The spatial gradient

B.5. The spatial divergence

B.6. The spatial curl

A.1. The `TimeAndSpace` coordinate product