Evaluation of the derivative of differential forms on vector fields

In this file we prove the following formula and its corollaries. If ω is a differentiable k-form and V i are k + 1 differentiable vector fields, then

$$ dω(V_0(x), \dots, V_n(x)) = \left(\sum_{i=0}^k (-1)^i • D_x(ω(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_k(x)))(V_i(x)) + \sum_{0 \le i < j\le k} (-1)^{i + j} ω(x; [V_i, V_j](x), V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_j(x)}, …, V_k(x)), $$ where $$[V_i, V_j]$$ is the commutator of the vector fields $$V_i$$ and $$V_j$$. As usual, $$\widehat{V_i(x)}$$ means that this item is removed from the sequence.

There is no convenient way to write the second term in Lean for k = 0, so we only state this theorem for k = n + 1, see extDerivWithin_apply_vectorField and extDeriv_apply_vectorField.

In this case, we write the second term as a sum over i j : Fin (n + 1), i ≤ j, where the indexes (i, j) in our sum currespond to (i, j + 1) (formally, (Fin.castSucc i, Fin.succ j)) in the formula above. For this reason, we have - before the sum in our formal statement.

theorem extDerivWithin_apply_vectorField {𝕜 : 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} {ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F} {V : Fin (n + 2) → E → E} (hω : DifferentiableWithinAt 𝕜 ω s x) (hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) s x) (hsx : UniqueDiffWithinAt 𝕜 s x) : ((extDerivWithin ω s x) fun (x_1 : Fin (n + 1 + 1)) => V x_1 x) = ∑ i : Fin (n + 2), (-1) ^ ↑i • (fderivWithin 𝕜 (fun (x : E) => (ω x) (i.removeNth fun (x_1 : Fin (n + 1 + 1)) => V x_1 x)) s x) (V i x) - ∑ i : Fin (n + 1), ∑ j ∈ Finset.Ici i, (-1) ^ (↑i + ↑j) • (ω x) (Matrix.vecCons (VectorField.lieBracketWithin 𝕜 (V i.castSucc) (V j.succ) s x) (j.removeNth (i.castSucc.removeNth fun (x_1 : Fin (n + 1 + 1)) => V x_1 x)))

If ω is a differentiable (n + 1)-form and V i are n + 2 differentiable vector fields, then

$$ dω(V_0(x), \dots, V_{n + 1}(x)) = \left(\sum_{i=0}^{n + 1} (-1)^i • D_x(ω(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)))(V_i(x)) - \sum_{0 \le i \le j\le n} (-1)^{i + j} ω(x; [V_i, V_{j + 1}](x), V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_{j + 1}(x)}, …, V_k(x)), $$

where $$[V_i, V_{j + 1}]$$ is the commutator of the vector fields $$V_i$$ and $$V_{j + 1}$$. As usual, $$\widehat{V_i(x)}$$ means that this item is removed from the sequence.

In informal texts, this formula is usually written as

$$ dω(V_0(x), \dots, V_{n + 1}(x)) = \left(\sum_{i=0}^{n + 1} (-1)^i • D_x(ω(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)))(V_i(x)) - \sum_{0 \le i < j\le n + 1} (-1)^{i + j} ω(x; [V_i, V_j](x), V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_j(x)}, …, V_k(x)). $$

In the sum from our formalization, each index (i, j) corresponds to the index (Fin.castSucc i, Fin.succ j) in the sum used in informal texts.

For this reason, i + j in our sum has the opposite parity compared to informal texts, which changes the sign before the sum from + to -.

theorem extDeriv_apply_vectorField {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : E} {ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F} {V : Fin (n + 2) → E → E} (hω : DifferentiableAt 𝕜 ω x) (hV : ∀ (i : Fin (n + 2)), DifferentiableAt 𝕜 (V i) x) : ((extDeriv ω x) fun (x_1 : Fin (n + 1 + 1)) => V x_1 x) = ∑ i : Fin (n + 2), (-1) ^ ↑i • (fderiv 𝕜 (fun (x : E) => (ω x) (i.removeNth fun (x_1 : Fin (n + 1 + 1)) => V x_1 x)) x) (V i x) - ∑ i : Fin (n + 1), ∑ j ∈ Finset.Ici i, (-1) ^ (↑i + ↑j) • (ω x) (Matrix.vecCons (VectorField.lieBracket 𝕜 (V i.castSucc) (V j.succ) x) (j.removeNth (i.castSucc.removeNth fun (x_1 : Fin (n + 1 + 1)) => V x_1 x)))

