VectorIdentities

In this file we define common vector calculus identities based on Space.

General auxiliary lemmas

theorem fderiv_pi' {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] {X : Type u_4} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {ι : Type u_1} [Fintype ι] {Y' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (Y' i)] [(i : ι) → NormedSpace 𝕜 (Y' i)] {Φ : X → (i : ι) → Y' i} {x : X} (h : DifferentiableAt 𝕜 Φ x) : fderiv 𝕜 Φ x = ContinuousLinearMap.pi fun (i : ι) => fderiv 𝕜 (fun (x : X) => Φ x i) x

theorem ContDiff.differentiable_fderiv {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] {X : Type u_4} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {Y : Type u_5} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (f : X → Y) (hf : ContDiff 𝕜 2 f) : Differentiable 𝕜 fun (x : X) => fderiv 𝕜 f x

theorem fderiv_coord_eq_proj_comp {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] {X : Type u_4} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {ι : Type u_1} [Fintype ι] {Y' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (Y' i)] [(i : ι) → NormedSpace 𝕜 (Y' i)] {Φ : X → (i : ι) → Y' i} {x : X} {i : ι} (h : DifferentiableAt 𝕜 Φ x) : fderiv 𝕜 (fun (x : X) => Φ x i) x = (ContinuousLinearMap.proj i).comp (fderiv 𝕜 Φ x)

Space.deriv lemmas

theorem Space.deriv_add {M : Type u_1} {d : ℕ} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f1 f2 : Space d → M) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : deriv u (f1 + f2) = deriv u f1 + deriv u f2

Derivatives on space distiribute over addition.

theorem Space.deriv_coord_add {d : ℕ} {u i : Fin d} (f1 f2 : Space d → EuclideanSpace ℝ (Fin d)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : (deriv u fun (x : Space d) => f1 x i + f2 x i) = (deriv u fun (x : Space d) => f1 x i) + deriv u fun (x : Space d) => f2 x i

Derivatives on space distiribute coordinate-wise over addition.

theorem Space.deriv_smul {M : Type u_1} {d : ℕ} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Space d → M) (k : ℝ) (hf : Differentiable ℝ f) : deriv u (k • f) = k • deriv u f

Scalar multiplication on space derivatives.

theorem Space.deriv_coord_smul {d : ℕ} {u i : Fin d} {x : Space d} (f : Space d → EuclideanSpace ℝ (Fin d)) (k : ℝ) (hf : Differentiable ℝ f) : deriv u (fun (x : Space d) => k * f x i) x = (k • deriv u fun (x : Space d) => f x i) x

Coordinate-wise scalar multiplication on space derivatives.

theorem Space.deriv_commute {M : Type u_1} {d : ℕ} {u v : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Space d → M) (hf : ContDiff ℝ 2 f) : deriv u (deriv v f) = deriv v (deriv u f)

Derivatives on space commute with one another.

theorem Space.differentiable_fderiv_coord {i : Fin 3} (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : Differentiable ℝ (fderiv ℝ fun (x : Space) => f x i)

Coordiate functions of fderiv is differentiable.

theorem Space.deriv_coord_2nd_add {i u v w : Fin 3} (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : (deriv i fun (x : Space) => deriv u (fun (x : Space) => f x u) x + (deriv v (fun (x : Space) => f x v) x + deriv w (fun (x : Space) => f x w) x)) = deriv i (deriv u fun (x : Space) => f x u) + deriv i (deriv v fun (x : Space) => f x v) + deriv i (deriv w fun (x : Space) => f x w)

Second derivatives distiribute coordinate-wise over addition (all three components for div).

theorem Space.deriv_coord_2nd_sub {u v w : Fin 3} (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : (deriv u fun (x : Space) => deriv v (fun (x : Space) => f x w) x - deriv w (fun (x : Space) => f x v) x) = deriv u (deriv v fun (x : Space) => f x w) - deriv u (deriv w fun (x : Space) => f x v)

Second derivatives distiribute coordinate-wise over subtraction (two components for curl).

Vector calculus identities

theorem Space.laplacian_eq_div_of_grad (f : Space → ℝ) : laplacian f = div (grad f)

theorem Space.div_of_curl_eq_zero (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : div (curl f) = 0

theorem Space.curl_of_curl (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : curl (curl f) = grad (div f) - laplacian_vec f

@[simp]

theorem Space.grad_zero {d : ℕ} : grad 0 = 0

@[simp]

theorem Space.div_zero {d : ℕ} : div 0 = 0

@[simp]

theorem Space.curl_zero : curl 0 = 0

@[simp]

theorem Space.grad_const {d : ℕ} (c : ℝ) : (grad fun (x : Space d) => c) = 0

@[simp]

theorem Space.div_const {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) : (div fun (x : Space d) => v) = 0

@[simp]

theorem Space.curl_const (v₃ : EuclideanSpace ℝ (Fin 3)) : (curl fun (x : Space) => v₃) = 0

Addition of ∇ operations

theorem Space.grad_add {d : ℕ} (f1 f2 : Space d → ℝ) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : grad (f1 + f2) = grad f1 + grad f2

theorem Space.div_add (f1 f2 : Space → EuclideanSpace ℝ (Fin 3)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : div (f1 + f2) = div f1 + div f2

theorem Space.curl_add (f1 f2 : Space → EuclideanSpace ℝ (Fin 3)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : curl (f1 + f2) = curl f1 + curl f2

Scalar multiplication of ∇ operations

theorem Space.grad_smul {d : ℕ} (f : Space d → ℝ) (k : ℝ) (hf : Differentiable ℝ f) : grad (k • f) = k • grad f

theorem Space.div_smul (f : Space → EuclideanSpace ℝ (Fin 3)) (k : ℝ) (hf : Differentiable ℝ f) : div (k • f) = k • div f

theorem Space.curl_smul (f : Space → EuclideanSpace ℝ (Fin 3)) (k : ℝ) (hf : Differentiable ℝ f) : curl (k • f) = k • curl f

Linearity of div and curl

theorem Space.div_linear_map {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : W → Space → EuclideanSpace ℝ (Fin 3)) (hf : ∀ (w : W), Differentiable ℝ (f w)) (hf' : IsLinearMap ℝ f) : IsLinearMap ℝ fun (w : W) => div (f w)

theorem Space.curl_linear_map {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : W → Space → EuclideanSpace ℝ (Fin 3)) (hf : ∀ (w : W), Differentiable ℝ (f w)) (hf' : IsLinearMap ℝ f) : IsLinearMap ℝ fun (w : W) => curl (f w)