Weak partial derivatives are a local property

Being the ith weak partial derivative is checked against test functions with compact support, so it is local: if a single locally integrable function is the ith weak partial derivative of u on every member of an open cover of U, then it is the ith weak partial derivative of u on U itself.

The proof decomposes a test function with the finite smooth partition of unity of exists_smooth_partition_of_unity_of_isCompact, applies the hypothesis to each piece, and reassembles the integrals. The corresponding statement was not available anywhere: the previously existing interface for weak derivatives consisted only of restriction, transport and almost-everywhere uniqueness.

theorem CKN.hasWeakPartialDerivOn_of_isOpen_cover {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {V : ι → Set (Vec d)} {i : Fin d} {u g : Vec d → ℝ} (hU : MeasurableSet U) (hV : ∀ (b : ι), IsOpen (V b)) (hcover : U ⊆ ⋃ (b : ι), V b) (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g U MeasureTheory.volume) (hloc : ∀ (b : ι), HasWeakPartialDerivOn (V b) i u g) : HasWeakPartialDerivOn U i u g

Locality of weak partial derivatives. If g is the ith weak partial derivative of u on each member of an open cover of U, and both u and g are locally integrable on U, then g is the ith weak partial derivative of u on U.

The cover members are not required to be contained in U; only that they cover U and that the identity holds on each of them.