Fourier symbols for the force pressure

The force pressure symbol has order minus one. Its spatial gradient is the bounded orthogonal projection onto the frequency direction.

noncomputable def CKN.Leray.forcePressureMultiplierSymbol (ξ : Foundation.Parabolic.L2Vec3) (v : ComplexVec3) : ℂ

The order-one scalar force-pressure symbol in lem:force-pressure, defined to be zero at the origin.

Equations

• CKN.Leray.forcePressureMultiplierSymbol ξ v = if ξ = 0 then 0 else -Complex.I * inner ℂ (CKN.Leray.complexifyFrequency ξ) v / ↑(2 * Real.pi * ‖ξ‖ ^ 2)

noncomputable def CKN.Leray.forcePressureGradientSymbol (ξ : Foundation.Parabolic.L2Vec3) (v : ComplexVec3) : ComplexVec3

The frequency symbol of the spatial gradient of the force pressure.

Equations

• CKN.Leray.forcePressureGradientSymbol ξ v = if ξ = 0 then 0 else (↑(‖ξ‖ ^ 2)⁻¹ * inner ℂ (CKN.Leray.complexifyFrequency ξ) v) • CKN.Leray.complexifyFrequency ξ

theorem CKN.Leray.forcePressureGradientSymbol_measurable : Measurable fun (p : Foundation.Parabolic.L2Vec3 × ComplexVec3) => forcePressureGradientSymbol p.1 p.2

The force-pressure gradient symbol is measurable in frequency and input.

theorem CKN.Leray.forcePressureGradientSymbol_norm_le (ξ : Foundation.Parabolic.L2Vec3) (v : ComplexVec3) : ‖forcePressureGradientSymbol ξ v‖ ≤ 2 * ‖v‖

The force-pressure gradient symbol is bounded by twice the input norm.

theorem CKN.Leray.forcePressureMultiplierSymbol_spatialDeriv (ξ : Foundation.Parabolic.L2Vec3) (v : ComplexVec3) (k : Fin 3) : 2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp k) * forcePressureMultiplierSymbol ξ v = (forcePressureGradientSymbol ξ v).ofLp k

Differentiating the scalar order-one symbol gives the bounded projection onto the frequency direction.

noncomputable def CKN.Leray.forcePressureGradientFourierMultiplier (v : ↥(MeasureTheory.Lp ComplexVec3 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ComplexVec3 2 MeasureTheory.volume)

The bounded multiplier for the gradient of the force pressure on spatial complex L².

Equations

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

theorem CKN.Leray.forcePressureGradientFourierMultiplier_norm_le (v : ↥(MeasureTheory.Lp ComplexVec3 2 MeasureTheory.volume)) : ‖forcePressureGradientFourierMultiplier v‖ ≤ 2 * ‖v‖

The gradient multiplier is bounded on spatial complex L².

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

The pressure gradient in physical spatial real L², expressed as the complement of the Leray projection.

Equations

• CKN.Leray.forcePressureGradientL2 f = f - CKN.Leray.realLerayProjection f

theorem CKN.Leray.forcePressureGradientL2_norm_le (f : ↥RealVectorL2) : ‖forcePressureGradientL2 f‖ ≤ 2 * ‖f‖

The physical force-pressure gradient has the dimension-only L² bound obtained from the Leray projection.

def CKN.Leray.forcePressureCoordinateEquiv : Foundation.Parabolic.L2Vec3 ≃L[ℝ] Foundation.Parabolic.Vec3

The continuous equivalence between Hilbert velocities and coordinate triples for the force-pressure map.

Equations

• CKN.Leray.forcePressureCoordinateEquiv = PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ

def CKN.Leray.forcePressureToCoordinate : Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.Vec3

The continuous map that returns coordinate values from a Hilbert velocity.

Equations

• CKN.Leray.forcePressureToCoordinate = ↑CKN.Leray.forcePressureCoordinateEquiv

def CKN.Leray.forcePressureToHilbert : Foundation.Parabolic.Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

The continuous map that realizes a coordinate vector as a Hilbert velocity.

Equations

• CKN.Leray.forcePressureToHilbert = ↑CKN.Leray.forcePressureCoordinateEquiv.symm

noncomputable def CKN.Leray.forcePressureGradientRepresentative (f : ↥RealVectorL2) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The pointwise representative of the bounded I - ℙ force-pressure gradient multiplier on a real spatial L² class.

Equations

• CKN.Leray.forcePressureGradientRepresentative f x = CKN.Leray.forcePressureToCoordinate (↑↑f (WithLp.toLp 2 x))

theorem CKN.Leray.forcePressureInput_memLp (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.L2Vec3) => forcePressureToHilbert (f y.ofLp)) 2 MeasureTheory.volume

noncomputable def CKN.Leray.forcePressureInputL2 (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ↥RealVectorL2

The Hilbert L² class represented by a coordinate vector field with finite L² norm.

Equations

• CKN.Leray.forcePressureInputL2 f hf = MeasureTheory.MemLp.toLp (fun (y : CKN.Foundation.Parabolic.L2Vec3) => CKN.Leray.forcePressureToHilbert (f y.ofLp)) ⋯

noncomputable def CKN.Leray.forcePressureGradientFunction (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The pointwise I - ℙ force-pressure gradient applied to a coordinate field known to lie in spatial L².

Equations

• CKN.Leray.forcePressureGradientFunction f hf = CKN.Leray.forcePressureGradientRepresentative (CKN.Leray.forcePressureGradientL2 (CKN.Leray.forcePressureInputL2 f hf))

theorem CKN.Leray.forcePressureGradientFunction_memLp (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (forcePressureGradientFunction f hf) 2 MeasureTheory.volume

The pointwise representative of the force-pressure gradient is in spatial L², with the bounded multiplier estimate inherited from forcePressureGradientL2.