Pressure Gradient Product

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

theorem CKN.Core.Step4.weak_gradient_trace_eq_zero_ae {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ} (hu : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x i) 2 (MeasureTheory.volume.restrict U)) (hDu : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du x i j) 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u x i) fun (x : Vec 3) => Du x i) (hdiv : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ U → ∫ (x : Foundation.Parabolic.Vec3) in U, ∑ i : Fin 3, u x i * spatialDeriv ψ i x = 0) : (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, Du x i i) =ᵐ[MeasureTheory.volume.restrict U] 0

theorem CKN.Core.Step4.weak_gradient_product_indicator {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ} (hu : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x i) 2 (MeasureTheory.volume.restrict U)) (hDu : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du x i j) 2 (MeasureTheory.volume.restrict U)) (hweak : ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u x i) fun (x : Vec 3) => Du x i) (i j : Fin 3) : HasWeakGradientOn U (fun (x : Vec 3) => U.indicator (fun (y : Foundation.Parabolic.Vec3) => u y i) x * U.indicator (fun (y : Foundation.Parabolic.Vec3) => u y j) x) fun (x : Vec 3) (k : Fin 3) => U.indicator (fun (y : Foundation.Parabolic.Vec3) => Du y i k) x * U.indicator (fun (y : Foundation.Parabolic.Vec3) => u y j) x + U.indicator (fun (y : Foundation.Parabolic.Vec3) => u y i) x * U.indicator (fun (y : Foundation.Parabolic.Vec3) => Du y j k) x