The bounded physical regularized tensor map

The Schwartz bilinear estimate selects a continuous tensor map on two complex spatial L² fields.

noncomputable def CKN.Leray.regularisedTensorPhysicalConstant (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ℝ

A finite nonnegative bound for the complex physical tensor map.

Equations

• CKN.Leray.regularisedTensorPhysicalConstant ρ ε hε = Classical.choose ⋯

noncomputable def CKN.Leray.regularisedTensorPhysicalMap (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ↥ComplexVectorL2 →L[ℂ] ↥ComplexVectorL2 →L[ℂ] ↥ComplexTensorL2

The bounded complex bilinear regularized tensor on physical L² data.

Equations

• CKN.Leray.regularisedTensorPhysicalMap ρ ε hε = Classical.choose ⋯

theorem CKN.Leray.regularisedTensorPhysicalMap_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : 0 ≤ regularisedTensorPhysicalConstant ρ ε hε ∧ ‖regularisedTensorPhysicalMap ρ ε hε‖ ≤ regularisedTensorPhysicalConstant ρ ε hε

The chosen physical tensor map has its uniform operator bound.

theorem CKN.Leray.regularisedTensorPhysicalMap_schwartz (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : ((regularisedTensorPhysicalMap ρ ε hε) (g.toLp 2 MeasureTheory.volume)) (f.toLp 2 MeasureTheory.volume) = (regularisedSchwartzTensorBilinear ρ ε hε g f).toLp 2 MeasureTheory.volume

On Schwartz data, the physical tensor map equals the original regularized Schwartz tensor L² class.