If ω is a differentiable (n + 1)-form and V i are n + 2 differentiable vector fields, then

$$ dω(V_0(x), \dots, V_{n + 1}(x)) = \left(\sum_{i=0}^{n + 1} (-1)^i • D_x(ω(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)))(V_i(x)) - \sum_{0 \le i \le j\le n} (-1)^{i + j} ω(x; [V_i, V_{j + 1}](x), V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_{j + 1}(x)}, …, V_k(x)), $$

where $$[V_i, V_{j + 1}]$$ is the commutator of the vector fields $$V_i$$ and $$V_{j + 1}$$. As usual, $$\widehat{V_i(x)}$$ means that this item is removed from the sequence.

In informal texts, this formula is usually written as

$$ dω(V_0(x), \dots, V_{n + 1}(x)) = \left(\sum_{i=0}^{n + 1} (-1)^i • D_x(ω(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)))(V_i(x)) - \sum_{0 \le i < j\le n + 1} (-1)^{i + j} ω(x; [V_i, V_j](x), V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_j(x)}, …, V_k(x)). $$

In the sum from our formalization, each index (i, j) corresponds to the index (Fin.castSucc i, Fin.succ j) in the sum used in informal texts.

For this reason, i + j in our sum has the opposite parity compared to informal texts, which changes the sign before the sum from + to -.

theorem extDerivWithin_apply_vectorField_of_pairwise_commute {𝕜 : 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} {ω : E → E [⋀^Fin n]→L[𝕜] F} {V : Fin (n + 1) → E → E} (hω : DifferentiableWithinAt 𝕜 ω s x) (hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) s x) (hsx : UniqueDiffWithinAt 𝕜 s x) (hcomm : Pairwise fun (i j : Fin (n + 1)) => VectorField.lieBracketWithin 𝕜 (V i) (V j) s x = 0) : ((extDerivWithin ω s x) fun (x_1 : Fin (n + 1)) => V x_1 x) = ∑ i : Fin (n + 1), (-1) ^ ↑i • (fderivWithin 𝕜 (fun (x : E) => (ω x) (i.removeNth fun (x_1 : Fin (n + 1)) => V x_1 x)) s x) (V i x)

Let ω be a differentiable n-form and V i be n + 1 differentiable vector fields. If V i pairwise commute at x, i.e., $$[V_i, V_j](x) = 0$$ for all i ≠ j, then

$$ dω(V_0(x), \dots, V_{n + 1}(x)) = \left(\sum_{i=0}^{n + 1} (-1)^i • D_x(ω(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)))(V_i(x)). $$

theorem extDeriv_apply_vectorField_of_pairwise_commute {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : E} {ω : E → E [⋀^Fin n]→L[𝕜] F} {V : Fin (n + 1) → E → E} (hω : DifferentiableAt 𝕜 ω x) (hV : ∀ (i : Fin (n + 1)), DifferentiableAt 𝕜 (V i) x) (hcomm : Pairwise fun (i j : Fin (n + 1)) => VectorField.lieBracket 𝕜 (V i) (V j) x = 0) : ((extDeriv ω x) fun (x_1 : Fin (n + 1)) => V x_1 x) = ∑ i : Fin (n + 1), (-1) ^ ↑i • (fderiv 𝕜 (fun (x : E) => (ω x) (i.removeNth fun (x_1 : Fin (n + 1)) => V x_1 x)) x) (V i x)

Let ω be a differentiable n-form and V i be n + 1 differentiable vector fields. If V i pairwise commute at x, i.e., $$[V_i, V_j](x) = 0$$ for all i ≠ j, then

$$ dω(V_0(x), \dots, V_{n + 1}(x)) = \left(\sum_{i=0}^{n + 1} (-1)^i • D_x(ω(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)))(V_i(x)). $$