Real-valuedness of the Fourier solution of the mild equation

The heat, Leray and Stokes symbols commute with the reflected conjugation ĝ ↦ conj ĝ(-·), and so does the frequency-side right-hand side of the mild equation eq:reg-mild-forced whenever its data are Fourier transforms of real fields. Consequently the complex solution curve is the complexification of its real part, and the inverse transform of its frequency gradient is real. These are the facts behind the exact energy equality of thm:regularised.

theorem CKN.Leray.complexVecConj_complexifyValue (y : Foundation.Parabolic.L2Vec3) : complexVecConj (complexifyValue y) = complexifyValue y

theorem CKN.Leray.complexTensorConj_complexifyTensorValue (y : RealTensor3) : complexTensorConj (complexifyTensorValue y) = complexifyTensorValue y

theorem CKN.Leray.conjLp_complexifyVectorL2 (x : ↥RealVectorL2) : (conjLp complexVecConj) (complexifyVectorL2 x) = complexifyVectorL2 x

theorem CKN.Leray.conjLp_complexifyTensorL2 (x : ↥RealTensorL2) : (conjLp complexTensorConj) (complexifyTensorL2 x) = complexifyTensorL2 x

theorem CKN.Leray.conjReflectLp_fourier_complexifyVectorL2 (x : ↥RealVectorL2) : (conjReflectLp complexVecConj) ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 x)) = (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 x)

The Fourier transform of a real vector field is invariant under the reflected conjugation.

theorem CKN.Leray.conjReflectLp_fourier_complexifyTensorL2 (x : ↥RealTensorL2) : (conjReflectLp complexTensorConj) ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3) (complexifyTensorL2 x)) = (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3) (complexifyTensorL2 x)

The Fourier transform of a real tensor field is invariant under the reflected conjugation.

theorem CKN.Leray.conjReflectLp_heatMultiplier_smul (t : ℝ) (ht : 0 ≤ t) (g : ↥ComplexVectorL2) : (conjReflectLp complexVecConj) (heatMultiplier t ht • g) = heatMultiplier t ht • (conjReflectLp complexVecConj) g

The heat multiplier commutes with the reflected conjugation.

theorem CKN.Leray.conjReflectLp_measurableFourierMultiplier {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [MeasurableSpace F] [BorelSpace F] [NormedAddCommGroup G] [InnerProductSpace ℂ G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (σF : F ≃ₗᵢ[ℝ] F) (σG : G ≃ₗᵢ[ℝ] G) (m : Foundation.Parabolic.L2Vec3 × F → G) (hm : Measurable m) (C : ℝ) (hbound : ∀ (ξ : Foundation.Parabolic.L2Vec3) (x : F), ‖m (ξ, x)‖ ≤ C * ‖x‖) (hsym : ∀ (ξ : Foundation.Parabolic.L2Vec3) (x : F), σG (m (-ξ, x)) = m (ξ, σF x)) (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) : (conjReflectLp σG) (measurableFourierMultiplier m hm C hbound f) = measurableFourierMultiplier m hm C hbound ((conjReflectLp σF) f)

A measurable Fourier multiplier whose symbol is symmetric under the reflected conjugation commutes with it.

theorem CKN.Leray.tensorDivergenceLinear_neg_freq (ξ : Foundation.Parabolic.L2Vec3) (T : ComplexTensor3) : (tensorDivergenceLinear (-ξ)) T = -(tensorDivergenceLinear ξ) T

theorem CKN.Leray.complexVecConj_tensorDivergenceLinear (ξ : Foundation.Parabolic.L2Vec3) (T : ComplexTensor3) : complexVecConj ((tensorDivergenceLinear ξ) T) = (tensorDivergenceLinear ξ) (complexTensorConj T)

theorem CKN.Leray.lerayApplyFormula_neg_freq (ξ : Foundation.Parabolic.L2Vec3) (z : ComplexVec3) : lerayApplyFormula (-ξ) z = lerayApplyFormula ξ z

theorem CKN.Leray.complexVecConj_lerayApplyFormula (ξ : Foundation.Parabolic.L2Vec3) (z : ComplexVec3) : complexVecConj (lerayApplyFormula ξ z) = lerayApplyFormula ξ (complexVecConj z)

theorem CKN.Leray.lerayApplyFormula_neg (ξ : Foundation.Parabolic.L2Vec3) (z : ComplexVec3) : lerayApplyFormula ξ (-z) = -lerayApplyFormula ξ z

theorem CKN.Leray.complexVecConj_stokesApplyFormula (t : ℝ) (ξ : Foundation.Parabolic.L2Vec3) (T : ComplexTensor3) : complexVecConj (stokesApplyFormula t (-ξ) T) = stokesApplyFormula t ξ (complexTensorConj T)

theorem CKN.Leray.conjReflectLp_stokesFourierMultiplier {t : ℝ} (ht : 0 < t) (g : ↥ComplexTensorL2) : (conjReflectLp complexVecConj) (stokesFourierMultiplier ht g) = stokesFourierMultiplier ht ((conjReflectLp complexTensorConj) g)

The Stokes multiplier commutes with the reflected conjugation.

theorem CKN.Leray.conjReflectLp_lerayFourierMultiplier (g : ↥ComplexVectorL2) : (conjReflectLp complexVecConj) (lerayFourierMultiplier g) = lerayFourierMultiplier ((conjReflectLp complexVecConj) g)

The Leray multiplier commutes with the reflected conjugation.

theorem CKN.Leray.conjReflectLp_forcedFourierMild (b : ↥ComplexVectorL2) (hb : (conjReflectLp complexVecConj) b = b) (F : ℝ → ↥ComplexTensorL2) (hF : ∀ (s : ℝ), (conjReflectLp complexTensorConj) (F s) = F s) (H : ℝ → ↥ComplexVectorL2) (hH : ∀ (s : ℝ), (conjReflectLp complexVecConj) (H s) = H s) (t : ℝ) (ht : 0 ≤ t) : (conjReflectLp complexVecConj) (forcedFourierMild b F H t ht) = forcedFourierMild b F H t ht

The frequency-side right-hand side of eq:reg-mild-forced is invariant under the reflected conjugation when its data are.

theorem CKN.Leray.conjLp_forcedComplexCurve (b : ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) (h : ℝ → ↥RealVectorL2) (s : ℝ) : (conjLp complexVecConj) (forcedComplexCurve b F h s) = forcedComplexCurve b F h s

The complex solution curve of the forced mild equation is invariant under coordinatewise conjugation.

theorem CKN.Leray.complexifyVectorL2_realPartVectorL2_of_conj (w : ↥ComplexVectorL2) (hw : (conjLp complexVecConj) w = w) : complexifyVectorL2 (realPartVectorL2 w) = w

A complex field fixed by coordinatewise conjugation is the complexification of its real part.

theorem CKN.Leray.forcedComplexCurve_eq_complexify (b : ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) (h : ℝ → ↥RealVectorL2) (s : ℝ) : forcedComplexCurve b F h s = complexifyVectorL2 (realPartVectorL2 (forcedComplexCurve b F h s))

The complex solution curve of the forced mild equation is the complexification of its real part.

theorem CKN.Leray.conjLp_forcedFourierGrad (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (hreal : (conjReflectLp complexVecConj) ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) = (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) : (conjLp complexTensorConj) (forcedFourierGrad v hv) = forcedFourierGrad v hv

The inverse transform of the frequency gradient of a field with conjugation-symmetric transform is fixed by coordinatewise conjugation.