Theorems · Theorem · global analysis

extDerivWithin_apply_vectorField_of_pairwise_commute

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {s : Set E} {x : E}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {V : Fin (n + 1) → E → E},
  DifferentiableWithinAt 𝕜 ω s x →
    (∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) s x) →
      UniqueDiffWithinAt 𝕜 s x →
        (Pairwise fun i j => VectorField.lieBracketWithin 𝕜 (V i) (V j) s x = 0) →
          ((extDerivWithin ω s x) fun x_1 => V x_1 x) =
            ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x => (ω x) (i.removeNth fun x_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)) = \sum_{i=0}^{n + 1} (-1)^i • D_x\left(ω\big(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)\big)\right)(V_i(x)). $$

Defined in

Mathlib.Analysis.Calculus.DifferentialForm.VectorField

Cited by

1 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace