The quadratic pressure in frequency variables

For a real tensor field T, the real part of the inverse transform of the double-Riesz symbol applied to T̂ satisfies the Laplacian identity of the Riesz pressure of T. Both are square integrable, so their difference is a square-integrable weakly harmonic function and vanishes by Liouville's theorem: the Riesz pressure has the frequency representation used in the pressure pairing of eq:reg-momentum-forced.

theorem CKN.Leray.pressureApplyFormula_eq (ξ : Foundation.Parabolic.L2Vec3) (F : ComplexTensor3) : pressureApplyFormula ξ F = -↑(inverseFrequencyNormSq ξ) * inner ℂ (complexifyFrequency ξ) ((tensorDivergenceLinear ξ) F)

theorem CKN.Leray.inverseFrequencyNormSq_mul (ξ : Foundation.Parabolic.L2Vec3) (hξ : ξ ≠ 0) : inverseFrequencyNormSq ξ * ‖ξ‖ ^ 2 = 1

theorem CKN.Leray.complexifyFrequency_apply (ξ : Foundation.Parabolic.L2Vec3) (k : Fin 3) : (complexifyFrequency ξ).ofLp k = ↑(ξ.ofLp k)

theorem CKN.Leray.inner_complexifyFrequency_left (ξ : Foundation.Parabolic.L2Vec3) (z : ComplexVec3) : inner ℂ (complexifyFrequency ξ) z = ∑ k : Fin 3, ↑(ξ.ofLp k) * z.ofLp k

theorem CKN.Leray.norm_sq_eq_sum_coord (ξ : Foundation.Parabolic.L2Vec3) : ‖ξ‖ ^ 2 = ∑ k : Fin 3, ξ.ofLp k ^ 2

theorem CKN.Leray.inner_neg_divergence_frequency (ξ : Foundation.Parabolic.L2Vec3) (F : ComplexTensor3) : inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) F)) (complexifyFrequency ξ) = 2 * ↑Real.pi * Complex.I * (starRingEnd ℂ) (inner ℂ (complexifyFrequency ξ) ((tensorDivergenceLinear ξ) F))

theorem CKN.Leray.inner_divergence_leray (ξ : Foundation.Parabolic.L2Vec3) (F : ComplexTensor3) (z : ComplexVec3) : inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) F)) ((leraySymbol ξ) z) = inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) F)) z + (starRingEnd ℂ) (pressureApplyFormula ξ F) * (2 * ↑Real.pi * Complex.I * inner ℂ (complexifyFrequency ξ) z)

The divergence source against the Leray projection of a test vector: ⟨-2πi ξ·F, ℙ̂z⟩ = ⟨-2πi ξ·F, z⟩ + conj(P̂F) · 2πi ⟨ξ, z⟩.

theorem CKN.Leray.inner_divergence_gradient (ξ : Foundation.Parabolic.L2Vec3) (F : ComplexTensor3) (c : ℂ) : inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) F)) ((2 * ↑Real.pi * Complex.I * c) • complexifyFrequency ξ) = -((starRingEnd ℂ) (pressureApplyFormula ξ F) * (-↑(forcedFourierLam ξ) * c))

The divergence source against a gradient test vector: ⟨-2πi ξ·F, 2πi c ξ⟩ = -conj(P̂F) · (-λ c).

noncomputable def CKN.Leray.quadPressureTilde (T : ↥RealTensorL2) : Foundation.Parabolic.Vec3 → ℝ

The real part of the inverse transform of the double-Riesz symbol of a real tensor field, on Vec3.

Equations

• CKN.Leray.quadPressureTilde T x = (↑↑(CKN.Leray.pressureL2Operator (CKN.Leray.complexifyTensorL2 T)) (WithLp.toLp 2 x)).re

theorem CKN.Leray.fourier_pressureL2Operator (G : ↥ComplexTensorL2) : ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ℂ) (pressureL2Operator G)) =ᵐ[MeasureTheory.volume] fun (ξ : Foundation.Parabolic.L2Vec3) => pressureApplyFormula ξ (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3) G) ξ)

theorem CKN.Leray.memLp_quadPressureTilde (T : ↥RealTensorL2) : MeasureTheory.MemLp (quadPressureTilde T) 2 MeasureTheory.volume

theorem CKN.Leray.integral_mul_quadPressureTilde (T : ↥RealTensorL2) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) : ∫ (x : Foundation.Parabolic.Vec3), χ x * quadPressureTilde T x = ∫ (ξ : Foundation.Parabolic.L2Vec3), ((starRingEnd ℂ) (pressureApplyFormula ξ (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3) (complexifyTensorL2 T)) ξ)) * FourierTransform.fourier (scalTestField χ) ξ).re

The pairing of the frequency pressure with a scalar test.

theorem CKN.Leray.integrable_fourier_integrand_scalTest {χ : Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (ξ : Foundation.Parabolic.L2Vec3) : MeasureTheory.Integrable (fun (v : Foundation.Parabolic.L2Vec3) => Real.fourierChar (-inner ℝ v ξ) • scalTestField χ v) MeasureTheory.volume

theorem CKN.Leray.fourier_scalTest_laplacian {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (ξ : Foundation.Parabolic.L2Vec3) : FourierTransform.fourier (scalTestField (spatialLaplacian ψ)) ξ = -↑(forcedFourierLam ξ) * FourierTransform.fourier (scalTestField ψ) ξ

The transform of the Laplacian of a scalar test is -λ times the transform of the test.