The force-pressure gradient is a limit of test-function gradients

The gradients of smooth compactly supported functions span a subspace of spatial L² whose orthogonal complement consists of weakly divergence-free fields. By the orthogonality of (I - ℙ) f to those fields, the gradient field of lem:force-pressure lies in the closure of the test gradients.

noncomputable def CKN.Leray.forcePressureTestGradient (φ : WeakTestFunction Set.univ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The classical gradient of a whole-space test function, as a coordinate vector field.

Equations

• CKN.Leray.forcePressureTestGradient φ x i = φ.partialDeriv i x

theorem CKN.Leray.forcePressureTestGradient_continuous (φ : WeakTestFunction Set.univ) : Continuous (forcePressureTestGradient φ)

The gradient of a test function is continuous.

theorem CKN.Leray.forcePressureTestGradient_hasCompactSupport (φ : WeakTestFunction Set.univ) : HasCompactSupport (forcePressureTestGradient φ)

The gradient of a test function has compact support.

theorem CKN.Leray.forcePressureTestGradient_memLp (φ : WeakTestFunction Set.univ) : MeasureTheory.MemLp (forcePressureTestGradient φ) 2 MeasureTheory.volume

The gradient of a test function is square integrable.

noncomputable def CKN.Leray.forcePressureTestGradientL2 (φ : WeakTestFunction Set.univ) : ↥RealVectorL2

The gradient of a test function as a real spatial L² field.

Equations

• CKN.Leray.forcePressureTestGradientL2 φ = CKN.Leray.realVectorL2OfCoordinateFunction (CKN.Leray.forcePressureTestGradient φ) ⋯

theorem CKN.Leray.realVectorL2Representative_apply (u : ↥RealVectorL2) (x : Foundation.Parabolic.Vec3) : realVectorL2Representative u x = (↑↑u (WithLp.toLp 2 x)).ofLp

The coordinate representative evaluates the Hilbert field at the corresponding point.

theorem CKN.Leray.realVectorL2Representative_memLp_two (u : ↥RealVectorL2) : MeasureTheory.MemLp (realVectorL2Representative u) 2 MeasureTheory.volume

The coordinate representative of a real spatial L² field is square integrable on the coordinate carrier.

theorem CKN.Leray.realVectorL2Representative_linearCombination_ae (a b : ℝ) (u v : ↥RealVectorL2) : realVectorL2Representative (a • u + b • v) =ᵐ[MeasureTheory.volume] a • realVectorL2Representative u + b • realVectorL2Representative v

The coordinate representative is linear up to null sets.

def CKN.Leray.forcePressureTestAdd (φ ψ : WeakTestFunction Set.univ) : WeakTestFunction Set.univ

The sum of two whole-space test functions.

Equations

• CKN.Leray.forcePressureTestAdd φ ψ = { toFun := fun (x : CKN.Vec 3) => φ.toFun x + ψ.toFun x, contDiff := ⋯, hasCompactSupport := ⋯, tsupport_subset := ⋯ }

def CKN.Leray.forcePressureTestSmul (c : ℝ) (φ : WeakTestFunction Set.univ) : WeakTestFunction Set.univ

A scalar multiple of a whole-space test function.

Equations

• CKN.Leray.forcePressureTestSmul c φ = { toFun := fun (x : CKN.Vec 3) => c * φ.toFun x, contDiff := ⋯, hasCompactSupport := ⋯, tsupport_subset := ⋯ }

def CKN.Leray.forcePressureTestZero : WeakTestFunction Set.univ

The zero whole-space test function.

Equations

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

theorem CKN.Leray.forcePressureTestGradient_add (φ ψ : WeakTestFunction Set.univ) : forcePressureTestGradient (forcePressureTestAdd φ ψ) = forcePressureTestGradient φ + forcePressureTestGradient ψ

The gradient of a sum of test functions is the sum of the gradients.

theorem CKN.Leray.forcePressureTestGradient_smul (c : ℝ) (φ : WeakTestFunction Set.univ) : forcePressureTestGradient (forcePressureTestSmul c φ) = c • forcePressureTestGradient φ

The gradient of a scalar multiple of a test function.

theorem CKN.Leray.forcePressureTestGradientL2_zero : forcePressureTestGradientL2 forcePressureTestZero = 0

The zero test function has zero gradient field.

noncomputable def CKN.Leray.forcePressureTestGradientSpan : Submodule ℝ ↥RealVectorL2

The real subspace spanned by the gradients of whole-space test functions.

Equations

• CKN.Leray.forcePressureTestGradientSpan = Submodule.span ℝ (Set.range CKN.Leray.forcePressureTestGradientL2)

theorem CKN.Leray.forcePressureTestGradientSpan_mem_range {u : ↥RealVectorL2} (hu : u ∈ forcePressureTestGradientSpan) : ∃ (φ : WeakTestFunction Set.univ), forcePressureTestGradientL2 φ = u

Every element of the span of the test gradients is the gradient of one test function.

theorem CKN.Leray.inner_forcePressureTestGradientL2_eq_integral (φ : WeakTestFunction Set.univ) (w : ↥RealVectorL2) : inner ℝ (forcePressureTestGradientL2 φ) w = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, realVectorL2Representative w x i * φ.partialDeriv i x

The pairing of a test gradient with a real spatial L² field is the integral of the coordinate dot product.

theorem CKN.Leray.isWeakDivFree_of_mem_orthogonal_testGradientSpan {w : ↥RealVectorL2} (hw : w ∈ forcePressureTestGradientSpanᗮ) : IsWeakDivFreeL2 (realVectorL2Representative w)

A field orthogonal to all test gradients has a weakly divergence-free representative.

theorem CKN.Leray.forcePressureGradientL2_mem_topologicalClosure (v : ↥RealVectorL2) : forcePressureGradientL2 v ∈ forcePressureTestGradientSpan.topologicalClosure

The force-pressure gradient field (I - ℙ) f of lem:force-pressure lies in the closure of the test gradients.

theorem CKN.Leray.exists_testGradient_tendsto_forcePressureGradientL2 (v : ↥RealVectorL2) : ∃ (φ : ℕ → WeakTestFunction Set.univ), Filter.Tendsto (fun (n : ℕ) => forcePressureTestGradientL2 (φ n)) Filter.atTop (nhds (forcePressureGradientL2 v))

The force-pressure gradient field (I - ℙ) f of lem:force-pressure is an L² limit of gradients of test functions.