Pointwise identities for backward mollifications

Constant-coefficient weak identities on an open set hold pointwise for the backward mollifications at every point whose kernel support lies inside the set. These are the smooth forms of the weak vorticity equation, of weak derivatives, and of the divergence and curl constraints used in the bootstrap of thm:vorticity-regularity of the Escauriaza–Seregin–Šverák manuscript.

theorem CKN.vorticity_spatialSecondPartial_eq_fderiv {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (j k : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialSecondPartial F j k z = (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ F y) (basisVec j, 0)) z) (basisVec k, 0)

A second coordinate derivative of a smooth space-time function is an iterated directional derivative.

theorem CKN.vorticityBackTest_admissible {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {ε : ℝ} (hε : 0 < ε) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall (z - vorticityBackShift ε) ε ⊆ W) : ContDiff ℝ (↑⊤) (vorticityBackTest ε hε z) ∧ HasCompactSupport (vorticityBackTest ε hε z) ∧ tsupport (vorticityBackTest ε hε z) ⊆ W

The backward test is admissible on an open set containing the closed kernel ball.

theorem CKN.vorticityBackTest_pairing_spatialPartial {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f W MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) (j : Fin 3) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, f y * spatialPartial (vorticityBackTest ε hε z) j y = -spatialPartial (vorticityBackMollify W f ε hε) j z

Pairing with a spatial derivative of the backward test.

theorem CKN.vorticityBackTest_pairing_timePartial {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f W MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, f y * timePartial (vorticityBackTest ε hε z) y = -timePartial (vorticityBackMollify W f ε hε) z

Pairing with the time derivative of the backward test.

theorem CKN.vorticityBackTest_pairing_spatialSecondPartial {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f W MeasureTheory.volume) {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.Vec3 × ℝ) (j k : Fin 3) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, f y * spatialSecondPartial (vorticityBackTest ε hε z) j k y = spatialSecondPartial (vorticityBackMollify W f ε hε) j k z

Pairing with a second spatial derivative of the backward test.

theorem CKN.vorticityBackMollify_spatialPartial_of_weak {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : IsOpen W) {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f W MeasureTheory.volume) {j : Fin 3} (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, f y * spatialPartial ψ j y = -∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, g y * ψ y) {ε : ℝ} (hε : 0 < ε) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall (z - vorticityBackShift ε) ε ⊆ W) : spatialPartial (vorticityBackMollify W f ε hε) j z = vorticityBackMollify W g ε hε z

A weak spatial derivative on an open set commutes with backward mollification at points whose kernel support lies inside the set.

theorem CKN.vorticityBackMollify_heat_of_weak {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : IsOpen W) {w : Foundation.Parabolic.Vec3 × ℝ → ℝ} {F : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ} (hw : MeasureTheory.IntegrableOn w W MeasureTheory.volume) (hF : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (F j) W MeasureTheory.volume) (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, w y * (-timePartial ψ y - ∑ j : Fin 3, spatialSecondPartial ψ j j y) = -∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, ∑ j : Fin 3, F j y * spatialPartial ψ j y) {ε : ℝ} (hε : 0 < ε) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall (z - vorticityBackShift ε) ε ⊆ W) : timePartial (vorticityBackMollify W w ε hε) z - ∑ j : Fin 3, spatialSecondPartial (vorticityBackMollify W w ε hε) j j z = ∑ j : Fin 3, spatialPartial (vorticityBackMollify W (F j) ε hε) j z

The weak heat equation with a divergence-form source holds pointwise for backward mollifications at points whose kernel support lies inside the domain.

theorem CKN.vorticityBackMollify_div_of_weak {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : IsOpen W) {Y : Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ} (hY : ∀ (i : Fin 3), MeasureTheory.IntegrableOn (Y i) W MeasureTheory.volume) (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, Y i y * spatialPartial ψ i y = 0) {ε : ℝ} (hε : 0 < ε) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall (z - vorticityBackShift ε) ε ⊆ W) : ∑ i : Fin 3, spatialPartial (vorticityBackMollify W (Y i) ε hε) i z = 0

A weak divergence constraint holds pointwise for backward mollifications.

theorem CKN.vorticityBackMollify_curl_of_weak {W : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : IsOpen W) {Ya Yb Ω : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hYa : MeasureTheory.IntegrableOn Ya W MeasureTheory.volume) (hYb : MeasureTheory.IntegrableOn Yb W MeasureTheory.volume) {a b : Fin 3} (hweak : ∀ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, Yb y * spatialPartial ψ a y - Ya y * spatialPartial ψ b y = -∫ (y : Foundation.Parabolic.Vec3 × ℝ) in W, Ω y * ψ y) {ε : ℝ} (hε : 0 < ε) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall (z - vorticityBackShift ε) ε ⊆ W) : spatialPartial (vorticityBackMollify W Yb ε hε) a z - spatialPartial (vorticityBackMollify W Ya ε hε) b z = vorticityBackMollify W Ω ε hε z

A weak antisymmetric derivative identity holds pointwise for backward mollifications.