JSpace Fourier Potential Base

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.weakFieldFourierComponent {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (i : Fin 3) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

One complex Fourier-space coordinate of an L² vector field.

Equations

• CKN.weakFieldFourierComponent ha i = MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.L2Vec3) => (CKN.complexifyVec3 a x).ofLp i) ⋯

noncomputable def CKN.regularizedPotentialComponentLp {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The regularized potential coordinate as a complex L² function.

Equations

• CKN.regularizedPotentialComponentLp ha δ hδ i = CKN.regularizedPotentialL2Component δ hδ i fun (j : Fin 3) => FourierTransform.fourier (CKN.weakFieldFourierComponent ha j)

noncomputable def CKN.regularizedPotentialVec3 {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The real vector field represented by the regularized potential.

Equations

• CKN.regularizedPotentialVec3 ha δ hδ x i = (↑↑(CKN.regularizedPotentialComponentLp ha δ hδ i) (WithLp.toLp 2 x)).re

noncomputable def CKN.regularizedPotentialDerivativeComponentLp {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (_hδ : 0 < δ) (i k : Fin 3) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

A first derivative of a coordinate of the regularized vector potential, represented as a complex L² function on the native Euclidean carrier.

Equations

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

noncomputable def CKN.regularizedPotentialGradientVec3 {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ

The real first derivatives of the regularized potential.

Equations

• CKN.regularizedPotentialGradientVec3 ha δ hδ x i k = (↑↑(CKN.regularizedPotentialDerivativeComponentLp ha δ hδ i k) (WithLp.toLp 2 x)).re

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

The coordinatewise equivalence between the native vector carrier and L² Pi space.

Equations

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

noncomputable def CKN.l2SpatialDeriv (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ℝ) (i : Fin 3) : Foundation.Parabolic.L2Vec3 → ℝ

A coordinate directional derivative on the L² Pi carrier.

Equations

• CKN.l2SpatialDeriv ψ i x = (fderiv ℝ (⇑ψ) x) (CKN.l2Vec3Equiv.symm (CKN.basisVec i))

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

The coordinate basis vector in the L² Pi carrier.

Equations

• CKN.l2BasisVec3 i = WithLp.toLp 2 (Pi.single i 1)

theorem CKN.l2Vec3Equiv_symm_basisVec (i : Fin 3) : l2Vec3Equiv.symm (basisVec i) = l2BasisVec3 i

The coordinate equivalence sends each native basis vector to its Pi representative.

theorem CKN.inner_l2BasisVec3 (ξ : Foundation.Parabolic.L2Vec3) (i : Fin 3) : inner ℝ ξ (l2BasisVec3 i) = (frequencyL2Coord i) ξ

The Pi inner product with a coordinate basis vector is the corresponding coordinate.

theorem CKN.regularizedPotentialVec3_hasWeakPartialDerivOn {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (i k : Fin 3) (hdist : MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialDerivativeComponentLp ha δ hδ i k) = LineDeriv.lineDerivOp (l2BasisVec3 k) (MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialComponentLp ha δ hδ i))) : HasWeakPartialDerivOn Set.univ k (fun (x : Vec 3) => regularizedPotentialVec3 ha δ hδ x i) fun (x : Vec 3) => regularizedPotentialGradientVec3 ha δ hδ x i k

The regularized potential has distributional derivatives represented by its Fourier derivatives.

def CKN.curlOfGradient (G : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The coordinate curl formed from a represented weak gradient.

Equations

• CKN.curlOfGradient G x i = if i = 0 then G x 2 1 - G x 1 2 else if i = 1 then G x 0 2 - G x 2 0 else G x 1 0 - G x 0 1

theorem CKN.curlOfGradient_memLp {G : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ} (hG : ∀ (i k : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => G x i k) 2 MeasureTheory.volume) : MeasureTheory.MemLp (curlOfGradient G) 2 MeasureTheory.volume

An L² matrix field has an L² coordinate curl.

theorem CKN.curl_spatialMollify_eq_spatialMollify_curlOfGradient {A : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {G : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ} (hA : MeasureTheory.MemLp A 2 MeasureTheory.volume) (hG : MeasureTheory.MemLp G 2 MeasureTheory.volume) (hweak : ∀ (i k : Fin 3), HasWeakPartialDerivOn Set.univ k (fun (x : Vec 3) => A x i) fun (x : Vec 3) => G x i k) {ε : ℝ} (hε : 0 < ε) (x : Foundation.Parabolic.Vec3) : curlVec3 (spatialMollifyVec3 A ε hε) x = spatialMollifyVec3 (curlOfGradient G) ε hε x

Spatial mollification commutes with the curl of a represented weak gradient.

theorem CKN.regularizedPotentialDerivativeComponentLp_toDist_zero {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (k : Fin 3) : MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialDerivativeComponentLp ha δ hδ 0 k) = (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ k 1)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 2)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ k 2)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 1))

Distributional formula for the first coordinate of the regularized potential derivative.

theorem CKN.regularizedPotentialDerivativeComponentLp_toDist_one {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (k : Fin 3) : MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialDerivativeComponentLp ha δ hδ 1 k) = (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ k 2)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 0)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ k 0)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 2))

Distributional formula for the second coordinate of the regularized potential derivative.

theorem CKN.regularizedPotentialDerivativeComponentLp_toDist_two {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (k : Fin 3) : MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialDerivativeComponentLp ha δ hδ 2 k) = (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ k 0)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 1)) - (TemperedDistribution.fourierMultiplierCLM ℂ (regularizedDerivativeEntry δ k 1)) (MeasureTheory.Lp.toTemperedDistribution (weakFieldFourierComponent ha 0))

Distributional formula for the third coordinate of the regularized potential derivative.

theorem CKN.regularizedPotentialComponentLp_is_weakDeriv {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) (i k : Fin 3) : MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialDerivativeComponentLp ha δ hδ i k) = LineDeriv.lineDerivOp (l2BasisVec3 k) (MeasureTheory.Lp.toTemperedDistribution (regularizedPotentialComponentLp ha δ hδ i))

The regularized potential derivatives are its distributional first derivatives.