JSpace Fourier

Supporting estimates for the Navier–Stokes development.

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

The linear functional pairing an extended vector field with test gradients.

Equations

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

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

The continuous extension of the test-gradient pairing on the extension space.

Equations

• CKN.extensionDotContinuous = CKN.extensionDotLinear.mkContinuous₂ 3 CKN.extensionDotContinuous._proof_1

noncomputable def CKN.schwartzGradient (ψ : SchwartzMap Foundation.Parabolic.Vec3 ℝ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The Schwartz-space gradient of a scalar Schwartz function on the Hilbert coordinates.

Equations

• CKN.schwartzGradient ψ x i = CKN.spatialDeriv (⇑ψ) i x

noncomputable def CKN.cutoffSchwartzGradient (ψ : SchwartzMap Foundation.Parabolic.Vec3 ℝ) (n : ℕ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The gradient of a Schwartz test function after applying the spatial cutoff.

Equations

• CKN.cutoffSchwartzGradient ψ n x i = CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.canonicalBallCutoff 0 (↑(n + 1)) (2 * ↑(n + 1)) y * ψ y) i x

noncomputable def CKN.extensionPairing (a : ↥(MeasureTheory.Lp Foundation.Parabolic.Vec3 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp Foundation.Parabolic.Vec3 2 MeasureTheory.volume) →L[ℝ] ℝ

The continuous extension-space pairing with the gradient of a compactly supported test function.

Equations

• CKN.extensionPairing a = (ContinuousLinearMap.lpPairing MeasureTheory.volume 2 2 CKN.extensionDotContinuous) a

theorem CKN.isWeakDivFreeL2_schwartz {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) (ψ : SchwartzMap Foundation.Parabolic.Vec3 ℝ) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, a x i * spatialDeriv (⇑ψ) i x = 0

The weak divergence identity extends from compact tests to every real Schwartz test.