Exterior derivative of a differential form on a normed space

In this file we define the exterior derivative of a differential form on a normed space. Under certain smoothness assumptions, we prove that this operation is linear in the form and the second exterior derivative of a form is zero.

We represent a differential n-form on E taking values in F as E → E [⋀^Fin n]→L[𝕜] F.

Implementation notes

There are a few competing definitions of the exterior derivative of a differential form that differ from each other by a normalization factor. We use the following one:

$$ dω(x; v_0, \dots, v_n) = \sum_{i=0}^n (-1)^i D_x ω(x; v_0, \dots, \widehat{v_i}, \dots, v_n) · v_i $$

where $$\widehat{v_i}$$ means that we omit this element of the tuple, see extDeriv_apply.

TODO

• Introduce notation for:
  • an unbundled n-form on a normed space;
  • a bundled C^r-smooth n-form on a normed space;
  • same for manifolds (not defined yet).
• Introduce bundled C^r-smooth n-forms on normed spaces and manifolds.
  • Discuss the future API and the use cases that need to be covered on Zulip.
  • Introduce new types & notation, copy the API.
• Add shorter and more readable definitions (or abbreviations?) for 0-forms (constOfIsEmpty) and 1-forms (ofSubsingleton), sync with the API for ContinuousMultilinearMap.

noncomputable def extDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (ω : E → E [⋀^Fin n]→L[𝕜] F) (x : E) : E [⋀^Fin (n + 1)]→L[𝕜] F

Exterior derivative of a differential form.

There are a few competing definitions of the exterior derivative of a differential form that differ from each other by a normalization factor. We use the following one:

$$ dω(x; v_0, \dots, v_n) = \sum_{i=0}^n (-1)^i D_x ω(x; v_0, \dots, \widehat{v_i}, \dots, v_n) · v_i $$

where $$\widehat{v_i}$$ means that we omit this element of the tuple, see extDeriv_apply.

Equations

• extDeriv ω x = ContinuousAlternatingMap.alternatizeUncurryFin (fderiv 𝕜 ω x)

noncomputable def extDerivWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (ω : E → E [⋀^Fin n]→L[𝕜] F) (s : Set E) (x : E) : E [⋀^Fin (n + 1)]→L[𝕜] F

Exterior derivative of a differential form within a set.

There are a few competing definitions of the exterior derivative of a differential form that differ from each other by a normalization factor. We use the following one:

$$ dω(x; v_0, \dots, v_n) = \sum_{i=0}^n (-1)^i D_x ω(x; v_0, \dots, \widehat{v_i}, \dots, v_n) · v_i $$

where $$\widehat{v_i}$$ means that we omit this element of the tuple, see extDerivWithin_apply.

Equations

• extDerivWithin ω s x = ContinuousAlternatingMap.alternatizeUncurryFin (fderivWithin 𝕜 ω s x)

@[simp]

theorem extDerivWithin_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (ω : E → E [⋀^Fin n]→L[𝕜] F) : extDerivWithin ω Set.univ = extDeriv ω

theorem extDerivWithin_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hsx : UniqueDiffWithinAt 𝕜 s x) (hω₁ : DifferentiableWithinAt 𝕜 ω₁ s x) (hω₂ : DifferentiableWithinAt 𝕜 ω₂ s x) : extDerivWithin (ω₁ + ω₂) s x = extDerivWithin ω₁ s x + extDerivWithin ω₂ s x

theorem extDerivWithin_fun_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hsx : UniqueDiffWithinAt 𝕜 s x) (hω₁ : DifferentiableWithinAt 𝕜 ω₁ s x) (hω₂ : DifferentiableWithinAt 𝕜 ω₂ s x) : extDerivWithin (fun (x : E) => ω₁ x + ω₂ x) s x = extDerivWithin ω₁ s x + extDerivWithin ω₂ s x

theorem extDeriv_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E} (hω₁ : DifferentiableAt 𝕜 ω₁ x) (hω₂ : DifferentiableAt 𝕜 ω₂ x) : extDeriv (ω₁ + ω₂) x = extDeriv ω₁ x + extDeriv ω₂ x

theorem extDeriv_fun_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E} (hω₁ : DifferentiableAt 𝕜 ω₁ x) (hω₂ : DifferentiableAt 𝕜 ω₂ x) : extDeriv (fun (x : E) => ω₁ x + ω₂ x) x = extDeriv ω₁ x + extDeriv ω₂ x

theorem extDerivWithin_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set E} {x : E} (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F) (hsx : UniqueDiffWithinAt 𝕜 s x) : extDerivWithin (c • ω) s x = c • extDerivWithin ω s x

theorem extDerivWithin_fun_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set E} {x : E} (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F) (hsx : UniqueDiffWithinAt 𝕜 s x) : extDerivWithin (fun (x : E) => c • ω x) s x = c • extDerivWithin ω s x

theorem extDeriv_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : E} (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F) : extDeriv (c • ω) x = c • extDeriv ω x

theorem extDeriv_fun_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : E} (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F) : extDeriv (c • ω) x = c • extDeriv ω x

