Classical vector calculus properties

Vector calculus properties under classical space and time derivatives.

theorem ClassicalMechanics.dt_distrib {u : Fin 3} {x dx1 : Space} {t : Time} {v : Fin 3} {dx2 : Space} (f : Time → Space → EuclideanSpace ℝ (Fin 3)) : (fderiv ℝ (fun (t : Time) => (fderiv ℝ (fun (x : Space) => f t x u) x) dx1) t - fderiv ℝ (fun (t : Time) => (fderiv ℝ (fun (x : Space) => f t x v) x) dx2) t) 1 = (fderiv ℝ (fun (t : Time) => (fderiv ℝ (fun (x : Space) => f t x u) x) dx1) t) 1 - (fderiv ℝ (fun (t : Time) => (fderiv ℝ (fun (x : Space) => f t x v) x) dx2) t) 1

theorem ClassicalMechanics.fderiv_coord_dt {i : Fin 3} (f : Time → Space → EuclideanSpace ℝ (Fin 3)) (t dt : Time) (hf : Differentiable ℝ ↿f) : (fun (x : Space) => (fderiv ℝ (fun (t : Time) => f t x i) t) dt) = fun (x : Space) => (fderiv ℝ (fun (t : Time) => f t x) t) dt i

theorem ClassicalMechanics.fderiv_swap_time_space_coord {i : Fin 3} (f : Time → Space → EuclideanSpace ℝ (Fin 3)) (t dt : Time) (x dx : Space) (hf : ContDiff ℝ 2 ↿f) : (fderiv ℝ (fun (t' : Time) => (fderiv ℝ (fun (x' : Space) => f t' x' i) x) dx) t) dt = (fderiv ℝ (fun (x' : Space) => (fderiv ℝ (fun (t' : Time) => f t' x' i) t) dt) x) dx

Derivatives along space coordinates and time commute.

theorem ClassicalMechanics.differentiableAt_fderiv_coord_single {u : Fin 3} {x : Space} {v : Fin 3} {t : Time} (ft : Time → Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 ↿ft) : DifferentiableAt ℝ (fun (t : Time) => (fderiv ℝ (fun (x : Space) => ft t x u) x) (EuclideanSpace.single v 1)) t

theorem ClassicalMechanics.time_deriv_curl_commute (fₜ : Time → Space → EuclideanSpace ℝ (Fin 3)) (t : Time) (x : Space) (hf : ContDiff ℝ 2 ↿fₜ) : Time.deriv (fun (t : Time) => Space.curl (fₜ t) x) t = Space.curl (fun (x : Space) => Time.deriv (fun (t : Time) => fₜ t x) t) x

Curl and time derivative commute.

def ClassicalMechanics.«term_⨯ₑ₃_» : Lean.TrailingParserDescr

Cross product in EuclideanSpace ℝ (Fin 3). Uses ⨯ which is typed using \X or \vectorproduct or \crossproduct.

Equations

• One or more equations did not get rendered due to their size.

theorem ClassicalMechanics.fderiv_cross_commute {u : ℝ} {s : Space} {f : ℝ → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) : (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s ((fderiv ℝ (fun (u : ℝ) => f u) u) 1) = (fderiv ℝ (fun (u : ℝ) => (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s (f u)) u) 1

Cross product and fderiv commute.

theorem ClassicalMechanics.time_deriv_cross_commute {t : Time} {s : Space} {f : Time → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) : (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s (Time.deriv (fun (t : Time) => f t) t) = Time.deriv (fun (t : Time) => (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s (f t)) t

Cross product and time derivative commute.

theorem ClassicalMechanics.inner_cross_self (v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ v ((fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) w v) = 0

theorem ClassicalMechanics.inner_self_cross (v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ v ((fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) v w) = 0