Signed coordinate evaluations of differential forms

Evaluating an n-form on the tuples obtained by omitting one of n + 1 vectors gives its signed coordinate coefficients. Summing the directional derivatives of these coefficients recovers the actual exterior derivative. The within-set identity is shared by the full-space and half-space Stokes proofs.

def ContinuousAlternatingMap.signedRemoveNth {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (v : Fin (n + 1) → E) : E [⋀^Fin n]→L[𝕜] F →L[𝕜] Fin (n + 1) → F

Signed evaluations on the tuples obtained by removing one vector, as a continuous linear map on alternating forms. In a coordinate basis these are the vector-field coefficients used in the divergence expression of the exterior derivative.

@[simp]

theorem ContinuousAlternatingMap.signedRemoveNth_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (v : Fin (n + 1) → E) (ω : E [⋀^Fin n]→L[𝕜] F) (i : Fin (n + 1)) : (signedRemoveNth v) ω i = (-1) ^ ↑i • ω (i.removeNth v)

theorem DifferentiableWithinAt.sum_fderivWithin_signedRemoveNth {𝕜 : 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) : ∑ i : Fin (n + 1), (fderivWithin 𝕜 (⇑(ContinuousAlternatingMap.signedRemoveNth v) ∘ ω) s x) (v i) i = (extDerivWithin ω s x) v

The sum of the directional derivatives of signed omission coefficients is the exterior derivative on the original tuple. Only differentiability within the given set is required.