Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.VorticitySmoothPackage

The weak and smooth relations among the bootstrap fields #

The velocity, its first and second derivatives, the vorticity and its first and second derivatives satisfy weak divergence and antisymmetric-derivative identities at each order; their backward mollifications satisfy the corresponding identities pointwise wherever the kernel ball lies in the box (the inputs of the div–curl steps of thm:vorticity-regularity).

source
theorem ESS.vorticityWeakRelations {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hWb : Bornology.IsBounded W) {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D2 Ω2 : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hU : ∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 (MeasureTheory.volume.restrict W)) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict W)) (hD2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (D2 i j k) 2 (MeasureTheory.volume.restrict W)) (hΩ1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 (MeasureTheory.volume.restrict W)) (hΩ2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (Ω2 i j k) 2 (MeasureTheory.volume.restrict W)) (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) (hdG : ∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, D2 i j k y * ψ y) (hdw : ∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i j y * ψ y) (hdΩ1 : ∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω2 i j k y * ψ y) (hdiv : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, U i y * CKN.spatialPartial ψ i y = 0) :
(∀ (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) ∧ (∀ (m : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, G i m y * CKN.spatialPartial ψ i y = 0) ∧ (∀ (m i k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, G k m y * CKN.spatialPartial ψ i y - G i m y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityAntisym (fun (l : Fin 3) => Ω1 l m y) i k * ψ y) ∧ (∀ (j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, D2 i j k y * CKN.spatialPartial ψ i y = 0) ∧ ∀ (j k i c : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, D2 c j k y * CKN.spatialPartial ψ i y - D2 i j k y * CKN.spatialPartial ψ c y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityAntisym (fun (l : Fin 3) => Ω2 l j k y) i c * ψ y

The weak divergence and antisymmetric-derivative identities of the first and second derivatives of the velocity.

source
theorem ESS.vorticitySmoothRelations {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hWo : IsOpen W) (hWb : Bornology.IsBounded W) {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D2 Ω2 : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hU : ∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 (MeasureTheory.volume.restrict W)) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict W)) (hD2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (D2 i j k) 2 (MeasureTheory.volume.restrict W)) (hΩ1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 (MeasureTheory.volume.restrict W)) (hΩ2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (Ω2 i j k) 2 (MeasureTheory.volume.restrict W)) (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) (hdG : ∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, D2 i j k y * ψ y) (hdw : ∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i j y * ψ y) (hdΩ1 : ∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω2 i j k y * ψ y) (hdiv : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, U i y * CKN.spatialPartial ψ i y = 0) {ε : ℝ} (hε : 0 < ε) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall (z - CKN.vorticityBackShift ε) ε ⊆ W) :
∑ i : Fin 3, CKN.spatialPartial (CKN.vorticityBackMollify W (U i) ε hε) i z = 0 ∧ (∀ (i k : Fin 3), CKN.spatialPartial (CKN.vorticityBackMollify W (U k) ε hε) i z - CKN.spatialPartial (CKN.vorticityBackMollify W (U i) ε hε) k z = vorticityAntisym (fun (l : Fin 3) => CKN.vorticityBackMollify W (vorticityCurl G l) ε hε z) i k) ∧ (∀ (i j : Fin 3), CKN.spatialPartial (CKN.vorticityBackMollify W (U i) ε hε) j z = CKN.vorticityBackMollify W (G i j) ε hε z) ∧ (∀ (m : Fin 3), ∑ i : Fin 3, CKN.spatialPartial (CKN.vorticityBackMollify W (G i m) ε hε) i z = 0) ∧ (∀ (m i k : Fin 3), CKN.spatialPartial (CKN.vorticityBackMollify W (G k m) ε hε) i z - CKN.spatialPartial (CKN.vorticityBackMollify W (G i m) ε hε) k z = vorticityAntisym (fun (l : Fin 3) => CKN.vorticityBackMollify W (Ω1 l m) ε hε z) i k) ∧ (∀ (i j k : Fin 3), CKN.spatialPartial (CKN.vorticityBackMollify W (G i j) ε hε) k z = CKN.vorticityBackMollify W (D2 i j k) ε hε z) ∧ (∀ (j k : Fin 3), ∑ i : Fin 3, CKN.spatialPartial (CKN.vorticityBackMollify W (D2 i j k) ε hε) i z = 0) ∧ (∀ (j k i c : Fin 3), CKN.spatialPartial (CKN.vorticityBackMollify W (D2 c j k) ε hε) i z - CKN.spatialPartial (CKN.vorticityBackMollify W (D2 i j k) ε hε) c z = vorticityAntisym (fun (l : Fin 3) => CKN.vorticityBackMollify W (Ω2 l j k) ε hε z) i c) ∧ (∀ (i j : Fin 3), CKN.spatialPartial (CKN.vorticityBackMollify W (vorticityCurl G i) ε hε) j z = CKN.vorticityBackMollify W (Ω1 i j) ε hε z) ∧ ∀ (i j k : Fin 3), CKN.spatialPartial (CKN.vorticityBackMollify W (Ω1 i j) ε hε) k z = CKN.vorticityBackMollify W (Ω2 i j k) ε hε z

The pointwise relations of the backward mollifications of the bootstrap fields.