theorem extDerivWithin_constOfIsEmpty {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} (f : E → F) (hs : UniqueDiffWithinAt 𝕜 s x) : extDerivWithin (fun (x : E) => ContinuousAlternatingMap.constOfIsEmpty 𝕜 E (Fin 0) (f x)) s x = (ContinuousAlternatingMap.ofSubsingleton 𝕜 E F 0) (fderivWithin 𝕜 f s x)

The exterior derivative of a 0-form given by a function f within a set is the 1-form given by the derivative of f within the set.

theorem extDeriv_constOfIsEmpty {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : extDeriv (fun (x : E) => ContinuousAlternatingMap.constOfIsEmpty 𝕜 E (Fin 0) (f x)) x = (ContinuousAlternatingMap.ofSubsingleton 𝕜 E F 0) (fderiv 𝕜 f x)

The exterior derivative of a 0-form given by a function f is the 1-form given by the derivative of f.

theorem Filter.EventuallyEq.extDerivWithin_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hs : ω₁ =ᶠ[nhdsWithin x s] ω₂) (hx : ω₁ x = ω₂ x) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

theorem Filter.EventuallyEq.extDerivWithin_eq_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hs : ω₁ =ᶠ[nhdsWithin x s] ω₂) (hx : x ∈ s) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

theorem Filter.EventuallyEq.extDerivWithin_eq_of_insert {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hs : ω₁ =ᶠ[nhdsWithin x (insert x s)] ω₂) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

theorem Filter.EventuallyEq.extDerivWithin' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s t : Set E} {x : E} (hs : ω₁ =ᶠ[nhdsWithin x s] ω₂) (ht : t ⊆ s) : extDerivWithin ω₁ t =ᶠ[nhdsWithin x s] extDerivWithin ω₂ t

theorem Filter.EventuallyEq.extDerivWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hs : ω₁ =ᶠ[nhdsWithin x s] ω₂) : extDerivWithin ω₁ s =ᶠ[nhdsWithin x s] extDerivWithin ω₂ s

theorem Filter.EventuallyEq.extDerivWithin_eq_nhds {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (h : ω₁ =ᶠ[nhds x] ω₂) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

theorem extDerivWithin_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hs : Set.EqOn ω₁ ω₂ s) (hx : ω₁ x = ω₂ x) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

theorem extDerivWithin_congr' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hs : Set.EqOn ω₁ ω₂ s) (hx : x ∈ s) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x

theorem Filter.EventuallyEq.extDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E} (h : ω₁ =ᶠ[nhds x] ω₂) : extDeriv ω₁ =ᶠ[nhds x] extDeriv ω₂

theorem Filter.EventuallyEq.extDeriv_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E} (h : ω₁ =ᶠ[nhds x] ω₂) : extDeriv ω₁ x = extDeriv ω₂ x

theorem extDerivWithin_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (h : DifferentiableWithinAt 𝕜 ω s x) (hs : UniqueDiffWithinAt 𝕜 s x) (v : Fin (n + 1) → E) : (extDerivWithin ω s x) v = ∑ i : Fin (n + 1), (-1) ^ ↑i • (fderivWithin 𝕜 (fun (x : E) => (ω x) (i.removeNth v)) s x) (v i)

theorem extDeriv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ω : E → E [⋀^Fin n]→L[𝕜] F} {x : E} (h : DifferentiableAt 𝕜 ω x) (v : Fin (n + 1) → E) : (extDeriv ω x) v = ∑ i : Fin (n + 1), (-1) ^ ↑i • (fderiv 𝕜 (fun (x : E) => (ω x) (i.removeNth v)) x) (v i)

theorem extDerivWithin_extDerivWithin_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞} {ω : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E} (hω : ContDiffWithinAt 𝕜 r ω s x) (hr : minSmoothness 𝕜 2 ≤ r) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ closure (interior s)) (h'x : x ∈ s) : extDerivWithin (extDerivWithin ω s) s x = 0

The second exterior derivative of a sufficiently smooth differential form is zero.

theorem extDerivWithin_extDerivWithin_eqOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞} {ω : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} (hω : ContDiffOn 𝕜 r ω s) (hr : minSmoothness 𝕜 2 ≤ r) (hs : UniqueDiffOn 𝕜 s) : Set.EqOn (extDerivWithin (extDerivWithin ω s) s) 0 (s ∩ closure (interior s))

The second exterior derivative of a sufficiently smooth differential form is zero.

theorem extDeriv_extDeriv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞} {ω : E → E [⋀^Fin n]→L[𝕜] F} {x : E} (hω : ContDiffAt 𝕜 r ω x) (hr : minSmoothness 𝕜 2 ≤ r) : extDeriv (extDeriv ω) x = 0

The second exterior derivative of a sufficiently smooth differential form is zero.

theorem extDeriv_extDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞} {ω : E → E [⋀^Fin n]→L[𝕜] F} (h : ContDiff 𝕜 r ω) (hr : minSmoothness 𝕜 2 ≤ r) : extDeriv (extDeriv ω) = 0

The second exterior derivative of a sufficiently smooth differential form is zero.