Fourier identities for the regularized Leray potential

theorem CKN.regularizedFrequencyWeight_mul_one_add_sum_sq (δ : ℝ) (ξ : Foundation.Parabolic.L2Vec3) : regularizedFrequencyWeight δ ξ * (1 + ∑ i : Fin 3, regularizedFrequencyCoord δ i ξ ^ 2) = 1

The regularization weight times its quadratic denominator is one.

noncomputable def CKN.regularizedPotentialCurl {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The curl of the regularized potential field.

Equations

• CKN.regularizedPotentialCurl ha δ hδ = CKN.curlOfGradient (CKN.regularizedPotentialGradientVec3 ha δ hδ)

theorem CKN.regularizedPotentialCurl_memJ {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) : IsInJ (regularizedPotentialCurl ha δ hδ)

Each regularized potential curl belongs to the L² closure defining J.

noncomputable def CKN.regularizedPotentialCurlComponentLp {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

One complex coordinate of the regularized curl.

Equations

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

theorem CKN.toTemperedDistribution_sub_l2 (u v : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.Lp.toTemperedDistribution (u - v) = MeasureTheory.Lp.toTemperedDistribution u - MeasureTheory.Lp.toTemperedDistribution v

The L² embedding into tempered distributions preserves subtraction.

theorem CKN.regularizedPotentialCurlComponentLp_toDist {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) : MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialCurlComponentLp ha δ hδ i) = if i = 0 then (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 1 0)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 1)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 1 1)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 0)) - ((TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 2 2)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 0)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 2 0)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 2))) else if i = 1 then (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 2 1)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 2)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 2 2)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 1)) - ((TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 0 0)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 1)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 0 1)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 0))) else (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 0 2)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 0)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 0 0)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 2)) - ((TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 1 1)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 2)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ 1 2)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 1)))

The distribution associated to a regularized curl coordinate is the corresponding combination of first-derivative Fourier multipliers.

def CKN.frequencyCoordinateComplex (i : Fin 3) : Foundation.Parabolic.L2Vec3 → ℂ

The complex-valued Fourier coordinate functional for component i.

Equations

• CKN.frequencyCoordinateComplex i ξ = ↑((CKN.frequencyL2Coord i) ξ)

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

The complex Fourier weight obtained from the real regularized frequency weight.

Equations

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

noncomputable def CKN.weightedFrequencyCoordinate (δ : ℝ) (i : Fin 3) : Foundation.Parabolic.L2Vec3 → ℂ

The ith frequency coordinate multiplied by the regularized Fourier weight.

Equations

• CKN.weightedFrequencyCoordinate δ i ξ = CKN.frequencyCoordinateComplex i ξ * CKN.regularizedWeightComplex δ ξ

theorem CKN.weakDivFreeL2_regularizedFrequencyDivergence_zero {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) (δ : ℝ) (i : Fin 3) : ∑ j : Fin 3, (TemperedDistribution.fourierMultiplierCLM ℂ fun (ξ : Foundation.Parabolic.L2Vec3) => ↑(regularizedFrequencyCoord δ i ξ * regularizedFrequencyCoord δ j ξ * regularizedFrequencyWeight δ ξ)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ⋯ j)) = 0

A weakly divergence-free L² field annihilates the regularized frequency-weighted divergence multiplier.

theorem CKN.regularizedPotentialCurlComponentLp_real_eq {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) : (fun (y : Foundation.Parabolic.L2Vec3) => (↑↑(regularizedPotentialCurlComponentLp ha δ hδ i) y).re) =ᵐ[MeasureTheory.volume] fun (y : Foundation.Parabolic.L2Vec3) => regularizedPotentialCurl ha δ hδ y.ofLp i

Taking real parts of the complex regularized curl recovers the real regularized curl on the spatial carrier.