Physical L² extension of the regularized tensor

The regularized bilinear Schwartz tensor has a bounded extension to two complex spatial L² inputs.

noncomputable def CKN.Leray.regularisedSchwartzTensorBilinearL2Linear (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] ↥ComplexTensorL2

The L² class of the Schwartz tensor is complex bilinear in its two inputs.

Equations

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

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

The bilinear L² map evaluates to the canonical Schwartz tensor class.

theorem CKN.Leray.regularisedSchwartzTensorBilinear_L2_extension (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (F : ↥ComplexVectorL2 →L[ℂ] ↥ComplexVectorL2 →L[ℂ] ↥ComplexTensorL2), ‖F‖ ≤ C ∧ ∀ (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), (F (g.toLp 2 MeasureTheory.volume)) (f.toLp 2 MeasureTheory.volume) = (regularisedSchwartzTensorBilinear ρ ε hε g f).toLp 2 MeasureTheory.volume

A fixed L² bound selects a continuous bilinear extension of the regularized tensor on physical complex velocity fields.