Young's inequality for the bounded drift term

This is the pointwise absorption used after the weak energy estimate. The norm conversion from the product norm on Vec 2 to its Euclidean gradient norm is provided by the Galerkin drift estimates.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.drift_product_le_young {B κ a c : ℝ} (hκ : 0 < κ) : B * a * c ≤ κ / 2 * a ^ 2 + B ^ 2 / (2 * κ) * c ^ 2

Young's inequality in the normalization used for a drift pairing.