JSpace Fourier Converse

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.regularizedPositiveDerivativeSymbol (δ : ℝ) (k j : Fin 3) : Foundation.Parabolic.L2Vec3 → ℂ

The regularized positive-frequency derivative multiplier used in the Fourier approximation.

Equations

• CKN.regularizedPositiveDerivativeSymbol δ k j ξ = ↑(CKN.regularizedFrequencyCoord δ k ξ * CKN.regularizedFrequencyCoord δ j ξ * CKN.regularizedFrequencyWeight δ ξ)

noncomputable def CKN.regularizationScale (n : ℕ) : ℝ

The positive scale sequence used to remove the Fourier regularization.

Equations

• CKN.regularizationScale n = 1 / ↑(n + 1)

noncomputable def CKN.regularizedWeightMultiplier (δ : ℝ) : Foundation.Parabolic.L2Vec3 → ℂ

The complex Fourier multiplier associated with the regularized frequency weight.

Equations

• CKN.regularizedWeightMultiplier δ ξ = ↑(CKN.regularizedFrequencyWeight δ ξ)

noncomputable def CKN.regularizedCurlMultiplier (δ : ℝ) : Foundation.Parabolic.L2Vec3 → ℂ

The Fourier multiplier representing the regularized curl operation.

Equations

• CKN.regularizedCurlMultiplier δ ξ = ↑(1 - CKN.regularizedFrequencyWeight δ ξ)

theorem CKN.regularizationScale_pos (n : ℕ) : 0 < regularizationScale n

Every term of regularizationScale is positive.

theorem CKN.regularizedPotentialCurlComponentLp_error_tendsto {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) (i : Fin 3) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (↑↑(regularizedPotentialCurlComponentLp ⋯ (regularizationScale n) ⋯ i - weakFieldFourierComponent ⋯ i)) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

The Fourier multiplier error of the regularized curl tends to zero in L² on each complex coordinate.