JSpace Fourier Limit

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.regularizedPotentialCurlSequence {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) : ℕ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The sequence of regularized curls used to approximate a weakly divergence-free field.

Equations

• CKN.regularizedPotentialCurlSequence ha n = CKN.regularizedPotentialCurl ⋯ (CKN.regularizationScale n) ⋯

noncomputable def CKN.regularizedPotentialCurlCoordError {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) (n : ℕ) (i : Fin 3) : Foundation.Parabolic.Vec3 → ℝ

The coordinatewise error between the regularized potential curl and the target field.

Equations

• CKN.regularizedPotentialCurlCoordError ha n i x = CKN.regularizedPotentialCurlSequence ha n x i - a x i

noncomputable def CKN.regularizedPotentialCurlErrorMajor {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) (n : ℕ) : Foundation.Parabolic.Vec3 → ℝ

The scalar pointwise majorant for a coordinate error in the regularized curl approximation.

Equations

• CKN.regularizedPotentialCurlErrorMajor ha n x = ∑ i : Fin 3, ‖CKN.regularizedPotentialCurlCoordError ha n i x‖

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

A square-integrable weakly divergence-free field lies in the closure of compactly supported smooth divergence-free fields.

theorem CKN.isInJ_iff_weakDivFree {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} : IsInJ a ↔ IsWeakDivFreeL2 a

The closure definition of J agrees with weak divergence-freeness in L².