Physical realization of the complete Bessel Stokes operator

The spatial realization of the complete Stokes output agrees with applying the physical Stokes operator to the spatial realization of its input.

noncomputable def CKN.Leray.physicalBesselInverseWeight (s : ℝ) (ξ : Foundation.Parabolic.L2Vec3) : ℂ

The scalar physical Fourier weight for the inverse Bessel-potential operator.

Equations

• CKN.Leray.physicalBesselInverseWeight s ξ = ↑((1 + ‖ξ‖ ^ 2) ^ (-s / 2))

theorem CKN.Leray.physicalBesselInverseWeight_memLp (s : ℝ) (hs : 0 ≤ s) : MeasureTheory.MemLp (physicalBesselInverseWeight s) ⊤ MeasureTheory.volume

noncomputable def CKN.Leray.physicalBesselInverseWeightLp (s : ℝ) (hs : 0 ≤ s) : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)

The L∞ representative of the physical inverse Bessel Fourier weight.

Equations

• CKN.Leray.physicalBesselInverseWeightLp s hs = MeasureTheory.MemLp.toLp (CKN.Leray.physicalBesselInverseWeight s) ⋯

noncomputable def CKN.Leray.physicalTensorBesselSymbol (s : ℝ) (p : Foundation.Parabolic.L2Vec3 × ComplexTensor3) : ComplexTensor3

The tensor-valued physical Bessel symbol obtained by scaling a tensor by the inverse weight.

Equations

• CKN.Leray.physicalTensorBesselSymbol s p = CKN.Leray.physicalBesselInverseWeight s p.1 • p.2

theorem CKN.Leray.physicalTensorBesselSymbol_measurable (s : ℝ) : Measurable (physicalTensorBesselSymbol s)

theorem CKN.Leray.physicalTensorBesselSymbol_norm_le (s : ℝ) (hs : 0 ≤ s) (ξ : Foundation.Parabolic.L2Vec3) (v : ComplexTensor3) : ‖physicalTensorBesselSymbol s (ξ, v)‖ ≤ ‖v‖

noncomputable def CKN.Leray.physicalTensorBesselMultiplier (s : ℝ) (hs : 0 ≤ s) (F : ↥ComplexTensorL2) : ↥ComplexTensorL2

The bounded Fourier multiplier defined by the physical tensor Bessel symbol.

Equations

• CKN.Leray.physicalTensorBesselMultiplier s hs F = CKN.Leray.measurableFourierMultiplier (CKN.Leray.physicalTensorBesselSymbol s) ⋯ 1 ⋯ F

theorem CKN.Leray.regularisedBesselStokesOperator_physical {t : ℝ} (ht : 0 < t) (k : ℕ) (F : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) : regularisedBesselSobolevToL2 ↑(2 * k) ⋯ ((regularisedBesselStokesOperator ht k) F) = stokesL2Operator ht ((regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) F)

The spatial L² realization intertwines the complete Bessel Stokes operator with the physical L² Stokes operator.