Localized Equation Gradient Data

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

theorem CKN.Core.Step4.localized_gradient_source_data_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ spaceTimeTestFunction Ω I) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) (hφbox : tsupport φ ⊆ Ω' ×ˢ J) {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hDpInt : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) : (∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i) MeasureTheory.volume) ∧ (∀ (j i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => -localizedGradientSourceH φ u j z i) MeasureTheory.volume) ∧ (∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i) ∧ ∀ (j i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => -localizedGradientSourceH φ u j z i