The regularized bilinear tensor in even Bessel norms

On complex Schwartz data, the complete H²ᵏ norm of the regularized bilinear tensor (J_ε g) ⊗ f is bounded by a fixed constant times the L² norm of g and the complete H²ᵏ norm of f. The mollified factor absorbs every derivative in the uniform norm, so no derivative of g enters the estimate.

theorem CKN.Leray.regularisedSchwartzTensorBilinear_bessel_even_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), ‖⋯.toBesselPotentialSpace‖ ≤ C * ‖g.toLp 2 MeasureTheory.volume‖ * ‖regularisedBesselOfSchwartz (↑(2 * k)) f‖

The regularized bilinear Schwartz tensor is bounded from L² × H²ᵏ into the complete Bessel space H²ᵏ, with a constant depending only on the mollifier, the regularization scale and k.