Support and almost-everywhere stability of weak partial derivatives

Three elementary facts used when weak derivatives produced on small sets are combined on a larger one: a weak derivative may be replaced by any function equal to it almost everywhere on the domain; the product of a locally integrable function with a compactly supported continuous function is integrable on the domain; and a set integral of a function supported in a common subset does not see the ambient set.

theorem CKN.HasWeakPartialDerivOn.congr_deriv_ae {d : ℕ} {U : Set (Vec d)} {i : Fin d} {u g h : Vec d → ℝ} (hgh : g =ᵐ[MeasureTheory.volume.restrict U] h) (hg : HasWeakPartialDerivOn U i u g) : HasWeakPartialDerivOn U i u h

A weak partial derivative may be replaced by any function that agrees with it almost everywhere on the domain: the defining integral identity only sees the values of the derivative through the ambient measure restricted to U.

theorem CKN.integrableOn_mul_continuous_of_locallyIntegrableOn {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) {u c : Vec d → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hc : Continuous c) (hcc : IsCompact (tsupport c)) (hcU : tsupport c ⊆ U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => u x * c x) U MeasureTheory.volume

A locally integrable function times a compactly supported continuous function is integrable on a measurable domain containing the support of the continuous factor.

theorem CKN.setIntegral_eq_of_support_subset {d : ℕ} {A B S : Set (Vec d)} {F : Vec d → ℝ} (hzero : ∀ x ∉ S, F x = 0) (hA : S ⊆ A) (hB : S ⊆ B) : ∫ (x : Vec d) in A, F x = ∫ (x : Vec d) in B, F x

A set integral of a function that vanishes off a set S agrees on any two ambient sets containing S: the integrand is invisible outside S, so neither ambient set contributes anything beyond it.