Source Morrey Gradient

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

The pressure-gradient source is kept in the heat slot. The definitions below are deliberately separate from the divergence-form sources: the latter place p * φ in the spatial derivative slot and therefore have a different Morrey order.

noncomputable def CKN.Core.Step4.localizedGradientSourceG (φ : Foundation.Parabolic.ParabolicPoint → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

Localized scalar heat source after subtracting the cutoff times the weak pressure gradient.

Equations

• CKN.Core.Step4.localizedGradientSourceG φ u Du f Dp z i = CKN.Core.Step3.localizedEquationG φ u Du f z i - φ z * Dp z i

noncomputable def CKN.Core.Step4.localizedGradientSourceH (φ : Foundation.Parabolic.ParabolicPoint → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

Localized divergence source in the pressure-gradient formulation of the heat equation.

Equations

• CKN.Core.Step4.localizedGradientSourceH φ u = CKN.Core.Step3.localizedEquationH φ u

noncomputable def CKN.Core.Step4.vectorHeatPotential (F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

Componentwise vector heat potential of scalar and divergence sources.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.vectorHeatPotential_eq_duhamelPotential_neg {F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (z : Foundation.Parabolic.ParabolicPoint) : vectorHeatPotential F G z = Step3.duhamelPotential F (fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) => -G j w) z

theorem CKN.Core.Step4.localized_gradient_slot_heat_representation {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hrep : Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume] Step3.duhamelPotential (localizedGradientSourceG φ u Du f Dp) fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) => -localizedGradientSourceH φ u j w) : Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume] vectorHeatPotential (localizedGradientSourceG φ u Du f Dp) (localizedGradientSourceH φ u)

The exact sign adapter for the gradient-slot representation. Thus a representation through the Duhamel-named interface passes -G as its derivative source, while the heat-potential consumer sees G.