Real fields for Fourier multiplier operators

The Fourier symbols act on complex Euclidean component fields. These maps connect them to the real Euclidean carriers used by eq:reg-leray-symbol and lem:reg-multiplier-bounds.

@[reducible, inline]

abbrev CKN.Leray.RealTensor3 : Type

Real Euclidean tensor values on the three component indices.

Equations

• CKN.Leray.RealTensor3 = PiLp 2 fun (x : Fin 3) => CKN.Foundation.Parabolic.L2Vec3

@[reducible, inline]

noncomputable abbrev CKN.Leray.RealVectorL2 : AddSubgroup (Foundation.Parabolic.L2Vec3 →ₘ[MeasureTheory.volume] Foundation.Parabolic.L2Vec3)

Real vector-valued spatial L² on the Euclidean three-dimensional carrier.

Equations

• CKN.Leray.RealVectorL2 = MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume

@[reducible, inline]

noncomputable abbrev CKN.Leray.ComplexVectorL2 : AddSubgroup (Foundation.Parabolic.L2Vec3 →ₘ[MeasureTheory.volume] ComplexVec3)

Complex vector-valued spatial L² on the Euclidean three-dimensional carrier.

Equations

• CKN.Leray.ComplexVectorL2 = MeasureTheory.Lp CKN.Leray.ComplexVec3 2 MeasureTheory.volume

@[reducible, inline]

noncomputable abbrev CKN.Leray.RealTensorL2 : AddSubgroup (Foundation.Parabolic.L2Vec3 →ₘ[MeasureTheory.volume] RealTensor3)

Real tensor-valued spatial L² on the Euclidean three-dimensional carrier.

Equations

• CKN.Leray.RealTensorL2 = MeasureTheory.Lp CKN.Leray.RealTensor3 2 MeasureTheory.volume

@[reducible, inline]

noncomputable abbrev CKN.Leray.ComplexTensorL2 : AddSubgroup (Foundation.Parabolic.L2Vec3 →ₘ[MeasureTheory.volume] ComplexTensor3)

Complex tensor-valued spatial L² on the Euclidean three-dimensional carrier.

Equations

• CKN.Leray.ComplexTensorL2 = MeasureTheory.Lp CKN.Leray.ComplexTensor3 2 MeasureTheory.volume

def CKN.Leray.complexifyValueLinear : Foundation.Parabolic.L2Vec3 →ₗ[ℝ] ComplexVec3

The coordinate embedding of a real Euclidean vector into its complexification.

Equations

• CKN.Leray.complexifyValueLinear = { toFun := CKN.Leray.complexifyFrequency, map_add' := ⋯, map_smul' := ⋯ }

theorem CKN.Leray.complexifyValue_norm (x : Foundation.Parabolic.L2Vec3) : ‖complexifyValueLinear x‖ = ‖x‖

noncomputable def CKN.Leray.complexifyValue : Foundation.Parabolic.L2Vec3 →L[ℝ] ComplexVec3

The norm-preserving real-linear embedding of real Euclidean vectors into complex vectors.

Equations

• CKN.Leray.complexifyValue = CKN.Leray.complexifyValueLinear.mkContinuous 1 CKN.Leray.complexifyValue._proof_1

def CKN.Leray.realPartValueLinear : ComplexVec3 →ₗ[ℝ] Foundation.Parabolic.L2Vec3

Coordinatewise real part as a real-linear contraction on Euclidean vectors.

Equations

• CKN.Leray.realPartValueLinear = { toFun := fun (z : CKN.Leray.ComplexVec3) => WithLp.toLp 2 fun (i : Fin 3) => (z.ofLp i).re, map_add' := ⋯, map_smul' := ⋯ }

theorem CKN.Leray.realPartValue_norm_le (z : ComplexVec3) : ‖realPartValueLinear z‖ ≤ ‖z‖

noncomputable def CKN.Leray.realPartValue : ComplexVec3 →L[ℝ] Foundation.Parabolic.L2Vec3

The coordinatewise real-part map on Euclidean vectors.

Equations

• CKN.Leray.realPartValue = CKN.Leray.realPartValueLinear.mkContinuous 1 CKN.Leray.realPartValue._proof_1

noncomputable def CKN.Leray.complexifyVectorL2 : ↥RealVectorL2 →L[ℝ] ↥ComplexVectorL2

