The divergence-free initial-data space

The closure characterization of the Leray space in def:leray-hopf.

def CKN.IsWeakDivFreeL2 (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Prop

The weak-divergence formulation used in lem:J-weak-div.

Equations

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

def CKN.dotLinear : Foundation.Parabolic.Vec3 →ₗ[ℝ] Foundation.Parabolic.Vec3 →ₗ[ℝ] ℝ

The linear functional pairing a vector field with gradients of weak test functions.

Equations

• CKN.dotLinear = LinearMap.mk₂ ℝ (fun (x y : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, x i * y i) CKN.dotLinear._proof_1 CKN.dotLinear._proof_2 CKN.dotLinear._proof_3 CKN.dotLinear._proof_4

noncomputable def CKN.dotContinuous : Foundation.Parabolic.Vec3 →L[ℝ] Foundation.Parabolic.Vec3 →L[ℝ] ℝ

The continuous extension of the weak gradient-pairing functional.

Equations

• CKN.dotContinuous = CKN.dotLinear.mkContinuous₂ 3 CKN.dotContinuous._proof_1

noncomputable def CKN.testGradient (ψ : WeakTestFunction Set.univ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The coordinate gradient of a scalar weak test function.

Equations

• CKN.testGradient ψ x i = ψ.partialDeriv i x

theorem CKN.testGradient_memLp (ψ : WeakTestFunction Set.univ) : MeasureTheory.MemLp (testGradient ψ) 2 MeasureTheory.volume

noncomputable def CKN.testPairing (ψ : WeakTestFunction Set.univ) : ↥(MeasureTheory.Lp Foundation.Parabolic.Vec3 2 MeasureTheory.volume) →L[ℝ] ℝ

The integral pairing of a vector field with the gradient of a weak test function.

Equations

• CKN.testPairing ψ = (ContinuousLinearMap.lpPairing MeasureTheory.volume 2 2 CKN.dotContinuous).flip (MeasureTheory.MemLp.toLp (CKN.testGradient ψ) ⋯)

theorem CKN.smoothSolenoidal_test_integral_zero (v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (hdiv : ∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => v y i) i x = 0) (ψ : WeakTestFunction Set.univ) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, v x i * ψ.partialDeriv i x = 0

A smooth solenoidal field pairs to zero with gradients of compactly supported smooth scalar tests.

theorem CKN.isInJ_weakDivFree {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : IsWeakDivFreeL2 a

Compactly supported smooth solenoidal approximants imply weak divergence-freeness of their L² limit.

theorem CKN.smoothL2Potential_curl_memJ {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hA : ContDiff ℝ (↑⊤) A) (hA2 : MeasureTheory.MemLp A 2 MeasureTheory.volume) (hcurl2 : MeasureTheory.MemLp (curlVec3 A) 2 MeasureTheory.volume) : IsInJ (curlVec3 A)

A smooth L² vector potential with L² curl yields data in the Leray closure by cutting the potential off on expanding balls.

theorem CKN.isInJ_closed_under_L2_limit {aSeq : ℕ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (haSeq : ∀ (n : ℕ), IsInJ (aSeq n)) (hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (aSeq n - a) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : IsInJ a

The L² closure of smooth compactly supported solenoidal fields is closed under L² limits.