English
Under sufficient smoothness, the second exterior derivative vanishes: extDerivWithin (extDerivWithin ω s) s x = 0.
Русский
При достаточной гладкости второе внешнее производное равно нулю: extDerivWithin (extDerivWithin ω s) s x = 0.
LaTeX
$$$ h_ω : ContDiffWithinAt 𝕜 r ω s, \\ hr : minSmoothness 𝕜 2 ≤ r, \\ hs : UniqueDiffOn 𝕜 s, \\ hx : x ∈ closure (interior s), \\ h'x : x ∈ s \\Rightarrow extDerivWithin (extDerivWithin ω s) s x = 0 $$$
Lean4
/-- The second exterior derivative of a sufficiently smooth differential form is zero. -/
theorem extDerivWithin_extDerivWithin_apply (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 :=
calc
extDerivWithin (extDerivWithin ω s) s x =
alternatizeUncurryFin (fderivWithin 𝕜 (fun y ↦ alternatizeUncurryFin (fderivWithin 𝕜 ω s y)) s x) :=
rfl
_ = alternatizeUncurryFin (alternatizeUncurryFinCLM _ _ _ ∘L fderivWithin 𝕜 (fderivWithin 𝕜 ω s) s x) :=
by
congr 1
have : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 ω s) s x :=
by
refine (hω.fderivWithin_right hs ?_ h'x).differentiableWithinAt le_rfl
exact le_minSmoothness.trans hr
exact
alternatizeUncurryFinCLM _ _ _ |>.hasFDerivAt.comp_hasFDerivWithinAt x this.hasFDerivWithinAt |>.fderivWithin
(hs.uniqueDiffWithinAt h'x)
_ = 0 := alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric <| hω.isSymmSndFDerivWithinAt hr hs hx h'x
