The quadratic regularized tensor on complete Sobolev data

The bounded bilinear map and the continuous physical L² realization give a locally Lipschitz quadratic nonlinearity in H²ᵏ.

noncomputable def CKN.Leray.regularisedBesselTensorQuadratic (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (u : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2

The complete Sobolev tensor formed from one Sobolev velocity and its underlying spatial L² field.

Equations

• CKN.Leray.regularisedBesselTensorQuadratic ρ ε hε k u = ((CKN.Leray.regularisedBesselTensorMap ρ ε hε k) ((CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) u)) u

theorem CKN.Leray.regularisedBesselTensorQuadratic_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (u : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : ‖regularisedBesselTensorQuadratic ρ ε hε k u‖ ≤ regularisedBesselTensorConstant ρ ε hε k * ‖u‖ ^ 2

The quadratic tensor grows at most quadratically in the complete H²ᵏ norm.

theorem CKN.Leray.regularisedBesselTensorQuadratic_difference_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (u v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : ‖regularisedBesselTensorQuadratic ρ ε hε k u - regularisedBesselTensorQuadratic ρ ε hε k v‖ ≤ regularisedBesselTensorConstant ρ ε hε k * ‖u - v‖ * (‖u‖ + ‖v‖)

The quadratic tensor is locally Lipschitz in the complete H²ᵏ norm, with the two factors displayed separately.