The force-pressure gradient is orthogonal to divergence-free fields

By Plancherel and the self-adjointness of the frequency projection, the Leray projection fixes the pairing with every weakly divergence-free field. Hence the field (I - ℙ) f of lem:force-pressure is L²-orthogonal to all weakly divergence-free fields.

theorem CKN.Leray.inner_realPartVectorL2_eq_re (Z : ↥ComplexVectorL2) (w : ↥RealVectorL2) : inner ℝ (realPartVectorL2 Z) w = (inner ℂ Z (complexifyVectorL2 w)).re

The real pairing of a real part is the real part of the complex pairing with the complexification.

theorem CKN.Leray.inner_complexifyVectorL2_re (v w : ↥RealVectorL2) : (inner ℂ (complexifyVectorL2 v) (complexifyVectorL2 w)).re = inner ℝ v w

Complexification preserves the real L² pairing.

theorem CKN.Leray.inner_lerayProjectionL2_of_fourierOrthogonal (Z W : ↥ComplexVectorL2) (hW : ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), inner ℂ (complexifyFrequency ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) W) ξ) = 0) : inner ℂ (lerayProjectionL2 Z) W = inner ℂ Z W

The Leray projection does not change the pairing with a field whose Fourier transform is orthogonal to the frequency almost everywhere.

theorem CKN.Leray.realLerayProjection_inner_of_isWeakDivFree (v w : ↥RealVectorL2) (hw : IsWeakDivFreeL2 (realVectorL2Representative w)) : inner ℝ (realLerayProjection v) w = inner ℝ v w

The real Leray projection fixes the pairing with every field whose representative is weakly divergence-free.

theorem CKN.Leray.forcePressureGradientL2_inner_eq_zero (v w : ↥RealVectorL2) (hw : IsWeakDivFreeL2 (realVectorL2Representative w)) : inner ℝ (forcePressureGradientL2 v) w = 0

The force-pressure gradient field (I - ℙ) f of lem:force-pressure is L²-orthogonal to every weakly divergence-free field.