Weak divergence and curl identities along the bootstrap

Restriction of weak identities to smaller sets, and the propagation of the weak divergence-free condition and of the weak antisymmetric-derivative identity to weak derivatives. These supply the inputs of the div–curl recovery at each level of thm:vorticity-regularity.

theorem ESS.vorticity_restrict_identity {W W' : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW' : W' ⊆ W) {Φ Ψ : (CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hΦ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ∀ z ∉ tsupport ψ, Φ ψ z = 0) (hΨ : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ∀ z ∉ tsupport ψ, Ψ ψ z = 0) (h : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Φ ψ z = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ψ ψ z) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W' → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', Φ ψ z = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', Ψ ψ z

A weak identity between integrands supported where the test is supported restricts to every smaller set.

theorem ESS.vorticity_spatialPartial_off {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) (j : Fin 3) : CKN.spatialPartial ψ j z = 0

A spatial derivative of a test vanishes off its support.

theorem ESS.vorticity_weakPartial_restrict {W W' : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW' : W' ⊆ W) {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {j : Fin 3} (h : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, f y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, g y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W' → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', f y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', g y * ψ y

A weak derivative identity restricts to smaller sets.

theorem ESS.vorticityHeat_restrict {W W' : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW' : W' ⊆ W) {w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {F : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, w y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ j : Fin 3, F j y * CKN.spatialPartial ψ j y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W' → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', w y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', ∑ j : Fin 3, F j y * CKN.spatialPartial ψ j y

A weak heat equation restricts to smaller sets.

theorem ESS.vorticityDiv_restrict {W W' : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hW' : W' ⊆ W) {Y : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, Y i y * CKN.spatialPartial ψ i y = 0) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W' → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W', ∑ i : Fin 3, Y i y * CKN.spatialPartial ψ i y = 0

A weak divergence-free condition restricts to smaller sets.

theorem ESS.vorticityAnti_base {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (G i j) W MeasureTheory.volume) (hU : ∀ (i : Fin 3), MeasureTheory.IntegrableOn (U i) W MeasureTheory.volume) (hdU : ∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, G i j y * ψ y) (i k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, U k y * CKN.spatialPartial ψ i y - U i y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityAntisym (fun (l : Fin 3) => vorticityCurl G l y) i k * ψ y

The velocity satisfies the weak antisymmetric-derivative identity with the vorticity of its weak gradient.

theorem ESS.vorticity_weakPartial_testDeriv {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {Y Y' : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {m : Fin 3} (hdY : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y' y * ψ y) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψW : tsupport ψ ⊆ W) (a : Fin 3) : ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y' y * CKN.spatialPartial ψ a y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y y * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial ψ m y) a y

Moving a weak derivative onto a derivative of the test: ∫ Y' ∂ₐψ = -∫ Y ∂ₐ(∂ₘψ).

theorem ESS.vorticityDiv_deriv {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {Y Y' : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {m : Fin 3} (hY : ∀ (i : Fin 3), MeasureTheory.IntegrableOn (Y i) W MeasureTheory.volume) (hY' : ∀ (i : Fin 3), MeasureTheory.IntegrableOn (Y' i) W MeasureTheory.volume) (hdiv : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, Y i y * CKN.spatialPartial ψ i y = 0) (hdY : ∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y i y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y' i y * ψ y) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, Y' i y * CKN.spatialPartial ψ i y = 0

Weak derivatives of a weakly divergence-free field are weakly divergence free.

theorem ESS.vorticityAnti_deriv {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {Y Y' v v' : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {m : Fin 3} (hY : ∀ (i : Fin 3), MeasureTheory.IntegrableOn (Y i) W MeasureTheory.volume) (hv : ∀ (l : Fin 3), MeasureTheory.IntegrableOn (v l) W MeasureTheory.volume) (hv' : ∀ (l : Fin 3), MeasureTheory.IntegrableOn (v' l) W MeasureTheory.volume) (hanti : ∀ (i k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y k y * CKN.spatialPartial ψ i y - Y i y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityAntisym (fun (l : Fin 3) => v l y) i k * ψ y) (hdY : ∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y i y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y' i y * ψ y) (hdv : ∀ (l : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, v l y * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, v' l y * ψ y) (hY' : ∀ (i : Fin 3), MeasureTheory.IntegrableOn (Y' i) W MeasureTheory.volume) (i k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Y' k y * CKN.spatialPartial ψ i y - Y' i y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityAntisym (fun (l : Fin 3) => v' l y) i k * ψ y

Weak derivatives of a field satisfying the weak antisymmetric-derivative identity satisfy it with the derivative of the antisymmetric data.