Complexification of a real vector-valued spatial L² field.

Equations

• CKN.Leray.complexifyVectorL2 = ContinuousLinearMap.compLpL 2 MeasureTheory.volume CKN.Leray.complexifyValue

noncomputable def CKN.Leray.realPartVectorL2 : ↥ComplexVectorL2 →L[ℝ] ↥RealVectorL2

Taking real parts of a complex vector-valued spatial L² field.

Equations

• CKN.Leray.realPartVectorL2 = ContinuousLinearMap.compLpL 2 MeasureTheory.volume CKN.Leray.realPartValue

theorem CKN.Leray.complexifyVectorL2_norm_le (f : ↥RealVectorL2) : ‖complexifyVectorL2 f‖ ≤ ‖f‖

theorem CKN.Leray.realPartVectorL2_norm_le (f : ↥ComplexVectorL2) : ‖realPartVectorL2 f‖ ≤ ‖f‖

def CKN.Leray.complexifyTensorLinear : RealTensor3 →ₗ[ℝ] ComplexTensor3

The coordinatewise complexification used by lem:reg-multiplier-bounds.

Equations

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

theorem CKN.Leray.complexifyTensor_norm (F : RealTensor3) : ‖complexifyTensorLinear F‖ = ‖F‖

noncomputable def CKN.Leray.complexifyTensorValue : RealTensor3 →L[ℝ] ComplexTensor3

The continuous tensor complexification used by lem:reg-multiplier-bounds.

Equations

• CKN.Leray.complexifyTensorValue = CKN.Leray.complexifyTensorLinear.mkContinuous 1 CKN.Leray.complexifyTensorValue._proof_1

noncomputable def CKN.Leray.complexifyTensorL2 : ↥RealTensorL2 →L[ℝ] ↥ComplexTensorL2

Complexification of a real tensor-valued spatial L² field.

Equations

• CKN.Leray.complexifyTensorL2 = ContinuousLinearMap.compLpL 2 MeasureTheory.volume CKN.Leray.complexifyTensorValue

theorem CKN.Leray.complexifyTensorL2_norm_le (F : ↥RealTensorL2) : ‖complexifyTensorL2 F‖ ≤ ‖F‖

noncomputable def CKN.Leray.realHeatOperator (t : ℝ) (ht : 0 ≤ t) : ↥RealVectorL2 → ↥RealVectorL2

The real heat multiplier operator, defined by complexification and real part.

Equations

• CKN.Leray.realHeatOperator t ht f = CKN.Leray.realPartVectorL2 (CKN.Leray.heatSemigroup t ht (CKN.Leray.complexifyVectorL2 f))

theorem CKN.Leray.realHeatOperator_norm_le (t : ℝ) (ht : 0 ≤ t) (f : ↥RealVectorL2) : ‖realHeatOperator t ht f‖ ≤ ‖f‖

The real heat operator is an L² contraction, as in lem:reg-multiplier-bounds.

noncomputable def CKN.Leray.realLerayProjection (f : ↥RealVectorL2) : ↥RealVectorL2

The real Leray projection, defined by complexification and real part.

Equations

• CKN.Leray.realLerayProjection f = CKN.Leray.realPartVectorL2 (CKN.Leray.lerayProjectionL2 (CKN.Leray.complexifyVectorL2 f))

theorem CKN.Leray.realLerayProjection_norm_le (f : ↥RealVectorL2) : ‖realLerayProjection f‖ ≤ ‖f‖

The real Leray projection is an L² contraction, as in lem:reg-multiplier-bounds.

noncomputable def CKN.Leray.realStokesOperator {t : ℝ} (ht : 0 < t) : ↥RealTensorL2 → ↥RealVectorL2

The real Stokes operator, defined by complexification and real part.

Equations

• CKN.Leray.realStokesOperator ht F = CKN.Leray.realPartVectorL2 (CKN.Leray.stokesL2Operator ht (CKN.Leray.complexifyTensorL2 F))

theorem CKN.Leray.realStokesOperator_norm_le {t : ℝ} (ht : 0 < t) (F : ↥RealTensorL2) : ‖realStokesOperator ht F‖ ≤ 1 / √(2 * Real.exp 1 * t) * ‖F‖

The real Stokes operator has the Fourier multiplier bound of lem:reg-multiplier-bounds.