Pointwise bilinear tensor bound

The mollifier L²-to-pointwise estimate controls the rank-one tensor at each spatial point before taking its L² norm.

theorem CKN.Leray.regularisedSchwartzTensorBilinear_pointwise_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3), ‖(regularisedSchwartzTensorBilinear ρ ε hε g f) x‖ ≤ C * ‖g.toLp 2 MeasureTheory.volume‖ * ‖f x‖

One mollifier constant controls the pointwise tensor norm by the first field's L² norm and the second field's pointwise norm.