Product H1

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.HasWeakGradientOn.mul_of_memLp_two {U : Set (Vec 3)} (hU : IsOpen U) {u v : Vec 3 → ℝ} {Du Dv : Vec 3 → Vec 3} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict U)) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict U)) (hDu : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Vec 3) => Du x i) 2 (MeasureTheory.volume.restrict U)) (hDv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Vec 3) => Dv x i) 2 (MeasureTheory.volume.restrict U)) (hwu : HasWeakGradientOn U u Du) (hwv : HasWeakGradientOn U v Dv) : HasWeakGradientOn U (fun (x : Vec 3) => u x * v x) fun (x : Vec 3) (i : Fin 3) => Du x i * v x + u x * Dv x i