Gradient Slot Duhamel

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

The gradient-slot Duhamel representation of the localized velocity

Paper label lem:local-equation, displayed equation eq:local-equation. With φ a space-time cutoff supported in a compactly contained box Ω' × J, the localized velocity φu solves the whole-space heat equation with the heat-slot source localizedGradientSourceG and the divergence-form source ∂ⱼ localizedGradientSourceH. Testing the weak formulation of def:sws against the backward heat kernel, and using that a compactly supported localized field is determined by its heat potential, gives the representation φu = heatPotential G H almost everywhere.

The tested identity is supplied by gradientSlot_tested_transfer_of_sws; the passage from the tested identity to the potential is the established duhamel_of_localized_velocity, whose derivative slot carries the opposite sign convention and is converted by localized_gradient_slot_heat_representation.

theorem CKN.Core.Step3.localized_gradient_slot_duhamel_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))) (hDpweak : ∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Ω' ×ˢ J → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) : localizedVelocity φ u =ᵐ[MeasureTheory.volume] fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => HeatPotential.heatPotential (fun (w : Foundation.Parabolic.ParabolicPoint) => Step4.localizedGradientSourceG φ u Du f Dp w i) (fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) => Step4.localizedGradientSourceH φ u j w i) z

The gradient-slot Duhamel representation of the localized velocity, paper label lem:local-equation. For a suitable weak solution, a cutoff φ supported in a compactly contained box Ω' × J, and a weak pressure gradient Dp on that box, the localized velocity φu agrees almost everywhere with the heat potential of localizedGradientSourceG in the heat slot and localizedGradientSourceH in the divergence slot.