Complex conjugation and the spatial Fourier transform

Coordinatewise complex conjugation of vector and tensor fields intertwines the L² Fourier transform with the reflected conjugation ĝ ↦ conj ĝ(-·). This symmetry keeps the Fourier-side solution of the regularized mild equation eq:reg-mild real-valued, which the energy equality of thm:regularised uses.

def CKN.Leray.complexVecConj : ComplexVec3 ≃ₗᵢ[ℝ] ComplexVec3

Coordinatewise complex conjugation of complex Euclidean vectors.

Equations

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

theorem CKN.Leray.complexVecConj_apply (z : ComplexVec3) (i : Fin 3) : (complexVecConj z).ofLp i = (starRingEnd ((fun (x : Fin 3) => ℂ) i)) (z.ofLp i)

theorem CKN.Leray.complexVecConj_involutive (z : ComplexVec3) : complexVecConj (complexVecConj z) = z

def CKN.Leray.complexTensorConj : ComplexTensor3 ≃ₗᵢ[ℝ] ComplexTensor3

Coordinatewise complex conjugation of complex Euclidean tensors.

Equations

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

theorem CKN.Leray.complexTensorConj_apply (T : ComplexTensor3) (i : Fin 3) : (complexTensorConj T).ofLp i = complexVecConj (T.ofLp i)

theorem CKN.Leray.complexVecConj_smul (c : ℂ) (z : ComplexVec3) : complexVecConj (c • z) = (starRingEnd ℂ) c • complexVecConj z

theorem CKN.Leray.complexTensorConj_smul (c : ℂ) (T : ComplexTensor3) : complexTensorConj (c • T) = (starRingEnd ℂ) c • complexTensorConj T

theorem CKN.Leray.fourier_comp_conj_apply {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (σ : F ≃ₗᵢ[ℝ] F) (hσ : ∀ (c : ℂ) (x : F), σ (c • x) = (starRingEnd ℂ) c • σ x) (f : Foundation.Parabolic.L2Vec3 → F) (w : Foundation.Parabolic.L2Vec3) : FourierTransform.fourier (fun (v : Foundation.Parabolic.L2Vec3) => σ (f v)) w = σ (FourierTransform.fourier f (-w))

The Fourier integral of a conjugated function is the conjugate of the Fourier integral at the reflected frequency.

noncomputable def CKN.Leray.reflectLp (F : Type u_1) [NormedAddCommGroup F] [InnerProductSpace ℂ F] : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)

Reflection ξ ↦ -ξ of the spatial variable, on L².

Equations

• CKN.Leray.reflectLp F = (MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => -ξ) CKN.Leray.reflectLp._proof_5).toContinuousLinearMap

noncomputable def CKN.Leray.conjLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (σ : F ≃ₗᵢ[ℝ] F) : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)

Pointwise application of a real-linear isometry, on L².

Equations

• CKN.Leray.conjLp σ = ContinuousLinearMap.compLpL 2 MeasureTheory.volume ↑↑σ

noncomputable def CKN.Leray.conjReflectLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (σ : F ≃ₗᵢ[ℝ] F) : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)

The reflected conjugation g ↦ σ(g(-·)) on L².

Equations

• CKN.Leray.conjReflectLp σ = CKN.Leray.reflectLp F ∘SL CKN.Leray.conjLp σ

theorem CKN.Leray.conjLp_ae {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (σ : F ≃ₗᵢ[ℝ] F) (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) : ↑↑((conjLp σ) f) =ᵐ[MeasureTheory.volume] fun (ξ : Foundation.Parabolic.L2Vec3) => σ (↑↑f ξ)

theorem CKN.Leray.conjReflectLp_ae {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (σ : F ≃ₗᵢ[ℝ] F) (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) : ↑↑((conjReflectLp σ) f) =ᵐ[MeasureTheory.volume] fun (ξ : Foundation.Parabolic.L2Vec3) => σ (↑↑f (-ξ))

theorem CKN.Leray.conjReflectLp_conjReflectLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (σ : F ≃ₗᵢ[ℝ] F) (hσσ : ∀ (x : F), σ (σ x) = x) (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) : (conjReflectLp σ) ((conjReflectLp σ) f) = f

The reflected conjugation is an involution.

noncomputable def CKN.Leray.conjReflectEquiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (σ : F ≃ₗᵢ[ℝ] F) (hσσ : ∀ (x : F), σ (σ x) = x) : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ≃L[ℝ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)

The reflected conjugation as a continuous real-linear involution.

Equations

• CKN.Leray.conjReflectEquiv σ hσσ = ContinuousLinearEquiv.equivOfInverse (CKN.Leray.conjReflectLp σ) (CKN.Leray.conjReflectLp σ) ⋯ ⋯

theorem CKN.Leray.conjReflectEquiv_apply {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] (σ : F ≃ₗᵢ[ℝ] F) (hσσ : ∀ (x : F), σ (σ x) = x) (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) : (conjReflectEquiv σ hσσ) f = (conjReflectLp σ) f

theorem CKN.Leray.fourierTransform_conjLp {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (σ : F ≃ₗᵢ[ℝ] F) (hσ : ∀ (c : ℂ) (x : F), σ (c • x) = (starRingEnd ℂ) c • σ x) (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) : (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 F) ((conjLp σ) f) = (conjReflectLp σ) ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 F) f)

The L² Fourier transform of a conjugated field is the reflected conjugate of its Fourier transform.

theorem CKN.Leray.conjLp_fourierTransform_symm {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (σ : F ≃ₗᵢ[ℝ] F) (hσ : ∀ (c : ℂ) (x : F), σ (c • x) = (starRingEnd ℂ) c • σ x) (g : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)) : (conjLp σ) ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 F).symm g) = (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 F).symm ((conjReflectLp σ) g)

The inverse L² Fourier transform of a reflected conjugate is the conjugate of the inverse transform.