Weak Derivative Curl Identity

This is a compact-support weak integration-by-parts identity for two directional derivatives of the same scalar function.

Let $f$ have weak derivatives $p$ and $q$ along directions $v$ and $w$, respectively, with $p$ and $q$ locally in $L^2$. Let $\eta$ have weak derivatives $a$ and $b$ along $v$ and $w$, respectively. Assume $\eta,a,b$ have compact support and $a,b$ are globally in $L^2$. Then

The identity is valid in every finite dimension, including dimension zero, and is a supporting rough-testing statement.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem integral_weakDeriv_mul_eq_swap {n : ℕ}
    {f p q η a b : EuclideanSpace ℝ (Fin n) → ℝ}
    {v w : EuclideanSpace ℝ (Fin n)}
    (hp : HasWeakDerivAlong f p v) (hq : HasWeakDerivAlong f q w)
    (hp2 : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp p 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    (hq2 : ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp q 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    (hηv : HasWeakDerivAlong η a v) (hηw : HasWeakDerivAlong η b w)
    (hηc : HasCompactSupport η) (hac : HasCompactSupport a) (hbc : HasCompactSupport b)
    (ha2 : MemLp a 2 (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hb2 : MemLp b 2 (volume : Measure (EuclideanSpace ℝ (Fin n)))) :
    (∫ x, p x * b x ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
      ∫ x, q x * a x ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: exists_contDiff_compact_weak_deriv_approximation.

Previous: HasWeakDerivAlong.mul_of_locally_bounded · Next: compact_bounded_test_domination.

Source excerpt, lines 833–846 · Frozen source 408915f.