Product rules for compactly supported smooth multipliers

The statements here use the representative functions carried by the weak-derivative predicate. Compact support keeps every test-function product inside the open set, so the resulting derivative is a global weak derivative of the zero extension.

theorem CKN.HasWeakPartialDerivOn.mul_smooth_zeroExtend {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {i : Fin d} {u gi : Vec d → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hgi : MeasureTheory.LocallyIntegrableOn gi U MeasureTheory.volume) (hweak : HasWeakPartialDerivOn U i u gi) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηCompact : HasCompactSupport η) (hηU : tsupport η ⊆ U) : HasWeakPartialDerivOn Set.univ i (fun (x : Vec d) => η x * u x) fun (x : Vec d) => η x * gi x + u x * (fderiv ℝ η x) (basisVec i)

theorem CKN.HasWeakGradientOn.mul_smooth_zeroExtend {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {u : Vec d → ℝ} {g : Vec d → Vec d} (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hg : ∀ (i : Fin d), MeasureTheory.LocallyIntegrableOn (fun (x : Vec d) => g x i) U MeasureTheory.volume) (hweak : HasWeakGradientOn U u g) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηCompact : HasCompactSupport η) (hηU : tsupport η ⊆ U) : HasWeakGradientOn Set.univ (fun (x : Vec d) => η x * u x) fun (x : Vec d) => η x • g x + u x • classicalGradient η x

theorem CKN.HasWeakPartialDerivOn.mono {d : ℕ} {U V : Set (Vec d)} (hVOpen : IsOpen V) (hVU : V ⊆ U) {i : Fin d} {u gi : Vec d → ℝ} (h : HasWeakPartialDerivOn U i u gi) : HasWeakPartialDerivOn V i u gi

theorem CKN.HasWeakGradientOn.mono {d : ℕ} {U V : Set (Vec d)} (hVOpen : IsOpen V) (hVU : V ⊆ U) {u : Vec d → ℝ} {Du : Vec d → Vec d} (h : HasWeakGradientOn U u Du) : HasWeakGradientOn V u Du