Weak derivatives commute #
Let u have weak derivatives u₁ in the direction v and u₂ in the direction w on an open
set Ω. If u₁ has a weak derivative u₁₂ in the direction w, then u₂ has the same weak
derivative u₁₂ in the direction v: the mixed weak derivatives ∂_w ∂_v u and ∂_v ∂_w u
agree as soon as one of them exists. No regularity beyond the existence of the three weak
derivatives is assumed.
The proof moves both derivatives onto the test function and uses that directional derivatives of
test functions commute (TestFunction.lineDerivOp_comm).
Main declarations #
TauCeti.HasWeakLineDerivOn.comm: weak derivatives in two directions commute.
theorem
TauCeti.HasWeakLineDerivOn.comm
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace E]
{μ : MeasureTheory.Measure E}
{Ω : TopologicalSpace.Opens E}
{u u₁ u₂ u₁₂ : E → F}
{v w : E}
(h₁ : HasWeakLineDerivOn μ Ω u u₁ v)
(h₁₂ : HasWeakLineDerivOn μ Ω u₁ u₁₂ w)
(h₂ : HasWeakLineDerivOn μ Ω u u₂ w)
:
HasWeakLineDerivOn μ Ω u₂ u₁₂ v
Weak derivatives commute. If u has weak derivatives u₁ = ∂_v u and u₂ = ∂_w u on
Ω, and u₁ has a weak derivative u₁₂ = ∂_w ∂_v u, then u₁₂ is also a weak derivative of
u₂ in the direction v, that is, ∂_v ∂_w u = ∂_w ∂_v u.