Physical weak divergence of Fourier multiplier ranges

The frequency orthogonality in lem:reg-multiplier-bounds implies the physical weak-divergence identity by Plancherel.

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

The canonical continuous linear equivalence between coordinate triples and the Hilbert L² vector.

Equations

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

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

The coordinate representative on Vec3 of a real spatial L² field.

Equations

• CKN.Leray.realVectorL2Representative f x = CKN.Leray.l2Vec3Equiv (↑↑f (WithLp.toLp 2 x))

def CKN.Leray.l2BasisVec (i : Fin 3) : Foundation.Parabolic.L2Vec3

The Hilbert-space representative of the ith standard basis vector.

Equations

• CKN.Leray.l2BasisVec i = WithLp.toLp 2 (CKN.basisVec i)

def CKN.Leray.gradientOfCovectorLinear : (Foundation.Parabolic.L2Vec3 →L[ℝ] ℂ) →ₗ[ℂ] ComplexVec3

The complex-linear gradient vector associated to a continuous linear covector on Hilbert vectors.

Equations

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

theorem CKN.Leray.gradientOfCovectorLinear_norm_bound (D : Foundation.Parabolic.L2Vec3 →L[ℝ] ℂ) : ‖gradientOfCovectorLinear D‖ ≤ 2 * ‖D‖

noncomputable def CKN.Leray.gradientOfCovector : (Foundation.Parabolic.L2Vec3 →L[ℝ] ℂ) →L[ℂ] ComplexVec3

The bounded gradient vector associated to a continuous linear covector.

Equations

• CKN.Leray.gradientOfCovector = CKN.Leray.gradientOfCovectorLinear.mkContinuous 2 CKN.Leray.gradientOfCovector._proof_1

theorem CKN.Leray.fourier_postcompCLM {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G] (L : F →L[ℂ] G) (f : SchwartzMap Foundation.Parabolic.L2Vec3 F) : FourierTransform.fourier ((SchwartzMap.postcompCLM L) f) = (SchwartzMap.postcompCLM L) (FourierTransform.fourier f)

The Fourier transform commutes with bounded complex linear postcomposition.

noncomputable def CKN.Leray.weakTestSourceSchwartz (ψ : WeakTestFunction Set.univ) : SchwartzMap Foundation.Parabolic.Vec3 ℝ

The Schwartz representative of a compactly supported smooth weak test function.

Equations

• CKN.Leray.weakTestSourceSchwartz ψ = ⋯.toSchwartzMap ⋯

noncomputable def CKN.Leray.weakTestSchwartz {ψ : WeakTestFunction Set.univ} : SchwartzMap Foundation.Parabolic.L2Vec3 ℝ

The Schwartz-map encoding of a scalar weak test function.

Equations

• CKN.Leray.weakTestSchwartz = (SchwartzMap.compCLMOfContinuousLinearEquiv ℝ CKN.Leray.l2Vec3Equiv) (CKN.Leray.weakTestSourceSchwartz ψ)

noncomputable def CKN.Leray.weakTestComplexSchwartz {ψ : WeakTestFunction Set.univ} : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ

The complex-valued Schwartz encoding of a scalar weak test function on the Hilbert coordinates.

Equations

• CKN.Leray.weakTestComplexSchwartz = (SchwartzMap.postcompCLM Complex.ofRealCLM) CKN.Leray.weakTestSchwartz

noncomputable def CKN.Leray.weakTestGradientSchwartz (ψ : WeakTestFunction Set.univ) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3

The Schwartz encoding of the gradient of a weak test function.

Equations

• CKN.Leray.weakTestGradientSchwartz ψ = (SchwartzMap.postcompCLM CKN.Leray.gradientOfCovector) ((SchwartzMap.fderivCLM ℂ CKN.Foundation.Parabolic.L2Vec3 ℂ) CKN.Leray.weakTestComplexSchwartz)

noncomputable def CKN.Leray.realPartVectorL2Representative (v : ↥ComplexVectorL2) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The real coordinate representative of a complex Euclidean L² field, used for the weak-divergence conclusion in lem:reg-multiplier-bounds.

Equations

• CKN.Leray.realPartVectorL2Representative v x = CKN.Leray.l2Vec3Equiv (CKN.Leray.realPartValue (↑↑v (WithLp.toLp 2 x)))

theorem CKN.Leray.realPart_isWeakDivFree_of_fourierOrthogonal (v : ↥ComplexVectorL2) (hv : ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), inner ℂ (complexifyFrequency ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) v) ξ) = 0) : IsWeakDivFreeL2 (realPartVectorL2Representative v)

A complex L² field whose Fourier transform is orthogonal to frequency has real part with zero physical weak divergence, as in lem:reg-multiplier-bounds.

theorem CKN.Leray.isWeakDivFree_congr_ae {a b : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hab : a =ᵐ[MeasureTheory.volume] b) (ha : IsWeakDivFreeL2 a) : IsWeakDivFreeL2 b

Weak divergence freedom is invariant under almost everywhere equality.

theorem CKN.Leray.realPartVectorL2Representative_eq_ae (z : ↥ComplexVectorL2) : realVectorL2Representative (realPartVectorL2 z) =ᵐ[MeasureTheory.volume] realPartVectorL2Representative z

The representative of the real part agrees almost everywhere with the real part of the complex representative.

theorem CKN.Leray.realLerayProjectionRepresentative_isWeakDivFree (f : ↥RealVectorL2) : IsWeakDivFreeL2 (realPartVectorL2Representative (lerayProjectionL2 (complexifyVectorL2 f)))

The physical Leray projection has weakly divergence-free real range, the physical-space assertion in lem:reg-multiplier-bounds.

theorem CKN.Leray.realLerayProjection_isWeakDivFree (f : ↥RealVectorL2) : IsWeakDivFreeL2 (realVectorL2Representative (realLerayProjection f))

The representative of realLerayProjection is weakly divergence-free in physical space, as asserted in lem:reg-multiplier-bounds.

theorem CKN.Leray.realStokesOperatorRepresentative_isWeakDivFree {t : ℝ} (ht : 0 < t) (F : ↥RealTensorL2) : IsWeakDivFreeL2 (realPartVectorL2Representative (stokesL2Operator ht (complexifyTensorL2 F)))

The physical Stokes operator has weakly divergence-free real range, the physical-space assertion in lem:reg-multiplier-bounds.

theorem CKN.Leray.realStokesOperator_isWeakDivFree {t : ℝ} (ht : 0 < t) (F : ↥RealTensorL2) : IsWeakDivFreeL2 (realVectorL2Representative (realStokesOperator ht F))

The representative of realStokesOperator is weakly divergence-free in physical space, as asserted in lem:reg-multiplier-bounds.